Goedel-Prover专为自动化数学问题的形式证明生成而设计的 LLM，快速解决形式化数学问题。今天跟大家分享一下 Goedel-Prover 这个由普林斯顿大学、清华大学等机构联合推出的开源自动化数学问题的形式证明生成模型。
🚀 快速阅读
Goedel-Prover 是一款专注于自动化数学问题的形式证明生成的开源模型。
- 核心功能：将自然语言数学问题翻译成形式语言，并自动生成完整的证明。
- 技术原理：基于专家迭代方法，逐步提升证明能力，处理大规模形式化陈述和证明数据集。
Goedel-Prover 是什么
Goedel-Prover（哥德尔证明器）是由普林斯顿大学、清华大学等机构联合推出的开源大型语言模型（LLM），专为自动化数学问题的形式证明生成而设计。该模型通过将自然语言数学问题翻译成形式语言（如 Lean 4），解决了形式化数学陈述和证明稀缺的问题。Goedel-Prover 使用专家迭代方法进行训练，基于不断扩展的形式证明数据集，逐步提升其证明能力。
在多个基准测试中，Goedel-Prover 表现出色。例如，在 miniF2F 基准测试中，Goedel-Prover 达到了 57.6% 的成功率，显著优于之前的开源模型。此外，它成功解决了 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
1. 安装依赖环境
安装 Lean 4按照 Lean 4 安装页面 的说明设置 Lean 4。
2. 快速启动
要运行推理并重现 miniF2F 上的性能，可以使用以下命令：
sh eval/eval.sh -i datasets/minif2f.jsonl -s test -m Goedel-LM/Goedel-Prover-SFT -o results/minif2f/Godel-Prover-SFT -n 32 -g 2 -c 128
结果将总结在 results/minif2f/Godel-Prover-SFT/compilation_summarize.json 文件中。
指定参数如下：
-i：要评估的数据集路径-s：要评估的数据集分割，通常设置为 \”test\”-m：模型名称或路径-o：输出目录-n：Pass 数量-g：用于推理的 GPU 数量-c：用于编译的 CPU 数量
资源
– GitHub 仓库：https://github.com/Goedel-LM/Goedel-Prover
❤️ 如果你也关注 AI 的发展现状，且对 AI 应用开发感兴趣，我会每日分享大模型与 AI 领域的开源项目和应用，提供运行实例和实用教程，帮助你快速上手AI技术！
