作者：昇腾实战派
知识地图：【昇腾实战派】综合指导

本文聚焦昇腾 NPU 环境下Goedel-Prover的完整部署流程。从 CANN 驱动、torch_npu 适配、vLLM-Ascend 推理引擎到 Lean 4 形式验证，手把手带你将这款开源 SOTA 数学定理证明模型落地在国产算力上。

---

一、前言：当大模型开始“证明数学定理”

数学定理的自动形式化证明，一直是 AI 领域最具挑战性的方向之一。与常规的文本生成不同，形式证明要求模型输出的每一步都必须经得起 Lean、Coq 等证明器严格编译与校验，错一个符号就可能导致整段证明失效。

近年来，从 DeepSeek-Prover 到 Leanabell-Prover，开源社区在这条路上不断突破。而 Goedel-Prover 的出现，把开源模型的天花板再次抬高：

• 📌 miniF2F Pass@32 达到 57.6%，超越 DeepSeek-Prover-V1.5-RL 7.6 个百分点；
• 📌 在 PutnamBench 上解决 7 道难题，登顶当时开源榜单；
• 📌 仅通过监督微调（SFT）就取得上述成绩，无需强化学习；
• 📌 代码、模型、数据集、29.7K Lean 4 证明全部开源。

图：Goedel-Prover-SFT 在多项基准测试中的性能对比。

（左） miniF2F 基准上 Pass@32 的全证明生成性能；
（中） Goedel-Prover-SFT 与 DeepSeek-Prover-v1.5 在不同推理预算（Pass@32 至 Pass@4×6400）下的 miniF2F 性能对比；
（右） 在 Lean Workbook 中成功解决并开源的问题数量对比（本模型解决 29.7K 题，此前最优工作为 15.7K 题）。

下面我们从原理到实战，带你全面认识这款模型。

---

二、Goedel-Prover 是什么？

Goedel-Prover 是 Goedel-LM 团队开源的、面向 Lean 4 的自动化形式定理证明模型。它的核心思路可以概括为一句话：

用“数据合成 + 迭代证明 + 监督微调”的方式，把自然语言数学问题转化为可验证的 Lean 4 形式证明。

2.1 核心数据集：Goedel-Pset-v1

形式证明最大的瓶颈之一是“高质量形式化题目太少”。Goedel-LM 的解法分三步：

1. 形式化翻译：训练 LLM 把 Numina 数据集中的自然语言数学题目，翻译成等价的 Lean 4 定理陈述，得到 Goedel-Pset-v1（约 164 万条形式化陈述）；
2. 迭代证明：训练一系列 prover，每一代都能证明前一代证不出的题目，并把新证明不断加入训练集；
3. 构建 Goedel-Pset-v1-solved：最终沉淀出超过 80 万条带完整证明的形式化题目，用于训练最终模型。

2.2 模型架构

Goedel-Prover 并没有重新设计 Transformer 结构，而是站在巨人肩膀上：

项目	说明
基座模型	deepseek-ai/DeepSeek-Prover-V1.5-Base
参数量	7B
训练方式	在 Goedel-Pset-v1-solved 上做 SFT
输出格式	完整 Lean 4 证明脚本
代表模型	Goedel-LM/Goedel-Prover-SFT

💡 也就是说，Goedel-Prover 的“黑科技”主要体现在 数据工程与迭代训练策略，而非模型结构本身。

---

三、性能表现：开源 SOTA 有多强？

3.1 miniF2F 基准测试

miniF2F 是形式定理证明领域最权威的公开基准之一，涵盖高中数学竞赛级别题目。

模型	推理预算	miniF2F Pass
DeepSeek-Prover-V1	@32	46.1%
DeepSeek-Prover-V1.5-SFT	@32	48.2%
DeepSeek-Prover-V1.5-RL	@32	50.0%
Goedel-Prover-SFT	@32	57.6% ± 0.7%
DeepSeek-Prover-V1.5-RL	@3200	54.9%
Goedel-Prover-SFT	@3200	62.7%
DeepSeek-Prover-V1.5-RL	4×6400	58.5%
Goedel-Prover-SFT	4×6400	64.7%

可以看到，Goedel-Prover-SFT 在不同推理预算下均领先，且没有使用强化学习，训练流程更加简洁可控。

3.2 其他亮眼成绩

• PutnamBench：在 Pass@512 设置下解决 7 道题目，位居当时开源榜单第一；
• Lean Workbook：开源了 29,700+ 条形式化证明，几乎是此前最好结果（15.7K）的两倍；
• 后续基于 Goedel-Prover 继续训练的 Leanabell-Prover 更是将 Pass@32 提升到 59.8%，验证了这套数据与基座的高度可扩展性。

---

四、昇腾 NPU环境搭建

4.1 组件版本要求

组件	版本
HDK	25.3.rc1.2
CANN	8.3.RC1
Python	3.10
torch	5.1
torch-npu	5.1

⚠️ 如果你使用 GPU 环境，可直接忽略 NPU 相关依赖，按常规 PyTorch + CUDA 方式安装即可。

4.2 拉取仓库

git clone https://gitcode.com/AI4Science/LifeScience.git
cd LifeScience/PyTorch/Goedel-Prover
git clone --recurse-submodules https://github.com/Goedel-LM/Goedel-Prover.git
cd Goedel-Prover

4.3 创建 conda 环境

conda create -n goedel-prover python=3.10 -y
conda activate goedel-prover

4.4 安装依赖

export PIP_INDEX_URL=https://repo.huaweicloud.com/repository/pypi/simple/
pip install -r requirements.txt

requirements.txt 中主要包含：

setuptools<71
torch==2.5.1
torch_npu==2.5.1.post1
pytz==2022.1
termcolor==2.4.0
easydict==1.13
tabulate==0.9.0
transformers==4.46.1
numpy==1.26.4
pandas==1.4.3
accelerate==0.33.0
decorator
attrs
psutil
absl-py
cloudpickle
ml-dtypes
scipy
tornado

4.5 验证 PyTorch / torch_npu

python3 -c "import torch; import torch_npu; a = torch.randn(3, 4).npu(); print(a + a);"

正常输出类似：

tensor([[-0.6066,  6.3385,  0.0379,  3.3356],
        [ 2.9243,  3.3134, -1.5465,  0.1916],
        [-2.1807,  0.2008, -1.1431,  2.1523]], device='npu:0')

如果报错，按以下顺序排查：

1. 是否已 source set_env.sh；
2. decorator 等运行时依赖是否安装；
3. CANN 与 torch_npu 版本是否匹配。

4.6 安装 vLLM + vLLM-Ascend

git clone --depth 1 --branch v0.9.1 https://github.com/vllm-project/vllm
cd vllm
VLLM_TARGET_DEVICE=empty pip install -v -e .
cd ..
pip install vllm-ascend==0.9.1rc2

验证 vLLM：

python -c "from vllm import LLM; print('LLM class found:', LLM is not None)"

🔔 注意：如果项目根目录存在 vllm/ 源码文件夹，Python 会把它当作命名空间包优先导入，导致已安装的 vLLM 被遮蔽。解决方式：

mv vllm vllm-source

并确保 transformers 版本兼容：

pip install 'transformers>=4.51.1,<4.53.0'

4.7 安装 Lean 4

curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none

若网络受限，可手动下载 lean-4.9.0-rc1-linux_aarch64.tar.zst 并解压：

mkdir -p ~/.elan/toolchains/leanprover--lean4---v4.9.0-rc1
cd ~/.elan/toolchains/leanprover--lean4---v4.9.0-rc1
tar --zstd -xf /path/to/lean-4.9.0-rc1-linux_aarch64.tar.zst --strip-components=1

添加到 PATH：

export PATH=$HOME/.elan/toolchains/leanprover--lean4---v4.9.0-rc1/bin:$HOME/.elan/bin:$PATH

4.8 构建 mathlib4

cd mathlib4
lake build
cd ..

proofwidgets:optRelease 构建失败不影响证明验证，可忽略。

---

五、下载权重与快速验证

5.1 下载模型权重

git clone https://huggingface.co/Goedel-LM/Goedel-Prover-SFT

或者在魔乐Ascend-AI4S社区下载

git clone https://modelers.cn/Ascend-AI4S/Goedel-Prover.git

本地权重目录结构如下（总大小约 13 GB）：

Goedel-Prover-SFT/
├── config.json
├── generation_config.json
├── model-00001-of-00003.safetensors   # 4.7 GB
├── model-00002-of-00003.safetensors   # 4.7 GB
├── model-00003-of-00003.safetensors   # 3.6 GB
├── model.safetensors.index.json
├── special_tokens_map.json
├── tokenizer.json
├── tokenizer_config.json
└── training_args.bin

5.2 验证 Lean 4 环境

python prover/lean/verifier.py

5.3 单题快速验证

export ASCEND_RT_VISIBLE_DEVICES=2,3
sh eval/eval.sh -i datasets/mathd_algebra_338.jsonl -s test \
    -m Goedel-LM/Goedel-Prover-SFT -o results/mathd_algebra_338/Godel-Prover-SFT \
    -n 32 -g 2 -c 32

验证通过标准：

• results/mathd_algebra_338/Godel-Prover-SFT/compilation_summarize.json 中 accuracy 为 100.00；
• 推理 → 编译 → 汇总三步均正常退出。

5.4 完整 miniF2F 评测

sh eval/eval.sh -i datasets/minif2f.jsonl -s test \
    -m /path/to/model -o results/minif2f/Godel-Prover-SFT \
    -n 32 -g 2 -c 128

---

六、昇腾 NPU 上的实战经验

1. vLLM 源码目录遮蔽
   项目根目录若保留 vllm/ 源码目录，会导致 Python 优先导入本地源码而非已安装的 vLLM 包，出现 LLM 类导入失败。重命名为 vllm-source 即可。

2. transformers 版本
   建议锁定在 4.51.1 ~ 4.52.x 区间，避免与 vLLM 0.9.1 不兼容。

---

七、总结

Goedel-Prover 的出现标志着开源自动定理证明进入了一个新的阶段：

• ✅ 以 7B SFT 模型 击败此前需要 RL 的更大/更复杂系统；
• ✅ 通过 大规模数据合成与迭代证明，有效缓解了形式化数据稀缺问题；
• ✅ 完全开源，包括代码、模型、数据集和数万条 Lean 4 证明；
• ✅ 在昇腾 NPU 生态中已有社区迁移实践，降低了国产算力上的落地门槛。

无论你是做形式化数学、自动推理，还是关注大模型在严谨逻辑任务上的能力边界，Goedel-Prover 都值得深入研究和复现。

---

八、参考资料

• 📄 论文：Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
• 💻 GitHub：Goedel-LM/Goedel-Prover
• 🤗 模型：Goedel-LM/Goedel-Prover-SFT
• 🌐 主页：https://goedel-lm.github.io/
• 📦 昇腾迁移技能：AI4Science/AscendSkills/models/goedel-prover/SKILL.md

---

如果本文对你有帮助，欢迎点赞、收藏、转发。有任何环境搭建或推理问题，欢迎在评论区交流！ 🚀