数学能力评测一直是大模型能力评估的核心环节。从GSM8K到MATH，再到更具挑战性的竞赛级数学基准，社区投入了大量精力构建评测集。然而一个容易被忽视的问题是：答案对了，过程就一定对吗？大量的实践案例表明，模型完全可能通过错误的推导链条碰巧得到正确答案，也可能因为格式问题丢失正确答案。传统的最终答案匹配评测方式，无法回答“推理步骤是否正确”这个更本质的问题，这就是数学基准评测中的步骤难评问题。本文将从问题根源、自动验证方案、形式化证明路线三个角度展开讨论。
一、为什么最终答案匹配会失真
绝大多数数学基准采用的标准评测流程是：把模型输出的最终答案抽取出来，与标注答案做字符串或数值比对。这个流程实现简单，但存在两类系统性误差。第一类是假阳性，即答案正确但过程错误。研究者在分析模型输出时发现，某些模型会先通过错误的代数变形得到一个中间结果，再在后续步骤中恰好又犯了一次符号错误，两次错误相互抵消，最终答案反而是对的。这种情况在选择题和填空题上尤其常见，因为答案空间小，猜中或错中正确答案的概率并不低。
第二类是假阴性，即过程正确但被判错。常见原因包括答案格式不统一，比如模型输出“二分之一”而标注是“1/2”，模型输出“x=3或x=-3”而标注只写了“3, -3”，或者模型用了等价但形式不同的表达式。简单的字符串匹配无法处理这些等价性判断，于是评测代码里堆满了各种正则特判，越写越脆弱。
一个改进思路是引入符号计算库做答案等价性判定，例如用SymPy判断两个表达式是否数学等价：
from sympy import simplify, Rational
from sympy.parsing.latex import parse_latex
def answers_equal(pred: str, gold: str) -> bool:
try:
# 尝试按LaTeX解析，失败则按普通表达式解析
try:
p = parse_latex(pred)
g = parse_latex(gold)
except Exception:
from sympy import sympify
p = sympify(pred)
g = sympify(gold)
# 数值等价检查兜底
diff = simplify(p - g)
return diff == 0
except Exception:
# 无法解析时退回字符串归一化比较
return pred.strip() == gold.strip()
print(answers_equal("\\frac{1}{2}", "0.5")) # True这种方式能缓解假阴性问题，但对假阳性无能为力——它依然只看结果。要真正评估步骤质量，必须让评测器能读懂推理过程本身。
二、用大模型做自动过程验证器
既然人肉检查每一步推理不现实，一个自然的想法是用另一个大模型充当裁判，逐步检查推理链。这就是基于LLM的自动验证方案。具体做法是：先要求被评测模型输出结构化的分步解题过程，每一步带上编号和依据；再由验证模型逐步审查，判断该步是否由前文有效推出，最后汇总出步骤级的正确率。
构建提示词时，关键是给验证模型明确的审查标准和输出格式，避免它自己发散。一个实用的提示模板如下：
你是一名严格的数学审题员。给定一道题目和模型的分步解答，
请逐步审查：
1. 该步使用的公式或定理是否正确引用；
2. 该步的计算是否准确；
3. 该步是否逻辑上依赖前一步的结论；
4. 是否存在跳步（省略了关键推导）。
对每一步输出JSON：
{"step": 步骤编号, "verdict": "correct|wrong|skipped", "reason": "简短理由"}
题目：{question}
分步解答：{solution}这种方案的成本需要注意。一道题的解答可能有二三十步，每步都要调用一次验证模型，加上多数投票（例如对每步验证三次取多数），开销会成倍增长。工程上通常做两级过滤：先用轻量规则筛掉明显正确的计算步，比如可以重放验算的算术运算，只把逻辑推理步和定理引用步交给LLM审查，能显著降低成本。另外，验证模型自身的偏差也要处理，它可能对格式漂亮的步骤更宽容，因此最好准备一个人工标注的小型校准集，定期测量验证器与人类判断的一致率。
自动验证器的优势是通用性强，任何自然语言形式的推理都能审；劣势则是它本身会出错，本质上是用一个不确定的系统去评另一个不确定的系统，只能逼近而不能保证结论可靠。要获得严格的保证，就需要进入形式化世界。
三、形式化证明：可机器校验的数学推理评测
形式化证明工具如Lean、Coq、Isabelle，能够把数学命题和证明表示为计算机可检查的形式语言。证明检查器是确定性程序，一个证明要么通过检查要么不通过，没有模糊空间。这就是所谓的过程可验证（process-verifiable）评测：我们不再问模型答案是什么，而是要求模型产出一个完整的、机器可校验的证明。只要证明通过检查器验证，中间每一步的正确性就得到了数学层面的保证，从根本上消灭了假阳性。
以Lean 4为例，假设评测目标是证明一个简单的不等式，模型需要输出如下形式的证明文本：
theorem eval_test (a b : ℤ) (ha : 0 < a) (hb : 0 < b) :
0 < a * b := by
-- 每一步都必须通过Lean内核检查
apply Int.mul_pos ha hb评测系统只需要调用Lean编译器检查这段证明是否通过，通过则记为解决，不通过则记为失败。整个判分过程无需任何人工介入，也不依赖另一个模型的判断。基于这一思路，社区已经构建了miniF2F这样的形式化数学基准，收录了竞赛数学中的代数、数论、不等式问题，专门用于评测模型的形式化推理能力。
形式化路线的代价在于生态和表达难度。其一，大量现成的数学题库是自然语言形式的，要转写成Lean命题本身就需要专家劳动，这也是为什么形式化基准的题目规模远小于GSM8K这类数据集。其二，对被评测模型的要求陡然提高，模型不仅要会解题，还要掌握Lean的证明语法和数学库API，普通对话模型直接上场成绩会非常低。其三，证明搜索空间巨大，工程上通常把Lean环境包装成一个可交互的执行环境，让模型多轮尝试、根据编译错误反馈修正证明，这就把评测问题转化成了带工具调用的智能体评测问题。目前主流做法是用LeanDojo、lean-gym这类框架提供程序化的证明交互接口，配合搜索算法在证明树中探索。
四、构建混合评测流水线的实践建议
综合来看，三种手段各有适用场景：答案等价判定适合大规模初筛，成本低、覆盖广；LLM过程验证适合分析模型弱项，能定位到具体出错步骤，但结论是概率性的；形式化证明适合严格结论和小规模深度评测，能给出可复现的硬性指标。实际搭建评测系统时，推荐按漏斗结构组织：先用SymPy等价判定过滤出答案正确的样本，再用LLM验证器对这些样本做步骤审查，识别假阳性；对关键能力项，额外准备一个形式化子集，用Lean检查器做金标准校验。三类结果分别汇报，避免用一个单一分数掩盖评测方式的差异。
另外有几点工程细节值得注意。抽取最终答案时要针对模型的输出格式写适配器，不同模型的答案标记方式差异很大，建议在评测配置里显式声明答案抽取规则而不是硬编码。验证模型的一致性要定期用人工标注集校准，一旦发现验证器漂移，需要更新提示词或更换模型版本。形式化评测要注意Lean版本和数学库版本的锁定，同一个证明在不同mathlib版本下可能编译结果不同，版本不锁定的形式化分数没有可比性。把这些问题处理好，步骤级评测才能真正从“看起来合理”走向“经得起复查”。