论文页面 - 通过最小形式主义下的证明对LLM推理能力进行压力测试

来源：https://huggingface.co/papers/2605.12524

摘要

ProofGrid 提供了一个基准测试套件，用于通过机器可验证的证明评估 LLM 推理，包含采用最小形式化符号的证明编写与验证任务，以及一个比较框架用于评估推理深度与稳定性。

我们介绍了 ProofGrid，这是一个基准测试套件，通过机器可验证的证明（https://huggingface.co/papers?q=machine-checkable%20proofs）而非单纯最终答案来评估 LLM 推理。ProofGrid 包含 15 项任务，涵盖证明编写（https://huggingface.co/papers?q=proof%20writing）、证明检查（https://huggingface.co/papers?q=proof%20checking）、证明掩码（https://huggingface.co/papers?q=proof%20masking）和证明填空（https://huggingface.co/papers?q=proof%20gap-filling）。任务采用最小形式化符号（https://huggingface.co/papers?q=formal%20notation），特别是 NDL（https://huggingface.co/papers?q=NDL），一种紧凑的自然演绎语言（https://huggingface.co/papers?q=natural-deduction%20language），适合简短提示并支持精确、可审计的验证。这带来了机械性、可复现、细粒度的评估，而非依赖人类或 LLM 的判断。ProofGrid 覆盖了经过校准的难度谱系，从基础推理测试到结构丰富的挑战任务（当前没有模型能解决），同时最小化对领域知识、求解器委托和长上下文伪影的依赖。我们还开发了一个推理基准比较框架，并据此将 ProofGrid 定位于现有工作，从表示形式、验证保证和推理深度（https://huggingface.co/papers?q=reasoning%20depth）维度进行对比。方法论上，我们引入了一个带检测的证明检查流水线，容忍细微的表示差异，同时定位第一个实质性推理失败，从而提高测量分辨率，并将证明规划与低级执行噪声分离。利用该流水线，我们评估了多种开源和闭源模型。结果显示进展迅速但仍存在显著局限：前沿模型在若干基础任务上表现良好，但困难任务（尤其是需要全局组合推理或低级证明合成的任务）远未解决。我们还发现了认知不稳定性：模型生成有缺陷的证明，却能正确拒绝这些局部推理（隔离情况下），我们通过认知稳定性指数（https://huggingface.co/papers?q=Epistemic%20Stability%20Index）对此进行了形式化。最后，我们用 2PL IRT 分析（https://huggingface.co/papers?q=2PL%20IRT%20analyses）、赖特图（https://huggingface.co/papers?q=Wright%20maps）和基于费舍尔信息（https://huggingface.co/papers?q=Fisher%20information）的规范化任务区分度量补充了准确率指标。

查看 arXiv 页面（https://arxiv.org/abs/2605.12524）
查看 PDF（https://arxiv.org/pdf/2605.12524）
项目页面（https://github.com/System-2-Labs/ProofGrid）
GitHub2（https://github.com/System-2-Labs/ProofGrid）
添加到收藏（https://huggingface.co/login?next=%2Fpapers%2F2605.12524）

引用该论文的模型 0

无模型引用此论文

请在模型 README.md 中引用 arxiv.org/abs/2605.12524 以链接至此页面。

引用该论文的数据集 0

无数据集引用此论文

请在数据集 README.md 中引用 arxiv.org/abs/2605.12524 以链接至此页面。

引用该论文的 Spaces 0

无 Space 引用此论文

请在 Space README.md 中引用 arxiv.org/abs/2605.12524 以链接至此页面。

包含该论文的收藏集 0

无收藏集包含此论文

请将此论文添加到收藏（https://huggingface.co/new-collection）以链接至此页面。