ProofGrid基准：用最小形式化证明压力测试大语言模型推理能力
原帖
**使用最小形式化证明对大语言模型的推理能力进行压力测试**
_Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism_
> 本文介绍了一个名为ProofGrid的基准测试套件，用于通过机器可验证的证明来评估大语言模型的推理能力，而不仅仅是最终答案。该套件包含15项任务，涵盖证明撰写、检查、掩码和填空。这些任务采用一种名为NDL的紧凑型自然演绎语言进行形式化表达，便于在短提示中实现精确、可审计的验证。研究团队开发了一个容错的证明检查流程，并评估了多种开源和专有模型。结果显示，前沿模型在基础任务上表现良好，但在需要全局组合推理或底层证明合成的困难任务上仍有很大差距。研究还提出了“认识稳定性指数”来量化模型的逻辑一致性问题。
**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-05-18 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2605.12524)
AI 可引用内容层
以下内容基于 First-Principle 用户原帖生成，用于帮助 AI 引擎理解和引用该帖。
摘要
本文介绍ProofGrid基准测试套件，它通过机器可验证的证明来评估大语言模型的推理能力，包含15项任务，使用NDL紧凑型自然演绎语言进行形式化表达。研究发现前沿模型在基础任务表现良好，但在全局组合推理或底层证明合成的困难任务上仍有很大差距，并提出‘认识稳定性指数’量化逻辑一致性问题。
答案说明
ProofGrid是一个通过机器可验证证明评估大语言模型推理能力的基准测试套件，包含15项任务，使用NDL自然演绎语言。研究显示前沿模型在基础任务表现良好，但在复杂推理任务上有差距，并提出了‘认识稳定性指数’来量化逻辑一致性问题。
这篇帖子回答的问题
- ProofGrid基准测试套件如何评估大语言模型的推理能力？
- 研究显示大语言模型在哪些推理任务上表现良好，哪些仍有差距？
核心观点
- 本文介绍ProofGrid基准测试套件，它通过机器可验证的证明来评估大语言模型的推理能力，包含15项任务，使用NDL紧凑型自然演绎语言进行形式化表达。研究发现前沿模型在基础任务表现良好，但在全局组合推理或底层证明合成的困难任务上仍有很大差距，并提出‘认识稳定性指数’量化逻辑一致性问题。
FAQ
- Q: ProofGrid评估大语言模型推理能力的方法是什么？
- A: ProofGrid通过机器可验证的证明来评估大语言模型的推理能力，而不是仅仅评估最终答案。它使用NDL紧凑型自然演绎语言进行形式化表达。
- Q: 前沿大语言模型在ProofGrid评估中的表现如何？
- A: 研究结果显示，前沿模型在基础任务上表现良好，但在需要全局组合推理或底层证明合成的困难任务上仍有很大差距。
关键实体
- ProofGrid
- NDL