Definition grounding improves use of formal math code in proofs
Definition Grounding in Theory-Level Auto-formalization
Artificial Intelligence
Summary
Using large language models to turn math from textbooks into formal code often creates definitions that later math statements can't build on properly. The authors show that carefully checking and improving these definitions can make them much more useful, raising the success rate from about 25%-50% up to nearly 78%. They also find that giving the models some basic properties without proofs helps spot incompatible definitions more efficiently. The work includes a new test set to measure how well these improvements hold up.
What this means in practice
- •For software verification teams: Improve the reliability of formal specifications by continuously validating and refining definitions that underpin verified code.
- •For automated theorem proving developers: Use definition grounding to increase the proportion of formalized definitions that support further proof development in large mathematical libraries.
Authors
Leyan Pan, Christian Szegedy, Frederick Rajasekaran, Robi Bhattacharjee, Gregory Constantine, Wenke Lee
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.