Goedel-Prover – 自動(dòng)化數(shù)學(xué)問(wèn)題的形式證明生成開(kāi)源推理模型

Goedel-Prover是什么

Goedel-Prover（哥德?tīng)栕C明器）是由普林斯頓大學(xué)和清華大學(xué)等多家機(jī)構(gòu)聯(lián)合開(kāi)發(fā)的開(kāi)源大型語(yǔ)言模型（LLM），專注于數(shù)學(xué)問(wèn)題的自動(dòng)化形式證明生成。該模型通過(guò)將自然語(yǔ)言中的數(shù)學(xué)問(wèn)題轉(zhuǎn)化為形式語(yǔ)言（如Lean 4），來(lái)生成形式化的證明，旨在解決形式化數(shù)學(xué)陳述和證明不足的挑戰(zhàn)。Goedel-Prover采用專家迭代的方法進(jìn)行訓(xùn)練，依托不斷擴(kuò)充的形式證明數(shù)據(jù)集，逐步提升其證明能力。在多個(gè)基準(zhǔn)測(cè)試中，Goedel-Prover的表現(xiàn)卓越，例如在miniF2F基準(zhǔn)測(cè)試中達(dá)到了57.6%的成功率，顯著優(yōu)于以往的開(kāi)源模型。此外，Goedel-Prover成功解決了PutnamBench中的7個(gè)問(wèn)題，并為L(zhǎng)ean Workbook生成了近3萬(wàn)個(gè)形式證明，為自動(dòng)化定理證明領(lǐng)域帶來(lái)了重要的進(jìn)展。

Goedel-Prover的主要功能

• 形式化翻譯：將自然語(yǔ)言的數(shù)學(xué)問(wèn)題精確轉(zhuǎn)換為形式語(yǔ)言，確保翻譯的準(zhǔn)確性和完整性。
• 證明生成：自動(dòng)生成完整的數(shù)學(xué)證明，支持復(fù)雜的推理過(guò)程。
• 性能優(yōu)化：通過(guò)專家迭代的方式不斷提升證明能力，增加成功率。
• 大規(guī)模數(shù)據(jù)處理：處理和生成大量的形式化陳述與證明數(shù)據(jù)集，增強(qiáng)模型的泛化能力。

Goedel-Prover的技術(shù)原理

• 形式化翻譯：
  • 利用兩個(gè)形式化器（Formalizer A和Formalizer B）將自然語(yǔ)言數(shù)學(xué)問(wèn)題轉(zhuǎn)化為L(zhǎng)ean 4的形式語(yǔ)言。兩個(gè)形式化器依據(jù)不同的數(shù)據(jù)集進(jìn)行訓(xùn)練，以增加形式化表達(dá)的多樣性。
  • 通過(guò)編譯正確性（CC）測(cè)試以及忠實(shí)性與完整性（FC）測(cè)試評(píng)估形式化陳述質(zhì)量，確保其符合Lean的語(yǔ)法規(guī)范，且準(zhǔn)確反映原始問(wèn)題的含義。
• 專家迭代（Expert Iteration）：在初始階段，利用現(xiàn)有的證明器（如DeepSeek-Prover-V1.5-RL）為每個(gè)形式化陳述生成多個(gè)證明候選，并通過(guò)Lean編譯器驗(yàn)證其正確性。將驗(yàn)證通過(guò)的證明收集作為訓(xùn)練數(shù)據(jù)，監(jiān)督微調(diào)基礎(chǔ)模型（如DeepSeek-Prover-V1.5-Base），生成新的證明器。通過(guò)不斷的迭代，每次都用新證明器生成更多的證明，并將其整合入訓(xùn)練數(shù)據(jù)中，逐步提升模型的證明能力。
• 數(shù)據(jù)集擴(kuò)展：除了使用公開(kāi)的Numina數(shù)據(jù)集外，Goedel-Prover還形式化了大量私人收集的數(shù)學(xué)問(wèn)題，并與Lean Workbook中的現(xiàn)有陳述合并，形成大規(guī)模的形式化陳述數(shù)據(jù)集。在訓(xùn)練過(guò)程中，逐步加入Mathlib4等外部數(shù)據(jù)集，以增強(qiáng)模型對(duì)不同數(shù)學(xué)領(lǐng)域的適應(yīng)性。

Goedel-Prover的項(xiàng)目地址

• GitHub倉(cāng)庫(kù)：https://github.com/Goedel-LM/Goedel-Prover
• HuggingFace模型庫(kù)：https://huggingface.co/Goedel-LM/Goedel-Prover
• arXiv技術(shù)論文：https://arxiv.org/pdf/2502.07640v1

Goedel-Prover的應(yīng)用場(chǎng)景

• 數(shù)學(xué)研究：協(xié)助數(shù)學(xué)家快速驗(yàn)證復(fù)雜定理的證明，從而加速研究進(jìn)展。
• 數(shù)學(xué)教學(xué)：為教師提供詳細(xì)的證明過(guò)程，幫助學(xué)生理解數(shù)學(xué)概念和邏輯。
• 軟件驗(yàn)證：驗(yàn)證軟件算法的邏輯正確性，提升軟件的可靠性與安全性。
• AI算法驗(yàn)證：確保AI算法的理論基礎(chǔ)具有邏輯正確性與卓越性能。
• 跨學(xué)科研究：驗(yàn)證不同學(xué)科之間的理論聯(lián)系，為跨學(xué)科研究提供有力的理論支持。

常見(jiàn)問(wèn)題

• Goedel-Prover支持哪些語(yǔ)言？：當(dāng)前主要支持Lean 4形式語(yǔ)言。
• 如何獲取Goedel-Prover的最新版本？：您可以通過(guò)GitHub倉(cāng)庫(kù)訪問(wèn)最新版本和更新。
• Goedel-Prover的訓(xùn)練數(shù)據(jù)來(lái)源是什么？：訓(xùn)練數(shù)據(jù)來(lái)自多個(gè)公開(kāi)和私人數(shù)據(jù)集，包括Numina和Mathlib4。
• Goedel-Prover的應(yīng)用領(lǐng)域有哪些？：該工具廣泛應(yīng)用于數(shù)學(xué)研究、教育、軟件驗(yàn)證和跨學(xué)科研究等多個(gè)領(lǐng)域。