形式化证明基准

ProofGrid基准：用最小形式化证明压力测试大语言模型推理能力

本文介绍ProofGrid基准测试套件，它通过机器可验证的证明来评估大语言模型的推理能力，包含15项任务，使用NDL紧凑型自然演绎语言进行形式化表达。研究发现前沿模型在基础任务表现良好，但在全局组合推理或底层证明合成的困难任务上仍有很大差距，并提出‘认识稳定性指数’量化逻辑一致性问题。