测试 LLM 在最小形式化下的推理能力
计算机科学中的逻辑
2026-05-14 v1 人工智能
摘要
我们提出 ProofGrid，这是一个通过机器可验证的证明来评估大语言模型推理能力的基准套件，而不仅仅是依赖最终答案。ProofGrid 包含 15 个任务，涵盖证明编写、证明检查、证明掩码和证明填补。这些任务使用最小形式化符号表示，尤其是 NDL（一种紧凑的自然演绷语言），它适合简短提示并支持精确、可审计的验证。这实现了机械化、可重复且细粒度的评估，而非依赖人类或 LLM 的主观判断。ProofGrid 涵盖了已校准难度的光谱，从基础推理测试到结构丰富的挑战性任务（目前没有模型能解决），同时最大限地减少了对领域知识、求解器委托和长上下文人为因素的依赖。我们还开发了一个用于比较推理基准的框架，并将 ProofGrid 置于现有工作的语境中，依据表示、验证保证和推理深度进行评估。方法上，我们引入了一个可计量的证明检查管道，能够容忍轻微的表面偏差，同时定位第一个实质性推理失败，从而提高测量分辨率，并将证明规划与低层执行噪声分离。通过该管道，我们评估了广泛的开源和专有模型。结果表明，快速进步但仍有显著局限：前沿模型在多个基础任务上表现良好，但难题——尤其是需要全局组合推理或低层证明综合的任务——仍远未解决。我们还识别出认知不稳定性，即模型生成错误的证明，却能正确地拒绝局部推理，随后通过认知稳定性指数对其进行形式化。最后，我们补充使用 2PL IRT 分析、Wright 图以及基于 Fisher 信息的归一化任务判别度量。
引用
@article{arxiv.2605.12524,
title = {Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism},
author = {Konstantine Arkoudas and Serafim Batzoglou},
journal= {arXiv preprint arXiv:2605.12524},
year = {2026}
}