Goedel‑Prover‑V2 SITES

一、什么是Goedel‑Prover‑V2？

Goedel‑Prover‑V2 是由普林斯顿大学联合清华、北大、斯坦福、NVIDIA、Meta FAIR、亚马逊等顶尖机构推出的开源自动定理证明模型，基于Qwen3‑8B 与 32B 模型进行专家迭代与强化学习训练。

它专注于自动生成和验证 Lean 4 形式化证明，是自动化数学定理推理领域的旗舰模型，支持 8B 与 32B 两个参数规模版本。

二、突出性能表现与突破

2.1 MiniF2F基准

• 8B 模型 在 MiniF2F Pass@32 上达 83.3%，性能比肩 DeepSeek‑Prover‑671B（671B 模型）。

• 32B 模型 在无自我修正的基础模式下 Pass@32 达 88.0%，而启用自我修正则达 90.4% 。

2.2 PutnamBench 排行

32B自我修正模式在 Pass@64 下解决了 64 道难题，一举登顶 PutnamBench，超过 DeepSeek‑Prover‑671B 的 47 道作答记录。

2.3 MathOlympiadBench

首发包含 360 道 IMO 级别问题的 MathOlympiadBench，在该数据集上 32B 模型同样展现领先能力。

2.4 推理规模曲线

32B 模型在各种 sampling budget 下均稳定领先多项其他顶级模型。

三、模型创新与训练方法

3.1 专家迭代 + 强化学习

以 Qwen3‑8B / 32B 为基础，采用专家示例引导、证明生成、验证采纳，再结合 Clan feedback 进行强化学习优化。

3.2 分层式数据合成

使用 Scaffolded Data Synthesis 自动生成难度递进的中间证明任务，建立平滑难度曲线，提升训练效率。

3.3 验证器引导的自我修正

模型输出初始证明后，会基于 Lean 编译反馈进行两轮自我修正，将反馈机制融入训练与推理阶段，改善正确率。

3.4 模型平均机制

训练到一定阶段时，将多个 checkpoint 与基座模型执行加权平均，用以恢复模型多样性，提升鲁棒性与 Pass@K 能力。

四、技术架构与流程详解

4.1 输入与输出

输入一条 Lean 4 形式化命题，模型生成候选证明片段，通过 Lean 编译器验证是否成立，不成立则根据错误进行修正。

4.2 推理流程

• 标准模式：直接生成单次推理证明输出；

• 自我修正模式：生成 + Lean 验证反馈 + 两轮迭代修正，共消耗约 40K token，上下文窗口默认 32K。

4.3 训练脚本

开源 repo 包含问题形式化、初步生成、验证反馈与 RL 策略脚本，支持 researchers reproduction 和定制训练流程。

五、如何使用 Goedel‑Prover‑V2？

5.1 模型获取

模型与 benchmark 可从 Hugging Face 下载：

• Goedel‑Prover‑V2‑32B；

• Goedel‑Prover‑V2‑8B
  均采用 Apache‑2.0 开源协议。

数据集 MathOlympiadBench 也同步开源，支持研究使用。

5.2 快速推理示例

from transformers import AutoTokenizer, AutoModelForCausalLM import torch model_id = "Goedel-LM/Goedel-Prover-V2-32B" tokenizer = AutoTokenizer.from_pretrained(model_id) model = AutoModelForCausalLM.from_pretrained(model_id, trust_remote_code=True, torch_dtype=torch.bfloat16, device_map="auto") prompt = "theorem my_theorem : ... proof :=" inputs = tokenizer(prompt, return_tensors="pt").to(model.device) outputs = model.generate(**inputs, max_new_tokens=4096) print(tokenizer.decode(outputs[0]))

用户可根据需要自行部署于 GPU 或支持 local inference platforms（如 llama.cpp），结合自定义验证器调用 Lean。

六、适用场景与目标用户

6.1 研究者与教育者

适合数学 AI、形式化定理证明方向的科研人员和教师，用于教学实验、benchmark 比对、方法创新等。

6.2 Agent 构建者

可作为推理工具接入 Agent 系统，通过函数调用处理形式化证明任务。

6.3 数学竞赛组织者

可自动生成或验证 mathematical formal proofs，辅助出题、评测或赛后校对。

6.4 AI 开发者

适合想集成形式验证能力的 AI 工具开发者，用于 proofs 校验与自动推理服务。