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算法的理论基础，确保其逻辑正确性和性能。
• 跨学科研究：验证不同学科间理论联系，为跨学科研究提供理论支持。