Goedel-Prover – 自動化數學問題的形式證明生成開源推理模型

Goedel-Prover是什么

Goedel-Prover（哥德爾證明器）是由普林斯頓大學和清華大學等多家機構聯合開發的開源大型語言模型（LLM），專注于數學問題的自動化形式證明生成。該模型通過將自然語言中的數學問題轉化為形式語言（如Lean 4），來生成形式化的證明，旨在解決形式化數學陳述和證明不足的挑戰。Goedel-Prover采用專家迭代的方法進行訓練，依托不斷擴充的形式證明數據集，逐步提升其證明能力。在多個基準測試中，Goedel-Prover的表現卓越，例如在miniF2F基準測試中達到了57.6%的成功率，顯著優于以往的開源模型。此外，Goedel-Prover成功解決了PutnamBench中的7個問題，并為Lean Workbook生成了近3萬個形式證明，為自動化定理證明領域帶來了重要的進展。

Goedel-Prover的主要功能

• 形式化翻譯：將自然語言的數學問題精確轉換為形式語言，確保翻譯的準確性和完整性。
• 證明生成：自動生成完整的數學證明，支持復雜的推理過程。
• 性能優化：通過專家迭代的方式不斷提升證明能力，增加成功率。
• 大規模數據處理：處理和生成大量的形式化陳述與證明數據集，增強模型的泛化能力。

Goedel-Prover的技術原理

• 形式化翻譯：
  • 利用兩個形式化器（Formalizer A和Formalizer B）將自然語言數學問題轉化為Lean 4的形式語言。兩個形式化器依據不同的數據集進行訓練，以增加形式化表達的多樣性。
  • 通過編譯正確性（CC）測試以及忠實性與完整性（FC）測試評估形式化陳述質量，確保其符合Lean的語法規范，且準確反映原始問題的含義。
• 專家迭代（Expert Iteration）：在初始階段，利用現有的證明器（如DeepSeek-Prover-V1.5-RL）為每個形式化陳述生成多個證明候選，并通過Lean編譯器驗證其正確性。將驗證通過的證明收集作為訓練數據，監督微調基礎模型（如DeepSeek-Prover-V1.5-Base），生成新的證明器。通過不斷的迭代，每次都用新證明器生成更多的證明，并將其整合入訓練數據中，逐步提升模型的證明能力。
• 數據集擴展：除了使用公開的Numina數據集外，Goedel-Prover還形式化了大量私人收集的數學問題，并與Lean Workbook中的現有陳述合并，形成大規模的形式化陳述數據集。在訓練過程中，逐步加入Mathlib4等外部數據集，以增強模型對不同數學領域的適應性。

Goedel-Prover的項目地址

• GitHub倉庫：https://github.com/Goedel-LM/Goedel-Prover
• HuggingFace模型庫：https://huggingface.co/Goedel-LM/Goedel-Prover
• arXiv技術論文：https://arxiv.org/pdf/2502.07640v1

Goedel-Prover的應用場景

• 數學研究：協助數學家快速驗證復雜定理的證明，從而加速研究進展。
• 數學教學：為教師提供詳細的證明過程，幫助學生理解數學概念和邏輯。
• 軟件驗證：驗證軟件算法的邏輯正確性，提升軟件的可靠性與安全性。
• AI算法驗證：確保AI算法的理論基礎具有邏輯正確性與卓越性能。
• 跨學科研究：驗證不同學科之間的理論聯系，為跨學科研究提供有力的理論支持。

常見問題

• Goedel-Prover支持哪些語言？：當前主要支持Lean 4形式語言。
• 如何獲取Goedel-Prover的最新版本？：您可以通過GitHub倉庫訪問最新版本和更新。
• Goedel-Prover的訓練數據來源是什么？：訓練數據來自多個公開和私人數據集，包括Numina和Mathlib4。
• Goedel-Prover的應用領域有哪些？：該工具廣泛應用于數學研究、教育、軟件驗證和跨學科研究等多個領域。