Goedel-Prover：AI 自动证明数学题！

摘要： 普林斯顿大学、清华大学等机构联合推出开源大型语言模型Goedel-Prover，旨在自动化数学问题的形式证明生成。该模型通过将自然语言数学问题翻译成形式语言，并利用专家迭代方法训练，显著提升了证明能力，为数学研究、教学以及软件验证等领域带来重大突破。

人工智能（AI）正以前所未有的速度渗透到各个领域，其中，数学领域也迎来了新的变革。近日，由普林斯顿大学、清华大学等顶尖学府的研究人员联合开发的开源大型语言模型Goedel-Prover正式发布，为自动化数学问题的形式证明生成带来了新的曙光。

Goedel-Prover是什么？

Goedel-Prover，又称哥德尔证明器，是一个基于大型语言模型（LLM）的开源项目，其核心目标是自动化数学问题的形式证明生成。传统上，数学证明是一项高度依赖人工的任务，需要专业的数学知识和严谨的逻辑推理。Goedel-Prover的出现，旨在通过AI技术简化这一过程，提高数学研究和教学的效率。

核心功能与技术原理

Goedel-Prover的核心功能在于将自然语言描述的数学问题翻译成形式语言，如Lean 4，并自动生成相应的形式化证明。这一过程涉及以下关键技术：

形式化翻译： Goedel-Prover采用两个独立的“形式化器”（Formalizer A和Formalizer B）将自然语言数学问题转换为形式语言。这两个形式化器基于不同的数据集进行训练，从而增加了形式化风格的多样性。为了确保翻译的准确性和完整性，模型还利用编译正确性（CC）测试和忠实性与完整性（FC）测试来评估形式化陈述的质量。
专家迭代（Expert Iteration）： 该模型采用专家迭代方法进行训练。初始阶段，利用现有的证明器（如DeepSeek-Prover-V1.5-RL）为每个形式化陈述生成多个证明候选。然后，通过Lean编译器验证这些证明的正确性。验证通过的证明被收集起来，作为训练数据，对基础模型（如DeepSeek-Prover-V1.5-Base）进行监督微调，生成新的证明器。这个过程不断重复，每次迭代都用新的证明器生成更多的证明，并将其加入训练数据，从而逐步提升模型的证明能力。
数据集扩展： 除了使用公开的Numina数据集外，Goedel-Prover还形式化了大量私人收集的数学问题，并与Lean Workbook中的现有陈述合并，形成大规模的形式化陈述数据集。在训练过程中，逐步加入Mathlib4等外部数据集，增强模型对不同数学领域的适应能力。

性能表现与应用前景

Goedel-Prover在多个基准测试中表现出色。例如，在miniF2F基准测试中，该模型达到了57.6%的成功率，显著优于之前的开源模型。此外，Goedel-Prover还成功解决了PutnamBench中的7个问题，并为Lean Workbook生成了近3万个形式证明。

Goedel-Prover的应用场景广泛，包括：

数学研究： 帮助数学家快速验证复杂定理的证明，加速研究进程。
数学教学： 为教师提供详细证明过程，辅助学生理解数学概念和逻辑。
软件验证： 验证软件算法的逻辑正确性，提高软件的可靠性和安全性。
AI算法验证： 验证AI算法的理论基础，确保其逻辑正确性和性能。
跨学科研究： 验证不同学科间理论联系，为跨学科研究提供理论支持。

开源与未来展望

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技术的不断发展，我们有理由相信，未来的数学研究将更加高效和智能化。

参考文献：