Star11
13
代码
代码
Issues3
Pull Requests2
项目讨论
Wiki
分析
Star11
13
已开启
upload Goedel-Prover #15
xiaolingling_8909创建于 7月23日
upload Goedel-Prover #15
已开启
xiaolingling_8909创建于 7月23日
从xiaolingling_8909/LifeScience_xllmain合入到AI4Science/LifeSciencemain
共 3 个文件变更+240-0
APyTorch/Goedel-Prover/README.md+155-0
@@ -0,0 +1,155 @@
1+---
2+license: mit
3+---
4+ 
5+# 概述
6+ 
7+Goedel-Prover 是一个开源的大语言模型（LLM），在数学问题自动形式化证明生成领域达到了领先水平（SOTA）。该领域的关键挑战在于形式化数学语句和证明数据的稀缺性，Goedel-Prover 通过以下方式解决了这一问题：
8+ 
9+首先，训练语句形式化器（statement formalizers），将 Numina 数据集中的自然语言数学问题翻译为形式化语言（Lean 4），创建了一个包含 164 万条形式化语句的数据集。在此过程中，使用 LLM 来检查形式化语句是否准确保留了原始自然语言问题的内容。
10+ 
11+然后，通过训练一系列证明器（provers），迭代地构建了一个大规模形式化证明数据集。每个证明器都能成功证明前一个证明器无法解决的许多问题，这些新证明被添加到下一个证明器的训练集中。
12+ 
13+最终证明器在全证明生成（whole-proof generation）方面超越了所有现有的开源模型。在 miniF2F 基准测试上，达到了 **57.6%** 的成功率（Pass@32），比此前最佳开源模型高出 7.6%。在 PutnamBench 上，Goedel-Prover 成功解决了 **7 个问题**（Pass@512），在排行榜上排名第一。此外，为 Lean Workbook 问题生成了 29.7K 条形式化证明，几乎是此前工作（15.7K）的两倍。
14+ 
15+- 参考实现：
16+ 
17+ ```shell
18+ url=https://github.com/Goedel-LM/Goedel-Prover.git
19+ ```
20+ 
21+- 适配昇腾 AI 处理器的实现：
22+ 
23+ ```shell
24+ url=https://gitcode.com/AI4Science/LifeScience.git
25+ code_path=PyTorch/Goedel-Prover
26+ ```
27+ 
28+#### 组件版本
29+ 
30+```shell
31+hdk：25.3.rc1.2
32+cann：8.3.RC1
33+python：3.10
34+torch：2.5.1
35+torch-npu：2.5.1
36+```
37+ 
38+#### 拉取仓库
39+ 
40+```shell
41+git clone https://gitcode.com/AI4Science/LifeScience.git
42+cd LifeScience/PyTorch/Goedel-Prover
43+git clone --recurse-submodules https://github.com/Goedel-LM/Goedel-Prover.git
44+cd Goedel-Prover
45+```
46+ 
47+#### 环境准备
48+ 
49+1. 新建conda环境
50+```shell
51+conda create -n goedel-prover python=3.10 -y
52+conda activate goedel-prover
53+```
54+ 
55+2. 安装依赖
56+```shell
57+export PIP_INDEX_URL=https://repo.huaweicloud.com/repository/pypi/simple/
58+pip install -r requirements.txt
59+```
60+ 
61+3. 验证 PyTorch 与 torch_npu 安装
62+执行以下命令检查安装是否成功：
63+```shell
64+python3 -c "import torch;import torch_npu; a = torch.randn(3, 4).npu(); print(a + a);"
65+```
66+若输出类似以下信息，说明安装成功：
67+```
68+tensor([[-0.6066, 6.3385, 0.0379, 3.3356],
69+ [ 2.9243, 3.3134, -1.5465, 0.1916],
70+ [-2.1807, 0.2008, -1.1431, 2.1523]], device='npu:0')
71+```
72+若报错，排查顺序：
73+ - set_env.sh 是否已 source
74+ - decorator 等运行时依赖是否安装
75+ - CANN 与 torch_npu 版本是否匹配
76+ 
77+4. 安装 vLLM + vLLM-Ascend
78+```shell
79+git clone --depth 1 --branch v0.9.1 https://github.com/vllm-project/vllm
80+cd vllm
81+VLLM_TARGET_DEVICE=empty pip install -v -e .
82+cd ..
83+pip install vllm-ascend==0.9.1rc2
84+```
85+ 
86+- 验证vllm是否安装
87+```shell
88+python -c "from vllm import LLM; print('LLM class found:', LLM is not None)"
89+```
90+若项目根目录存在 vllm/ 源码仓库文件夹，Python 把它当作命名空间包优先导入，遮蔽了真正以 editable 方式安装在 vllm/vllm/ 下的包，导致vllm导包失败，需要该 vllm 源码仓库目录重命名，消除遮蔽。
91+```shell
92+cd Goedel-Prover && mv vllm vllm-source
93+```
94+ 
95+- 安装后确认 transformers 版本兼容：
96+```shell
97+pip install 'transformers>=4.51.1,<4.53.0'
98+```
99+ 
100+5. 安装 Lean 4
101+下载 elan（Lean 版本管理器）：
102+```shell
103+curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
104+```
105+ 
106+手动安装 Lean 4 toolchain（如网络受限，可手动下载 lean-4.9.0-rc1-linux_aarch64.tar.zst）：
107+```shell
108+mkdir -p ~/.elan/toolchains/leanprover--lean4---v4.9.0-rc1
109+cd ~/.elan/toolchains/leanprover--lean4---v4.9.0-rc1
110+tar --zstd -xf /path/to/lean-4.9.0-rc1-linux_aarch64.tar.zst --strip-components=1
111+```
112+ 
113+添加到 PATH：
114+```shell
115+export PATH=$HOME/.elan/toolchains/leanprover--lean4---v4.9.0-rc1/bin:$HOME/.elan/bin:$PATH
116+```
117+ 
118+#### 构建 mathlib4
119+```shell
120+cd mathlib4
121+lake build
122+cd ..
123+```
124+proofwidgets:optRelease 构建失败不影响证明验证，可忽略。
125+ 
126+#### 权重下载
127+```shell
128+git clone https://huggingface.co/Goedel-LM/Goedel-Prover-SFT
129+```
130+ 
131+#### 验证
132+验证 Lean 4 环境：
133+```shell
134+python prover/lean/verifier.py
135+```
136+ 
137+使用单题快速验证（NPU 卡号按需调整）：
138+```shell
139+export ASCEND_RT_VISIBLE_DEVICES=2,3
140+sh eval/eval.sh -i datasets/mathd_algebra_338.jsonl -s test \
141+ -m Goedel-LM/Goedel-Prover-SFT -o results/mathd_algebra_338/Godel-Prover-SFT \
142+ -n 32 -g 2 -c 32
143+```
144+ 
145+验证通过标准：
146+ 
147+- results/mathd_algebra_338/Godel-Prover-SFT/compilation_summarize.json 中 accuracy 为 100.00
148+- 三步（推理 → 编译 → 汇总）均正常退出
149+ 
150+完整 miniF2F 评测：
151+```shell
152+sh eval/eval.sh -i datasets/minif2f.jsonl -s test \
153+ -m /path/to/model -o results/minif2f/Godel-Prover-SFT \
154+ -n 32 -g 2 -c 128
155+```
APyTorch/Goedel-Prover/patch/Goedel-Prover.patch+66-0
@@ -0,0 +1,66 @@
1+diff --git a/eval/eval.sh b/eval/eval.sh
2+index 7c0863c..d1b0969 100644
3+--- a/eval/eval.sh
4++++ b/eval/eval.sh
5+@@ -1,3 +1,10 @@
6++source /usr/local/Ascend/ascend-toolkit/set_env.sh
7++source /usr/local/Ascend/nnal/atb/set_env.sh --cxx_abi=0
8++source /usr/local/Ascend/nnal/asdsip/set_env.sh
9++
10++export LD_LIBRARY_PATH=/usr/local/Ascend/driver/lib64/driver:/usr/local/Ascend/driver/lib64/common:/usr/local/Ascend/driver/lib64:$LD_LIBRARY_PATH
11++
12++export PYTHONPATH=$(python -c "import torch_npu; import os; print(os.path.join(os.path.dirname(torch_npu.__file__), 'dynamo'))"):$PYTHONPATH
13+ INPUT_PATH=datasets/minif2f.jsonl
14+ MODEL_PATH=Goedel-LM/Goedel-Prover-SFT
15+ OUTPUT_DIR=results/minif2f/Godel-Prover-SFT
16+@@ -33,4 +40,3 @@ python -m eval.step2_compile --input_path $INPUT_FILE --output_path $COMPILE_OUT
17+
18+ SUMMARIZE_OUTPUT_PATH=${OUTPUT_DIR}/compilation_summarize.json
19+ python -m eval.step3_summarize_compile --input_path $COMPILE_OUTPUT_PATH --output_path $SUMMARIZE_OUTPUT_PATH --field ${FIELD}
20+-
21+diff --git a/eval/step1_inference.py b/eval/step1_inference.py
22+index ba6b449..17d299c 100644
23+--- a/eval/step1_inference.py
24++++ b/eval/step1_inference.py
25+@@ -1,7 +1,9 @@
26+ import re
27+ from transformers import AutoTokenizer
28+ from vllm import LLM, SamplingParams
29+-
30++import torch
31++import torch_npu
32++from torch_npu.contrib import transfer_to_npu
33+ import json
34+ import argparse
35+
36+diff --git a/requirements.txt b/requirements.txt
37+index 10c89e4..8fdb2f2 100644
38+--- a/requirements.txt
39++++ b/requirements.txt
40+@@ -1,13 +1,19 @@
41++setuptools<71
42++torch==2.5.1
43++torch_npu==2.5.1.post1
44+ pytz==2022.1
45+ termcolor==2.4.0
46+ easydict==1.13
47+ tabulate==0.9.0
48+ transformers==4.46.1
49+-torch==2.4.0
50+-torchvision==0.19.0
51+ numpy==1.26.4
52+ pandas==1.4.3
53+ accelerate==0.33.0
54+-flash-attn==2.6.3
55+-vllm==0.6.3.post1
56+-vllm_nccl_cu12==2.18.1.0.4.0
57+ 
58++decorator
59++attrs
60++psutil
61++absl-py
62++cloudpickle
63++ml-dtypes
64++scipy
65++tornado
66+ 
APyTorch/Goedel-Prover/requirements.txt+19-0
@@ -0,0 +1,19 @@
1+setuptools<71
2+torch==2.5.1
3+torch_npu==2.5.1.post1
4+pytz==2022.1
5+termcolor==2.4.0
6+easydict==1.13
7+tabulate==0.9.0
8+transformers==4.46.1
9+numpy==1.26.4
10+pandas==1.4.3
11+accelerate==0.33.0
12+decorator
13+attrs
14+psutil
15+absl-py
16+cloudpickle
17+ml-dtypes
18+scipy
19+tornado