Goedel-Prover

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的应用领域有哪些？：该工具广泛应用于数学研究、教育、软件验证和跨学科研究等多个领域。