自动定理证明中的基准测试

大语言模型 (LLM) 的最新进展在形式定理证明方面显示出了前景，但评估语义正确性仍然具有挑战性。现有的评估依赖于间接代理，例如与人工注释证据的词汇重叠，或昂贵的手动检查。受到代码生成中从词汇比较到基于测试的评估的转变的启发，我们提出了 T ，一个评估形式定理语义正确性的框架：只有当所有依赖的后继定理编译成功时，生成的定理才被认为是正确的，类似于集成测试。我们从 5 个现实世界的 Lean 4 存储库构建了一个基准，其中包含 2,206 个问题，平均配有 41 个后继定理，无需人工操作即可自动提取。实验表明，虽然最先进的模型取得了很高的编译成功率，但在我们的语义指标下，它们的表现却明显较差。在自然语言证明和后继定理作为上下文的情况下，最好的模型 Claude-Sonnet-4.5 在整个模型上仅达到 38.9% 的测试准确度，揭示了当前定理生成能力的关键差距。