我们提出 ProofGrid，这是一个通过机器可验证的证明（而非仅凭最终答案）来评估大语言模型推理能力的基准测试套件。ProofGrid 包含 15 项任务，涵盖证明编写、证明检查、证明掩码和证明补全。任务采用极简形式化符号表示，特别是 NDL，这是一种紧凑的自然演绎语言，适合放入短提示词中，并支持精确、可审计的验证。
这带来了机械化、可复现且细粒度的评估，而非依赖人类或大语言模型的判断。ProofGrid 覆盖了校准后的难度谱系，从基础推理测试到结构丰富的挑战性任务（当前尚无模型能解决），同时最小化对领域知识、求解器委托和长上下文伪影的依赖。
我们还开发了一个推理基准比较框架，并用它从表示能力、验证保证和推理深度等方面，将 ProofGrid 与现有工作进行对比。在方法论上，我们引入了一条带检测的证明检查流水线，它能容忍细微的表面偏差，同时定位首次实质性推理失败的位置，从而提升测量分辨率，并将证明规划与低层执行噪声分离开来。
利用这条流水线，我们评估了广泛的开源和闭源模型。结果显示进展迅速，但仍有显著局限：前沿模型在多项基础任务上表现良好，但困难任务——尤其是那些需要全局组合推理或低层证明合成的任务——仍远未解决。我们还发现了认知不稳定性，即模型能生成有缺陷的证明，却又能在孤立情况下正确否定这些局部推理，我们通过认知稳定性指数对此进行了形式化。
最后，我们使用 2PL IRT 分析、Wright 图以及基于 Fisher 信息的归一化任务区分度指标，对准确率进行了补充。
We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning through machine-checkable proofs rather than final answers alone. ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling. Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts and supports precise, auditable verification. This yields mechanical, reproducible, and fine-grained evaluation rather than judgments by humans or LLMs. ProofGrid covers a calibrated difficulty spectrum, from foundational reasoning tests to structurally rich challenge tasks that no current model solves, while minimizing reliance on domain knowledge, solver delegation, and long-context artifacts.
We also develop a comparative framework for reasoning benchmarks and use it to situate ProofGrid relative to existing work in terms of representation, verification guarantees, and reasoning depth. Methodologically, we introduce an instrumented proof-checking pipeline that tolerates minor surface deviations while locating the first substantive reasoning failure, improving measurement resolution and separating proof planning from low-level execution noise. Using this pipeline, we evaluate a broad range of open and proprietary models. Results show rapid progress but substantial remaining limits: frontier models perform well on several foundational tasks, yet difficult tasks, especially those requiring global combinatorial reasoning or low-level proof synthesis, remain far from solved.
We also identify epistemic instability, where models generate flawed proofs yet correctly reject those local inferences in isolation, and formalize this with an Epistemic Stability Index. Finally, we complement accuracy with 2PL IRT analyses, Wright maps, and a normalized task-discrimination measure based on Fisher information.