用测试编译成功评估数学定理生成，发现现有模型实际正确率仅38.9%。
Benchmarking Testing in Automated Theorem Proving
- 以后续定理能否编译成功作为语义正确性标准，类似代码集成测试。
- 在2206个真实Lean 4问题上，最佳模型准确率仅38.9%。
- 无需人工标注，自动构建大规模评测基准，适合验证推理模型可靠性。
大型语言模型在形式化定理证明中展现出潜力，但评估语义正确性仍具挑战。现有方法依赖词法重叠或昂贵的人工检查。受代码生成中从词法比较转向测试评估的启发，我们提出T框架：只有当所有依赖的后续定理都能成功编译时，生成的定理才被视为正确，类比于集成测试。我们从5个真实Lean 4仓库构建基准，包含2,206个问题，平均每个问题对应41个后续定理，全部自动提取无需人工参与。实验表明，尽管先进模型在编译成功率上表现良好，但在我们的语义指标下表现显著下降。最佳模型Claude-Sonnet-4.5在提供自然语言证明和后续定理作为上下文时，整体测试准确率仅为38.9%，暴露出当前定理生成能力的关键差距。
原文摘要 · Abstract (English)
Recent advances in large language models (LLMs) have shown promise in formal theorem proving, yet evaluating semantic correctness remains challenging. Existing evaluations rely on indirect proxies such as lexical overlap with human-annotated proof, or expensive manual inspection. Inspired by the shift from lexical comparison to test-based evaluation in code generation, we propose T , a framework that evaluates the semantic correctness of formal theorems: a generated theorem is considered correct only if all dependent successor theorems compile successfully, analogous to integration testing. We construct a benchmark from 5 real-world Lean 4 repositories, comprising 2,206 problems paired with 41 successor theorems on average, automatically extracted without human effort. Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric. The best model, Claude-Sonnet-4.5, achieves only 38.9% Testing Accuracy on the full set, given both natural language proof and successor theorems as context, revealing a critical gap in current theorem generation capabilities.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。