哥德爾-Prover超過DeepSeek-Prover，陳丹琦團隊造出當前最強形式化推理模型

作者：機器之心 2025-02-13 12:23:28

近日，普林斯頓大學陳丹琦、Sanjeev Arora 和金馳領導的一個團隊開源了一個用于自動定理證明的形式化推理模型 Goedel-Prover（哥德爾證明器），并且該模型在數學問題的自動形式化證明生成任務上達到了 SOTA。

最近一段時間，以 DeepSeek-R1 為代表的大型推理模型可謂是「當紅炸子雞」，不過整體來說，這些模型所做的推理都屬于非形式化推理（informal reasoning）。也就是說，它們主要是通過自然語言執行推理。

但是，這種推理模式有個缺點：難以通過機器來自動驗證。也因此，非形式化推理在實際應用中的可靠性就大打折扣了。這還會讓研究者更加難以進一步對推理模型進行改進。

解決方案也很直觀：形式化推理（formal reasoning）。

近日，普林斯頓大學陳丹琦、Sanjeev Arora 和金馳領導的一個團隊開源了一個用于自動定理證明的形式化推理模型 Goedel-Prover（哥德爾證明器），并且該模型在數學問題的自動形式化證明生成任務上達到了 SOTA。代碼、模型還有在 Lean Workbook 中發現的新證明都已開源！

論文標題：Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
論文鏈接：https://arxiv.org/abs/2502.07640v1
項目地址：https://github.com/Goedel-LM/Goedel-Prover
Hugging Face：https://huggingface.co/Goedel-LM/Goedel-Prover-SFT

首先，先簡單解釋一下什么是形式化推理：簡單來說，形式化推理就是以機器可驗證的格式進行推理。這一類別中，比較知名的證明助手包括 Lean、Isabelle 和 Coq，它們都具備各自的形式語言（formal language），能以可被機器驗證的方式表達推理。因此，訓練 LLM 用這些形式語言編寫證明具有重要意義。

不過，訓練 LLM 用形式化語言進行定理證明還存在一個重大挑戰，即缺少形式化數學陳述和證明。

對于用形式語言表達的定理，為其編寫證明的要求很高，需要相當多的領域專業知識。

正因如此，目前公開的形式語言數據集規模都很有限。例如，Lean Workbook 數據集共有 140K 條形式化陳述，其中的形式化陳述使用了 Lean 來陳述問題，但沒有證明。這些陳述中，只有 15.7K 條帶有形式化證明，這些證明是由 InternLM2.5-StepProver 和 InternLM-Math-Plus 發現的。此外，Open Bootstrapped Theorems 數據集包含 107K 條陳述，其證明來自 Mathlib44。

然而，該團隊觀察到 Mathlib4 的分布與一般的問題求解基準（例如廣泛使用的 miniF2F）的分布存在顯著差異。例如，miniF2F 中的陳述主要來自高中數學，需要復雜的推理能力才能解決，而 Mathlib4 中的陳述則側重于對高級數學概念的簡單操作。此外，他們還發現將 Mathlib4 數據納入訓練并不能持續提高模型在 miniF2F 上的性能。

與形式語言的數據稀缺相比，用自然語言書寫的數學題卻有著海量數據儲備，高中生桌子上堆滿的「五三」就是一座座富礦。Numina 數據集更是收錄了 86 萬個高質量的問答對，囊括國內外的中小學數學題、國際奧數競賽題以及合成數據等等。

為了將這些數據轉化為可用的形式語言，研究團隊訓練了兩個形式化轉換器。其中一個基于 Lean Workbook 中的非形式 - 形式語言對訓練，另一個則采用 Claude-sonnet-3.5 標注的語言對進行訓練。下圖展示了這些形式化轉換器的訓練過程。

這兩個轉換器完成對原始語句的形式化后，團隊還用 LLM 加了一道驗證，確保形式化后的語句準確保留了原始內容的含義，成功構建了一個含有 164 萬個形式語句的數據集。

利用這個大規模形式化定理數據集，研究團隊采用了一種循環改進的方法，稱為專家迭代（expert iteration）：先用現有的最好模型（DeepSeek-Prover-V1.5-RL）去嘗試解答大量數學題目，把解對的答案收集起來訓練新模型，然后用新模型再去解題，不斷重復這個過程。經過 8 輪這樣的「以老帶新」訓練后，他們的新模型變得更加厲害了。下圖展示了專家迭代的過程。