MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlassis Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Mohamed, Bilal Aytekin, Jiewen Lang, Zezheng Song, Furong Huang
cs.CL, cs.AI, cs.LO
2026-08-26
马里兰团队发布诊断基准 MathAdv：321 道本研级题、13 个领域、298 条 Lean 4 陈述。最强 Goedel-Prover-V2 证明正确率 21.88%；GPT-5.4 选择题 82.88%、Lean 仅 10.62%。30 道等价改写上，模型更常只会做原题。
现有形式化数学基准大多只报一个数字：Lean 证明过了没有。过不了，分不清是缺知识、推理断了，还是不会写成内核认的证明。覆盖也窄。MiniF2F、PutnamBench 一类高度集中在竞赛代数和数论，拓扑、傅里叶分析、泛函这些本研级课几乎看不见。每道题还锁死在一种表述上，过关可能只是熟题面，换个写法就不知道还剩多少。
马里兰大学学院公园分校领衔，佐治亚理工和康奈尔参与，做了诊断基准 MathAdv。321 道本科到研究生级题目，横跨数论、线性代数、抽象代数、微积分、实分析、复分析、傅里叶分析、泛函分析、概率、拓扑、几何、组合、逻辑这 13 个领域。其中 298 道写成 Lean 4 陈述，另 23 道因为 Mathlib 缺定义，先留着只做辅助评测。每道题最多配三种辅助：81 道填空（论文里叫 direct-answer，考自然语言解题）、293 道选择题（考该用哪条定理或策略）、30 道专家手改的等价变体（数学不变，题面大改）。
题目来自教材和领域专家。贡献者都是相关方向的博士生，第二位专家独立复核题面和辅助题。一个概率题的选择题会问「可选停止定理还是 Doob 分解」；一道实分析原题把凸组合写开，改写版改口说「包含该点集的最小凸集」，认得出是同一件事才算真会。
形式化走人工在环流水线。大模型先起草 Lean 陈述，编译器报错打回去，改到能 type-check；再由另一套模型和一位专家核语义是不是原题；最后第二位专家终审。流水线不把模型当作「这代码能不能编过」的裁判。用 James Hanson 的 Lean 4 junk theorems（能编译、读起来却像胡话的片段）测过：gpt-5.5 判断能否编译只有 58%，两个 DeepSeek 变体只有 4%，但 deepseek-v4-pro 对语义理解能打到 1.91/2。编译判断交给 Lean，语义对齐交给模型和人。
Mathlib 缺口是硬约束。附录举了 Petersen 的黎曼几何题，截面曲率、测地球、Bishop-Gromov 不等式都还没入库，忠实翻译等于先修一整块库，这批就推迟。
评测分两类证明系统。逐步生成加搜索的有 InternLM2-Math-Plus-7B、InternLM2.5-StepProver、DeepSeek-Prover-V1.5-RL + RMaxTS、MA-LoT 挂 DeepSeek 或 Goedel、Goedel-Prover-V2-32B。整篇生成的有 Goedel-Prover-SFT/DPO 和 DeepSeek-Prover-V1.5 的 Base/SFT/RL。通用模型测了 GPT-5.4、DeepSeek-V3.2、DeepSeek-R1。计算预算不对齐：DeepSeek-Prover-V1.5 系列是 pass@128，Goedel-Prover-V2 是 pass@32 再加两轮自我修正，GPT-5.4 是 pass@32，DeepSeek-R1 是 pass@16。主表数字不能当成同等算力对比。
Lean 4 证明主表最高是 Goedel-Prover-V2 的 21.88%，其次是 DeepSeek-Prover-V1.5 RL + RMaxTS 的 16.56%。专用训练和搜索有用，天花板仍低。同一条 DeepSeek-Prover-V1.5 线，Base 1.25%，RL 11.25%，加上 RMaxTS 到 16.56%。GPT-5.4 为 10.62%，DeepSeek-R1 为 10.94%，DeepSeek-V3.2 为 5.31%。附录里 Goedel-Prover-V2 在数论 70.0%（7/10）、线性代数 65.0%（13/20），拓扑为 0%；论文写所有模型在拓扑上都是 0%。
| 模型 | Lean 证明 | 填空 DA | 选择题 MC |
| Goedel-Prover-V2 | 21.88% | 未报 | 未报 |
| DeepSeek-Prover-V1.5 RL+RMaxTS | 16.56% | 42.0% | 38.70% |
| InternLM2-Math-Plus-7B | 13.12% | 39.5% | 64.04% |
| GPT-5.4 | 10.62% | 64.2% | 82.88% |
| DeepSeek-V3.2 | 5.31% | 66.7% | 75.00% |
| Goedel-Prover-SFT | 10.62% | 4.9% | 21.23% |
通用模型会做题、会选题，写不出 Lean。Goedel-Prover 走反：SFT 和 DPO 填空都只有 4.9%，证明却到 10.62% 和 11.25%，专精在 tactic 搜索，自然语言答题反而弱。
30 道等价改写只记次数。Goedel-Prover-V2 原题会、改写不会的有 6 道，反过来 0 道；DeepSeek-R1 是 4 对 0。多数模型都是「只会做原题」多于「只会做改写」。绝对数量小，方向一致。
把 Lean 报错回灌进 prompt、同样预算 K=16×3 时，DeepSeek-V3.2 从 5.00% 升到 7.50%，GPT-5.4 从 9.06% 升到 13.75%。交互改掉不少语法错，剩下的是论证构造。GPT-5.4 会堆不必要的中间命题，短证明被拒就改成长证明。把选择题的正确策略当成自然语言提示塞进证明 prompt，帮的是通用模型，伤的是专用证明器：两个 DeepSeek 通用模型上升，Goedel-Prover-SFT/DPO 掉点。论文没有把 Figure 5 的精确百分点制成表。
失败常见四类：证了一半当完、tactic 用错（该整除性却上线性算术）、幻觉不存在的 Mathlib 引理、同一条命令空转。成功的要么命中现成引理，要么用 have 把步骤拆开，要么一展开定义题就变简单。
对做形式化证明的人，MathAdv 把「正确率低」拆开了：多数通用模型卡在形式化，不卡在知不知道用哪条定理。给通用模型塞自然语言提示可能有用，给 Goedel 这类专用器塞同样的提示可能帮倒忙。交互 Lean 反馈值得做，但别指望它自动长出干净证明。
对评测的人，只报竞赛基准总分会漏掉领域偏科和表述过拟合。拓扑全 0、数论和线代偏高，和竞赛语料、Mathlib 覆盖叠在一起。30 道改写不够当主榜，方向已经够用来当熟题面检查。
这是诊断基准，不是新证明算法。评测设计上的增量是同一批题拆成知识、推理、形式化、鲁棒性四块。
作者自己写了两条：题量小，专家成本高；Mathlib 覆盖不够，23 道还没形式化。
另外几处论文没摊开。主表各模型采样预算差一截，Goedel-Prover-V2 的 21.88% 和 GPT-5.4 的 10.62% 不能直接比谁更强。附录分母对不齐：有的表总体写 320，正文写 298 条已形式化；拓扑有的表 28 道、有的表 8 道。改写只有 30 道，Table 3 是个位数计数，统计上很脆。Figure 5 的提示实验没有表内数字，只说升和降。选择题问的是「哪条定理最有用」，不是证明本身，GPT-5.4 的 82.88% 测的是策略检索。题目来自公开教材，污染风险在，改写集就是为这个设的，但 30 道盖不住 321 道。