← 研踪 PaperTrailACL Anthology · ACL 2026:acl:2026.acl-industry.150 · 记录 #1
Benchmarking Testing in Automated Theorem Proving
来源日期（仅到月份） 2026-07
来源记录日期 2026-07
雷达观测 2026-11-01 22:06
摘要
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^2, 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.
论文发现出处
这些页面提供论文线索，不代表同行评审或质量认证。
观测到的版本
平台记录号代表本站观测到的元数据变化，不是作者修订号。来源日期仅到月份或年份时，按该月或该年首日存档。
记录 #1 · 2026-07 · 最新观测版本
Benchmarking Testing in Automated Theorem Proving
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^2, 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.
查看此版本解读 →查看此版本原文 ↗