aiqbench analysis
This arXiv paper studies how LLM agents translate textbook definitions into Lean code, and finds that many generated definitions can't be reused by later results: only 25% to 50% of definition sets were compatible with all downstream statements. Clarifying informal definitions raised compatibility to about 77.5% on average, and cheap unproven property checks helped model judges catch problems. For AI readers, the takeaway is that formal verification output is only useful if it's reusable, so judging and revising definitions is a practical quality lever. The evidence comes from a single new benchmark (ReuseBench), so the gains should be confirmed on other fields.
Definition Grounding in Theory-Level Auto-formalization
arXiv:2610.19223v1 Announce Type: new Abstract: LLM-based auto-formalization systems can now generate formally verified Lean code at unprecedented rates. However, a formalization advances mathematical research only when further mathematical results can be built on it, especially when its definitions and helper lemmas are general enough to be imported and used idiomatically. We propose definition grounding, where definition formalizations are continuously judged and revised, as a method to ensure formalization quality. We find that agents formalizing definitions from textbook text often produce definitions that later statements cannot use, and only 25%-50% of their definition sets are compatible with all later statements. However, clarifying the informal definitions can improve this rate up to 77.5% averaged over all models. Furthermore, stating a small set of basic properties without proving them can improve model judges' capability to detect definitions with compatibility issues, at only about 11% of the definition formalization cost. These results are verified with ReuseBench, a benchmark we curated for formalizing new mathematical fields and theories.
Abstract:LLM-based auto-formalization systems can now generate formally verified Lean code at unprecedented rates. However, a formalization advances mathematical research only when further mathematical results can be built on it, especially when its definitions and helper lemmas are general enough to be imported and used idiomatically. We propose definition grounding, where definition formalizations are continuously judged and revised, as a method to ensure formalization quality. We find that agents formalizing definitions from textbook text often produce definitions that later statements cannot use, and only 25%-50% of their definition sets are compatible with all later statements. However, clarifying the informal definitions can improve this rate up to 77.5% averaged over all models. Furthermore, stating a small set of basic properties without proving them can improve model judges' capability to detect definitions with compatibility issues, at only about 11% of the definition formalization cost. These results are verified with ReuseBench, a benchmark we curated for formalizing new mathematical fields and theories.
Artificial Intelligence (cs.AI)
arXiv:2610.19223 [cs.AI]
(or arXiv:2610.19223v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2610.19223 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
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.
Full text under the publisher's open licence · 252 words
