用极简形式化证明对 LLM 推理能力进行压力测试 Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism

完整的 PROOFGRID 评测流水线包含如下步骤。步骤一 (语言形式化)：使用 BNF 在提示中给出 NDL 的全部语法，包括 atomic 公式 (A、B、C、E、F、…)、复合公式 (parenthesized infix，如 $(A\Rightarrow B)$、$(\sim A)$、$(A\&B)$、$(A|B)$、$(A\Leftrightarrow B)$) 和四种证明结构 (axiom instantiation / inference application / assume block / composite sequence)，并显式规定合取右结合 (conjunction associates to the right) 等关键约定。步骤二 (数据生成)：对 PL1-PW (400 题)，随机选取 2-7 个命题变元，先用算法构造 200 道带前提的题目，再用“条件化 (conditionalization)” 流程把另外 200 道转成无前提的蕴涵式以增加多样性，最终使中位变元数 3、75 分位数 3；对 PL2-PW (200 题)，将任意命题公式 $p$ 经 Ab 算法 (电路化的模型诊断转换) 包装为 $T\cup\{p, \neg G_{root}\} \vdash \bigvee_v \neg N_v$ 形态，其中 $N_v$、$G_v$ 是为每个 AST 节点引入的 normality / gate-output 原子，使问题结构化且难度可控；对 PL3-PW (300 题)，分 8 个家族生成：10 道 DAG 金字塔 pebbling (高度至 10)、5 道计数原理 (partition)、30 道相对化鸽巢、60 道 Tseitin 公式、70 道子集基数、70 道 3-着色、15 道 De Bruijn、40 道简单 DAG pebbling，对每个家族用 cnfgen、networkx 或随机 CNF 生成器并用 Prover9/Vampire/Spass 验证可解性 (证明长度 <300 步) 且大部分 CNF 子句数 <100；对 PL4-PW (200 题)，把 PL1 的简单题改写为仅用否定与蕴涵的 Hilbert 演算形式 (3 个公理 + modus ponens)；对 EQ1 (1000 题)，用 $f, f_1, \ldots, g, g_1, \ldots, h, h_1, \ldots, r, r_1, \ldots$ 等函数符号和 $a, b, c, d, e$ 常量随机生成等式公理 $E_i$ 与短等式链。步骤三 (证明评分)：把模型输出送入 instrumented proof checker；先做语法修复 (自动补缺失的 `}`、调整括号、把 square bracket 替换为 round、修复 `assume I \{` 这种“忘了写公式”的常见误用)；再做语义修复 (双否消除、合取/析取交换、left-and/right-and 互换等 24 种常用小错误)；最后逐行评估，对每一步用 SAT 求解器 (在 NDL0 中) 或 Athena 模式匹配 (在 NDL 中) 验证结论是否从当前假设基 (assumption base) 合法推出，遇到无法自动修复的逻辑错误就报告为“first error”并终止评估。步骤四 (多维分析)：基于每模型的逐题结果计算 DI (Gini mean difference)、ESI (把单个推理步骤是否被模型自己认作 invalid 作为 $D_1$、把完整证明作为 $D_2$，再代入对数变换 $ESI = 1 - |Inc_{D_1}[D_2]|/|D_2| / \log(1+\gamma)$ 中，$\gamma=5$)，并对每个任务在 2PL IRT 下拟合 item 参数 $(a_i, b_i)$，据此计算题目的 Fisher 信息量 $I_i(\theta)$。步骤五 (误差归类)：把每个模型在每个任务上的第一次错误归入 6 类 (parsing/syntax, not-in-assumption-base, malformed-rule-application, malformed-assumption, wrong-conclusion, unbound-identifier) 或 5 类 (Type-1 至 Type-5，PL1-PC)，并报告每类错误在 24 模型上的分布，作为诊断报告。

从技术新颖性看，本文的贡献不在于提出某一种新算法或新网络结构，而在于把“推理评测”这件事系统地变成一种形式化诊断过程。具体新颖性可分四点。第一，instrumented proof checker 的“修理 + 报告”双阶段设计：这是形式化证明检查文献中少见的精细化思路，能在不牺牲严谨性的前提下显著提升评估的分辨率 (在 PL1-PW 上平均提升 19 个绝对百分点)。第二，proof masking (证明掩码) 和 proof gap-filling (证明填空) 是作者新设计的两类元推理任务：masking 把 NDL 证明中的结论、规则名、假设和参数随机掩去 30%-90%，要求模型在不重新规划整篇证明的前提下推理“如何填补”；gap-filling 把子证明层次整段挖空，让模型做逆向搜索 (inverse planning) 来还原原始证人的意图。这种任务在 Lean 系 benchmark 中几乎不存在。第三，ESI 形式化：把“epistemic stability”从“直觉性抱怨”提升为可计算指标——把 $D_1$ 设为模型对单个推理步骤做出的独立判断 (例如“$A$ 是否 follow from $(A|B)$”)，把 $D_2$ 设为该模型在多步证明中是否真的如此行事的整体行为，通过两者的“不相容比例”量化跨任务一致性，并用对数变换防止线性度量在尾部过平。第四，多层 taxonomy 与结构化诊断：作者把 33 个常用推理 benchmark 沿 6 个维度 (输入形式、输出形式、内容依赖、形式系统表达力、推理机制多样性、任务多样性) 分类，把 PROOFGRID 放在一个二维雷达图 (Fig. 1) 中凸显其独一无二的“低表达力 + 高结构化 + 机器可验证 + 未饱和”四元组合，论证其作为下一代推理基准的合理性。

本文作为方法论文，弱点主要不在技术设计，而在覆盖广度与可重复性。具体可分四点。弱点一：任务分布的“西方中心”偏向——所有 PL3 例子都来自西方数学与计算机科学传统 (鸽巢、图着色、De Bruijn)，缺乏非西方数学传统 (例如中国剩余定理、日历推算) 的样本，可能在文化公平的层面上不够中立。改进方向是引入非西方数学背景的问题族，并保证这些家族对训练语料同样陌生。弱点二：仪器化检查器的“修理清单”是手工编纂的，包含 24 类常见语义错误 (双否消除、合取交换等)，这相当于在 NDL 之上加了一层“影子语法”，可能掩盖那些未列入清单的错误类型。改进方向是采用随机器习 (reinfocement learning) 自动从模型错误分布中归纳出可修复错误集，并动态更新。弱点三：24 个模型的评测时间窗跨越约 1 年，模型的快照 (例如 deepseek-r1-0528 vs deepseek-reasoner) 间存在 checkpoint 漂移，难以严格控制“是否同一架构同一预训练”。改进方向是固定 inference 版本与 API 端点，并对所有模型做同时段的横向快照测试。弱点四：ESI 对“独立判断”使用同一个模型的另一个 prompt 回答，这一 self-recognition 实验容易受 prompt 措辞影响。改进方向是 (a) 用零样本 (zero-shot) 与少样本 (few-shot) 各做一遍取平均，(b) 用不同的提问顺序 (先 yes/no 再 counterexample) 做 permutation test 来检验稳健性。

作者在第 10 节与第 9.2 节明确提出四个有价值的未来方向。第一，把 Hilbert 演算任务与“deduction theorem”策略结合：让模型先解“有前提”的版本，再机械地 discharge 前提得到无前提的纯 Hilbert 证明。这能更精细地分离“高层策略”与“低层公理匹配”能力。第二，扩展到一阶逻辑与依赖类型论：PROOFGRID 目前只覆盖命题逻辑与无解释的等式逻辑，未来应加入 FOL 片段、模态逻辑、时序逻辑等更丰富的形式系统。第三，引入 calibrate-aware training：论文在 EQ-GF 任务上展示了 ECE 在所有 24 个模型上系统性 over-confidence (Gemini 2.5 Pro 的 ECE 高达 0.4+)，且 worst bins 集中在高置信区间 (L4、L5)——这意味着基于置信度的 self-correction 阈值并不可靠，未来应通过 confidence supervision 或 rejection-aware RL 来显式校准。第四，扩展到 agentic 协作场景：作者在 PL2-PW 部分观察到 o3 “失败-快速” (空字符串) 与 Mistral Magistral “失败-冗长” (无限延长) 的鲜明对比，提示未来的训练可以让模型学会在“不确定”时显式调用 $\text{force/sorry/Admitted}$ 之类的占位符，把未完成的证明外包给其他 agent。

PROOFGRID 的可复现性较好。数据生成算法在附录 C 中以伪代码形式给出 (Section C.1 详述 PL1-PW 的随机构造流程)，每个数据集的统计特征 (前提数、AST 大小、变元数) 都在论文中以 inline box-sparkline 形式给出 (例如 Table 2 的 9 行)，所有任务的 prompt 模板在论文主体或附录中有完整示例，instrumented proof checker 基于开源的 Athena 系统实现。论文也坦承评测在 wall-clock 上有 30 分钟的 timeout，且对 API 错误做了 retry 一次的策略；这些细节虽未在主文展开，但附录 C 给出。难度方面，复现工作涉及 (1) 用 cnfgen 重新生成 PL3 题目 (中等难度)；(2) 部署 NDL/Athena proof checker (开源，但配置较多)；(3) 跑 24 个模型的 API 调用 (需要相当的预算，论文未披露具体成本)；(4) 实现 IRT、DI、ESI、ECE 等统计量 (代码量适中，附录 B 给出了 IRT 拟合算法)。最大的不可复现因素是：模型 API 的版本可能已经更新 (例如 GPT-5.2 → GPT-5.4)，导致论文中的具体数字会与读者复现出的数字有出入。论文也明确建议把这些数字视为“快照”而非永恒真理。