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

但是，這種推理模式有個(gè)缺點(diǎn)：難以通過機(jī)器來自動(dòng)驗(yàn)證。也因此，非形式化推理在實(shí)際應(yīng)用中的可靠性就大打折扣了。這還會讓研究者更加難以進(jìn)一步對推理模型進(jìn)行改進(jìn)。

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

近日，普林斯頓大學(xué)陳丹琦、Sanjeev Arora 和金馳領(lǐng)導(dǎo)的一個(gè)團(tuán)隊(duì)開源了一個(gè)用于自動(dòng)定理證明的形式化推理模型 Goedel-Prover（哥德爾證明器），并且該模型在數(shù)學(xué)問題的自動(dòng)形式化證明生成任務(wù)上達(dá)到了 SOTA。代碼、模型還有在 Lean Workbook 中發(fā)現(xiàn)的新證明都已開源！

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

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

不過，訓(xùn)練 LLM 用形式化語言進(jìn)行定理證明還存在一個(gè)重大挑戰(zhàn)，即缺少形式化數(shù)學(xué)陳述和證明。

對于用形式語言表達(dá)的定理，為其編寫證明的要求很高，需要相當(dāng)多的領(lǐng)域?qū)I(yè)知識。

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

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

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

為了將這些數(shù)據(jù)轉(zhuǎn)化為可用的形式語言，研究團(tuán)隊(duì)訓(xùn)練了兩個(gè)形式化轉(zhuǎn)換器。其中一個(gè)基于 Lean Workbook 中的非形式 - 形式語言對訓(xùn)練，另一個(gè)則采用 Claude-sonnet-3.5 標(biāo)注的語言對進(jìn)行訓(xùn)練。下圖展示了這些形式化轉(zhuǎn)換器的訓(xùn)練過程。

這兩個(gè)轉(zhuǎn)換器完成對原始語句的形式化后，團(tuán)隊(duì)還用 LLM 加了一道驗(yàn)證，確保形式化后的語句準(zhǔn)確保留了原始內(nèi)容的含義，成功構(gòu)建了一個(gè)含有 164 萬個(gè)形式語句的數(shù)據(jù)集。

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

Goedel-Prover 表現(xiàn)如何？

具體有多厲害呢？如下圖所示，在 miniF2F 上，新模型的解題正確率比之前的最優(yōu)模型（DeepSeek-Prover-V1.5-RL）提高了 7.6%。在 Pass@32、64 直至 25600 測試中，都始終優(yōu)于 DeepSeek-Prover-V1.5-RL。

新模型在 Lean Workbook 數(shù)學(xué)題庫中成功解決了 29.7K 道題目，這個(gè)成績差不多是其他頂尖模型（InternLM2.5-StepProver 和 InternLMMath-Plus）的兩倍。在 PutnamBench 上，新模型解決了 7 個(gè)問題（Pass@512），位列排行榜第一。

論文共同一作、普林斯頓博士后 Yong Lin 在 ?? 上表示他們目前正在開發(fā)這個(gè)哥德爾證明器的強(qiáng)化學(xué)習(xí)版本，并且還會有一個(gè)比之前更強(qiáng)大的檢查點(diǎn)模型。此外，他們還將在開源這個(gè)強(qiáng)化學(xué)習(xí)版本的同時(shí)附帶 164 萬條形式化陳述。

真是讓人期待。