---
title: "Goedel-Prover – 自动化数学问题的形式证明生成开源推理模型"
url: "https://paooo.com/aigc-news/22020/"
author: "Prompt 语宙研究院"
published_at: "2026-06-09T08:33:28+08:00"
updated_at: "2026-06-09T08:33:28+08:00"
categories: "AIGC 资讯"
tags: "AI智能体, DeepSeek, HuggingFace, 大模型微调, 开源大模型"
source: "Prompt 语宙 (https://paooo.com)"
ai_tools_directory: "语宙 AI 导航 (https://ai.paooo.com)"
---

# Goedel-Prover – 自动化数学问题的形式证明生成开源推理模型

> 来源：[Prompt 语宙 (paooo.com)](https://paooo.com/aigc-news/22020/) · 作者：Prompt 语宙研究院 · 发布时间：2026-06-09

## AI 30 秒核心看点 (TL;DR)

- 基于专家迭代训练，Goedel-Prover 持续扩展证明数据并提升形式证明生成能力。
- 在 miniF2F 上取得 57.6% 成功率，且优于此前开源模型，验证了实测突破。
- 可用于数学研究、教学、软件验证与 AI 算法验证，覆盖多类高可信推理场景。

## 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](https://github.com/Goedel-LM/Goedel-Prover)

- **HuggingFace模型库**：[https://huggingface.co/Goedel-LM/Goedel-Prover](https://huggingface.co/Goedel-LM/Goedel-Prover-SFT)

- **arXiv技术论文**：[https://arxiv.org/pdf/2502.07640v1](https://arxiv.org/pdf/2502.07640v1)

## Goedel-Prover的应用场景

- **数学研究**：帮助数学家快速验证复杂定理的证明，加速研究进程。

- **数学教学**：为教师提供详细证明过程，辅助学生理解数学概念和逻辑。

- **软件验证**：验证软件算法的逻辑正确性，提高软件的可靠性和安全性。

- **AI算法验证**：验证AI算法的理论基础，确保其逻辑正确性和性能。

- **跨学科研究**：验证不同学科间理论联系，为跨学科研究提供理论支持。

## 常见问题解答 (FAQ)

### Goedel-Prover 是什么模型？
Goedel-Prover 是面向自动化数学证明的开源大型语言模型，核心任务是把自然语言数学问题翻译成 Lean 4 等形式语言，并生成可由编译器验证的形式证明。

### Goedel-Prover 的效果怎么样？
文中给出的结果显示，它在 miniF2F 基准上达到 57.6% 成功率，优于此前开源模型；还成功解决 PutnamBench 中 7 个问题，并为 Lean Workbook 生成近 3 万个形式证明。

### Goedel-Prover 适合哪些应用场景？
它适合数学研究、数学教学、软件验证、AI 算法验证和跨学科研究等场景，尤其适合需要高可信逻辑推理和形式化证明支持的任务。

---
探索 2,800+ 全球实用 AI 工具与官方直达入口：[语宙 AI 导航 (https://ai.paooo.com/)](https://ai.paooo.com/)