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

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