Goedel-Prover：清华等推出的自动化形式证明生成语言模型

Goedel-Prover简介

Goedel-Prover是由普林斯顿大学语言与智能实验室联合清华大学、亚马逊、Meta FAIR等机构共同开发的开源大型语言模型（LLM）。该模型专注于自动化形式证明生成，通过将自然语言数学问题转化为形式化语言（Lean 4），并利用专家迭代技术训练证明器，显著提升了自动化定理证明的性能。Goedel-Prover在多个基准测试中取得了优异成绩，例如在miniF2F基准测试中达到57.6%的成功率，超越了之前的最佳开源模型。此外，它还在Lean Workbook中生成了近3万条形式化证明，几乎翻倍了此前的工作成果。该团队通过开源代码、模型和新发现的证明，为形式化数学和自动化定理证明领域的发展提供了重要推动。

Goedel-Prover主要功能

1. 自动化形式证明生成：Goedel-Prover能够自动生成数学问题的形式化证明，提升了数学推理和验证的自动化水平。
2. 自然语言到形式语言的转换：通过训练的形式化器，Goedel-Prover能够将自然语言的数学问题转换为形式化语言（Lean 4），便于机器处理和验证。
3. 高效的证明生成和验证：利用大规模数据集和专家迭代技术，Goedel-Prover能够生成并验证大量的形式化证明，显著提高了证明生成的效率和准确性。
4. 开源代码和模型：Goedel-Prover的代码和模型是开源的，研究人员可以访问和使用这些资源来进一步研究和改进自动化定理证明技术。

Goedel-Prover技术原理

1. 数据集构建：
   • 形式化陈述生成：通过训练两个形式化器（Formalizer A和B），将自然语言的数学问题转换为形式化语言（Lean 4）。这些形式化器分别基于Lean Workbook和Claude-sonnet-3.5的数据进行训练，以增加形式化风格的多样性。
   • 数据集规模：最终生成了1.64百万条形式化陈述，显著扩展了可用于训练的数据集。
2. 专家迭代（Expert Iteration）：
   • 初始证明生成：使用DeepSeek-Prover-V1.5-RL为每个形式化陈述生成16个证明候选，并通过Lean编译器验证。
   • 迭代训练：收集正确的证明，基于DeepSeek-Prover-V1.5-Base进行监督微调（SFT），生成新的证明器。每次迭代都增加新的证明到训练数据中，共进行了9次迭代。
3. 质量评估：
   • 编译正确性（CC）测试：确保形式化陈述符合Lean语法并能成功编译。
   • 忠实性与完整性（FC）测试：确保形式化陈述准确捕捉原始问题的含义，包含所有假设、条件和隐含定义。
4. 性能评估：基准测试：在多个基准测试（如miniF2F、PutnamBench、Lean Workbook、ProofNet等）中评估模型性能，Goedel-Prover在这些测试中均取得了优异成绩。
5. 开源与社区贡献：资源开放：开源代码、模型和新发现的证明，供研究人员使用和改进，推动形式化数学和自动化定理证明领域的发展。

Goedel-Prover应用场景

1. 数学研究与教育：自动化生成数学问题的形式化证明，帮助数学家验证复杂定理，辅助数学教育中难题的解析。
2. 形式化软件验证：用于验证软件系统的正确性，通过形式化证明确保代码逻辑无误，提高软件的可靠性和安全性。
3. 硬件设计验证：在芯片设计和硬件开发中，通过形式化方法验证硬件逻辑的正确性，减少设计缺陷。
4. 人工智能与机器学习：为AI模型提供可验证的推理能力，提升模型的可信度和解释性，特别是在安全关键领域。
5. 理论计算机科学：用于算法复杂性分析、图论等领域的定理证明，推动理论研究的发展。
6. 工业自动化与安全：在工业控制系统中，通过形式化验证确保系统的安全性和稳定性，减少潜在风险。

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