2025年5月，來自香港中文大學、Numina、西湖大學、M-A-P、2077AI、加州大學洛杉磯分校以及德國圖賓根馬克斯·普朗克智能系統研究所的研究團隊聯合發布了一項重要研究成果—FormalMATH，這是一個用于評估大型語言模型(LLM)形式化數學推理能力的全新基準。該研究已于2025年5月5日發布在arXiv預印本平臺上，標識號為arXiv:2505.02735v1。

這項由俞周良、彭若天、丁可意等研究者共同領導的工作，旨在解決人工智能形式化數學推理領域面臨的關鍵挑戰。為什么這項研究值得關注？想象一下，我們希望計算機不僅能計算出數學問題的答案，還能像數學家一樣提供嚴格的、無懈可擊的證明。這就是形式化數學推理的核心——不僅要知道"是什么"，還要能夠嚴格證明"為什么"。

一、形式化數學推理：AI面臨的挑戰與契機

形式化數學推理（FMR）是數學實踐的一種特殊形式，它基于形式系統提供嚴格的公理化框架，對自動化證明驗證至關重要。然而，這對人類專家來說都極具挑戰性。例如，"Liquid Tensor實驗"和"多項式Freiman-Ruzsa猜想"這樣的數學難題，即使人類專家投入多年努力也尚未完全形式化證明。

想象一下，當你在解答一道復雜的數學題時，你不僅需要給出答案，還需要詳細解釋每一步推導的理由，不能有任何邏輯跳躍或假設——這就是形式化數學推理的嚴格要求。

近年來，大型語言模型(LLM)在這一領域展現出巨大潛力。研究人員通過自監督學習、思維鏈(CoT)微調以及可擴展的樹搜索等技術，使LLM能夠探索復雜的證明策略。盡管現有評估LLM形式化數學推理能力的基準如MiniF2F和ProofNet被廣泛使用，但它們存在幾個關鍵局限：

范圍局限：現有基準覆蓋面狹窄。例如，MiniF2F僅限于高中級別的代數和數論，而ProofNet則集中于本科級別的分析和代數。這種狹窄的范圍限制了對形式化數學推理能力的全面評估。

數據集規模：目前的形式化數學基準相對較小。MiniF2F測試集僅包含244個問題，ProofNet僅有186個。這限制了基準測試的穩健性，阻礙了可泛化FMR系統的開發。

性能飽和：目前最先進的定理證明器，如Kimina-Prover，在現有基準上的成功率已超過80.7%，表明這些基準可能接近其實用效用的極限。

二、FormalMATH：一個全面的形式化數學推理基準

為了解決上述限制，研究團隊引入了FormalMATH——一個基于Lean4的大規模基準，包含5,560個經過形式化驗證的數學陳述。這些問題涵蓋了廣泛的數學領域，如代數、幾何、微積分、數論和離散數學等，同時橫跨多個難度級別，從高中奧林匹克難題到本科水平定理。

FormalMATH的開發面臨兩大主要挑戰：

自動形式化難度：缺乏可靠的工具將自然語言問題轉換為精確的Lean4語句，特別是對于需要嚴格語義保留的高級數學領域。

驗證形式化語句需要確保語法正確性（通過Lean4編譯器檢查）和與原始問題的語義一致性——即使對人類專家來說，這也是一項技術上要求高且耗時的工作。

為應對這些挑戰，研究團隊提出了一個人機協作框架。這個框架通過集成以下技術大大減少了生成形式化數學語句所需的人工標注工作：

基于集成的自動形式化：通過best-of-N采樣使用多個大語言模型進行自動形式化。

自動化驗證：一個三層管道確保正確性——編譯器語法驗證、多LLM語義驗證，以及基于否定的反證來過濾不可證明的定理。

這種策略在保持高準確性的同時最小化了人工驗證工作，在最終的FormalMATH中保留了72.09%的翻譯語句。

三、研究發現：現有定理證明器的優勢與局限

當研究團隊在FormalMATH基準上評估最先進的LLM定理證明器時，發現了這些系統面臨的顯著挑戰。以最佳表現的模型Kimina-Prover為例，在FormalMATH-Full數據集上使用pass@32指標僅達到16.46%的準確率，而使用最佳優先搜索的BFS-Prover在采樣預算為1×32×100的情況下僅獲得11.13%的成功率。

想象一場數學競賽，最優秀的AI選手也只能正確解決約16%的問題！這一結果表明，盡管AI在許多領域取得了令人印象深刻的進展，但在嚴格的形式化數學推理方面，仍有很長的路要走。

對這些結果的分析揭示了幾個有趣的見解：

領域偏差顯著：現有證明器在不同數學領域的表現差異很大，主要擅長高中級別的代數和應用數學，而在其他數學領域如微積分方面則表現較差。這強調了它們在跨領域泛化能力方面的關鍵差距。

過度依賴簡化自動化策略：證明器經常將多步推理簡化為單一策略調用（如"aesop"和"linearith"），繞過了必要的推導嚴謹性。

思維鏈推理的反直覺影響：雖然思維鏈(CoT)推理提高了FormalMATH語句的性能，但添加自然語言解決方案實際上降低了成功率。這表明在形式化推理環境中，人類編寫的非形式化推理可能引入的是噪聲而非清晰度。

就像一個懂得基本運算但不理解數學推理原理的學生，這些AI系統可以執行某些操作，但在構建完整、嚴謹的證明時仍然面臨困難。

四、人機協作的自動形式化流水線

FormalMATH的核心創新之一是提出了一個高效的人機協作自動形式化流水線。這個系統如同一個翻譯團隊，將普通數學問題轉換為計算機可以理解和驗證的形式化語言。

研究團隊首先利用兩類LLM——專門用于編碼的LLM（如Qwen2.5-7B-Coder）和預訓練的定理證明LLM（如Deepseek-prover-base）。通過讓通用大語言模型（如GPT-4）反復將自然語言語句翻譯成Lean4語句，然后將每個候選語句傳遞給Lean4編譯器，并且只保留通過類型檢查的語句，研究團隊創建了一個高質量的9,260對訓練示例語料庫，最終用于微調他們自己的自動形式化模型。

整個流程包括以下幾個關鍵步驟：

自動形式化：對于每個自動形式化器（由LLM實現），采用best-of-N采樣策略生成N個形式候選語句。所有候選語句首先通過Lean4編譯器進行語法正確性驗證，只有語法有效的語句才會被保留用于后續語義驗證。

基于LLM的語義驗證：研究團隊使用多個強大的通用LLM（如o1-mini、claude-3.5-Sonnet）來評估自然語言數學問題與其Lean4形式化之間的語義一致性。每個模型采用思維鏈推理完成以下程序：(1)將Lean4語句反向翻譯為自然語言，(2)比較重構的描述與原始問題，(3)提供二元判斷（一致/不一致）。只有通過所有LLM語義驗證的Lean4語句才會被收集。

通過證明其否定來推翻錯誤語句：受排中律啟發，研究團隊進一步過濾出某些不可證明的形式化語句。對于任何形式化語句，他們執行以下步驟：(1)構造其邏輯否定，(2)對該否定進行自動化證明嘗試。如果成功證明了某個語句的否定，則原語句在該形式系統中不成立。

專家驗證：研究團隊招募了12位國際數學奧林匹克獎牌獲得者級別的人類專家，手動檢查自然語言語句與其Lean4形式化之間的語義一致性。結果表明，他們的多LLM自動形式化和驗證流水線具有實質性的效率，從LLM語義驗證的最后階段（從30.1%）保留了72.1%的語句（到21.7%），同時顯著減少了人工驗證工作。

五、深入分析現有證明器的常見錯誤模式

為了更好地理解現有證明器的局限性，研究團隊系統分析了它們的常見錯誤模式。就像一位教練分析運動員比賽錄像以找出改進點，研究者們仔細檢查了這些AI系統在嘗試證明復雜數學問題時的失誤。

他們發現了四種最常見的錯誤模式：

不當使用自動化策略：現有的基于LLM的Lean4證明器頻繁生成過度依賴自動化策略的證明，如aesop、simp和linarith，以簡化策略式證明所需的低級、逐步推理。這些策略依賴于固定的啟發式算法和預標記的引理，可能無法匹配每個證明的結構。當過度調用或配置不當時，它們可能會顯著擴展搜索空間，導致非終止或超時，甚至將目標轉換為不相關或不可解的形式。

處理復雜不等式的能力不足：當前的證明器過度依賴linarith和nlinarith來找出線性和部分非線性不等式假設之間的矛盾。使用它們的常見程序要求證明器能夠(1)混合高次多項式和有理函數，(2)利用循環或對稱結構，以及(3)使用特定領域的引理（如重排、Chebyshev、AM-GM變體）。

引入冗余假設：當前基于LLM的定理證明器的一個常見錯誤來自引入結構上冗余的假設。雖然這些本身不會導致邏輯錯誤，但它們會模糊證明的基本邏輯并降低可讀性。

不完整的證明：另一種常見的失效模式是生成未完成的證明嘗試，留下未解決的關鍵子目標或依賴于沒有證明中間步驟的占位符策略。

這些錯誤模式就像數學學習過程中的常見陷阱。例如，學生可能知道某個公式但不理解何時以及如何正確應用它，或者在解題過程中遺漏關鍵步驟。這些觀察為改進未來的AI定理證明器提供了寶貴線索。

六、測試時計算擴展的有限回報

受近期測試時計算擴展成功的啟發，研究團隊還研究了其對形式化數學推理能力的影響。為了簡化，他們只評估了最佳優先搜索（BFS）和重復采樣在FormalMATH基準上的表現。

為了進行系統評估，研究者們引入了FormalMATH-Lite，這是FormalMATH的一個精心選擇的子集，包含425個問題（359個高中水平和66個本科水平問題），設計用于高效但嚴格的測試時擴展分析。

結果顯示，在形式化定理證明上應用測試時擴展獲得的回報有限。例如，STP僅獲得4.58%的絕對改進（從48.59%@Pass@32到53.17%@Pass@3200），盡管采樣預算增加了100倍。雖然BFS-Prover展示了更好的擴展動態，在預算擴展32倍的情況下獲得18.78%的提升（從27.10%@Pass@1×32×100到45.88%@Pass@32×32×100），但相對于單次生成方法仍然表現不佳。

這與非形式推理中近乎線性的擴展性能增長形成鮮明對比。在非形式數學中，采樣過程中的偽連續獎勵信號創造了路徑，使得不完美的推理鏈，盡管存在邏輯缺陷，有時也能"偶然"得到正確答案。這表明即使中間步驟不嚴格合理，有效結論也可能出現。

形式定理證明缺乏這種容忍度。一個錯誤放置的策略或類型錯誤會使整個證明軌跡無效，使增量采樣無效。雖然驗證器引導的證明搜索（例如，可訪問中間證明狀態的BFS）在理論上比單步生成方法更能緩解這種脆弱性，但當前實現在計算上仍不實用，缺乏擴展效率。

七、思維鏈推理對形式化數學的影響

研究團隊還評估了不同推理策略在Lean4證明生成中的效果：(1)樸素思維鏈提示，(2)增強自然語言的思維鏈，以及(3)vanilla生成策略。目標是測量非正式數學推理在多大程度上有助于隨后推導的形式化證明的嚴謹性和有效性。

結果顯示，在SFT和RL兩種配置中，解碼策略的排名一致。通常，樸素思維鏈獲得最高Pass@K（從K等于32到3200）準確率，而增強自然語言的思維鏈表現介于樸素思維鏈和vanilla解碼之間。例如，在K=3200時，DeepSeek-V1.5-SFT使用思維鏈達到50.6%，使用增強自然語言的思維鏈達到49.2%，使用vanilla解碼達到47.0%。

這一發現展示了一個反直覺的現象：增強自然語言的思維鏈并沒有比簡單的思維鏈產生更好的結果。研究表明，自然語言指導與Lean4的策略空間之間存在內在不匹配。

想象一個數學老師給學生一個解題的大致思路，但沒有提供詳細的步驟。對于一個理解基礎數學但不熟悉特定證明技巧的學生來說，這種高層次的指導可能幫助不大，甚至可能增加混淆。這就是為什么在某些情況下，沒有額外人類引導的AI可能表現得更好——它可以按照自己的"思考方式"構建證明，而不必嘗試將人類的非形式化思維翻譯成精確的形式化步驟。

結語：未來的方向與挑戰

FormalMATH提供了一個強大的基準，用于評估形式化數學推理。研究發現揭示了當前LLM在這一領域的基本局限：(1)即使最強大的模型也只能在FormalMATH上達到16.46%的成功率，(2)現有證明器展示出嚴重的領域偏差，在代數等領域表現良好，但在微積分等其他領域表現不佳，(3)令人驚訝的是，在思維鏈場景中提供自然語言解決方案指導反而降低了證明成功率。

這些限制表明了改進基于LLM的證明器的重要潛在方向。就像人類在學習數學證明時需要逐步掌握從基礎到高級的技能，AI系統也需要更復雜、更強大的方法來克服當前的局限性。

FormalMATH的創新之處在于它不僅指出了問題，還提供了一個可擴展的框架來評估和改進未來的系統。通過其全面的基準和詳細的錯誤分析，它為研究人員提供了寶貴的見解，指導下一代AI形式化數學推理系統的開發。

想象未來，AI系統不僅能夠解決數學問題，還能提供人類可理解且機器可驗證的嚴格證明，這將在科學研究、軟件驗證和數學教育中開辟新的可能性。FormalMATH是朝著這一遠大目標邁出的重要一步。

對于想深入了解這項研究的讀者，可以通過論文項目網頁、GitHub倉庫或Huggingface數據集獲取更多信息，這些鏈接都可以在原始論文中找到。