analiza aiqbench
The paper audits CLEVER, a Lean 4 benchmark for verifiable code generation, and finds questionable reference specifications in 80 of its 161 entries, even though the benchmark's authors accepted them. It also shows that isomorphism-based scoring breaks down when generated and reference specifications encode different but defensible readings. For readers evaluating agentic systems, the main lesson is that high scores on formal-verification benchmarks may reflect benchmark flaws as much as model capability.
Isomorphism Is Not Enough: An Agentic Audit of Verified Code Generation in Lean
arXiv:2605.23772v2 Announce Type: replace Abstract: Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification and how reliably existing benchmarks can measure them, we audit CLEVER, a Lean 4 benchmark for verifiable code generation, using three independent agentic stacks based on Claude Opus 4.6, GPT-5.4, and Kimi K2.5. Our audit finds arguably erroneous reference specifications in 80 of 161 entries, each accepted by the benchmark's authors, distills a taxonomy of benchmark errors, and exposes structural limitations of isomorphism-based scoring, whose signal breaks down when generated and reference specifications formalize different yet defensible readings. In the process, the stacks generate arguably valid specifications for up to 98.8% of entries, certify implementations against sound reference specifications for up to 92.3%, and reach up to 96.2% end-to-end success over entries with sound premises, suggesting that CLEVER no longer stresses modern agentic provers as much as its design intended. Looking ahead, we translate our findings into recommendations for future work, with our error analysis doubling as a repair list for CLEVER and a heuristic checklist for the next generation of benchmarks.
Abstract:Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification and how reliably existing benchmarks can measure them, we audit CLEVER, a Lean 4 benchmark for verifiable code generation, using three independent agentic stacks based on Claude Opus 4.6, GPT-5.4, and Kimi K2.5. Our audit finds arguably erroneous reference specifications in 80 of 161 entries, each accepted by the benchmark's authors, distills a taxonomy of benchmark errors, and exposes structural limitations of isomorphism-based scoring, whose signal breaks down when generated and reference specifications formalize different yet defensible readings. In the process, the stacks generate arguably valid specifications for up to 98.8% of entries, certify implementations against sound reference specifications for up to 92.3%, and reach up to 96.2% end-to-end success over entries with sound premises, suggesting that CLEVER no longer stresses modern agentic provers as much as its design intended. Looking ahead, we translate our findings into recommendations for future work, with our error analysis doubling as a repair list for CLEVER and a heuristic checklist for the next generation of benchmarks.
Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Software Engineering (cs.SE)
arXiv:2605.23772 [cs.AI]
(or arXiv:2605.23772v2 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2605.23772 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 290 cuvinte
Subiecte conexe
Groupoid Representation of Lorentz Transformations Including Superluminal Observers
arXiv · 14 oct. 2026
PauLie: Fast Classification of Pauli Dynamical Lie Algebras
arXiv · 1 sept. 2026
Periodic Symmetry-Adapted Encoding: Qubit Reduction in Crystalline Electronic Structure
arXiv · 5 iun. 2026
Markovian Linguistic-Temporal Bridge: Unlocking the Potential of LLMs for Time Series Forecasting
arXiv · 20 oct. 2026