# 在极简形式主义下通过证明对LLM推理能力的压力测试

- 来源：HuggingFace Daily Papers（社区热门论文）
- 发布时间：2026-04-07 08:00
- AIHOT 分数：72
- AIHOT 标记：精选
- AIHOT 链接：https://aihot.news/items/cmpbk87rm181wslnzz0ejlk26
- 原文链接：https://arxiv.org/abs/2605.12524

## 精选理由

不再只看答案对不对，而是让机器一步步检查证明，ProofGrid 戳中了 LLM 推理的一个盲区，很多模型产出的证明连自己都不信，这个发现挺要命的。

## AI 摘要

本研究推出了名为ProofGrid的基准测试套件，旨在通过机器可检查的证明，而非仅凭最终答案，来严格评估大语言模型（LLM）的推理能力。该套件包含15项任务，涵盖证明编写、验证等环节，核心采用紧凑的最小自然演绎语言（NDL）进行表述。其评估框架能容忍表面偏差并定位首个实质性推理错误，实现了机械化、可复现的细粒度验证。测试表明，前沿模型在基础任务上表现尚可，但在需要全局组合推理或底层证明合成的困难任务上仍存在显著局限。研究还识别并量化了模型“生成有缺陷证明却能在局部正确识别其错误”的“认识不稳定”现象。

## 正文

我们提出 ProofGrid，这是一个通过机器可验证的证明（而非仅凭最终答案）来评估大语言模型推理能力的基准测试套件。ProofGrid 包含 15 项任务，涵盖证明编写、证明检查、证明掩码和证明补全。任务采用极简形式化符号表示，特别是 NDL，这是一种紧凑的自然演绎语言，适合放入短提示词中，并支持精确、可审计的验证。

这带来了机械化、可复现且细粒度的评估，而非依赖人类或大语言模型的判断。ProofGrid 覆盖了校准后的难度谱系，从基础推理测试到结构丰富的挑战性任务（当前尚无模型能解决），同时最小化对领域知识、求解器委托和长上下文伪影的依赖。

我们还开发了一个推理基准比较框架，并用它从表示能力、验证保证和推理深度等方面，将 ProofGrid 与现有工作进行对比。在方法论上，我们引入了一条带检测的证明检查流水线，它能容忍细微的表面偏差，同时定位首次实质性推理失败的位置，从而提升测量分辨率，并将证明规划与低层执行噪声分离开来。

利用这条流水线，我们评估了广泛的开源和闭源模型。结果显示进展迅速，但仍有显著局限：前沿模型在多项基础任务上表现良好，但困难任务——尤其是那些需要全局组合推理或低层证明合成的任务——仍远未解决。我们还发现了认知不稳定性，即模型能生成有缺陷的证明，却又能在孤立情况下正确否定这些局部推理，我们通过认知稳定性指数对此进行了形式化。

最后，我们使用 2PL IRT 分析、Wright 图以及基于 Fisher 信息的归一化任务区分度指标，对准确率进行了补充。