SITA: A Framework for Structure-to-Instance Theorem Autoformalization
This addresses the problem of automating formal theorem proving for researchers in mathematics and computer science, but it is incremental as it builds on existing LLM and typeclass methods.
The paper tackles the challenge of autoformalizing theorems that instantiate abstract structures in concrete settings, developing the SITA framework to bridge this gap in Lean, and demonstrates its effectiveness on a dataset of optimization problems.
While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing mathematical results at the research level, we develop a framework for structure-to-instance theorem autoformalization (SITA), which systematically bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant. Formalized abstract structures are treated as modular templates that contain definitions, assumptions, operations, and theorems. These templates serve as reusable guides for the formalization of concrete instances. Given a specific instantiation, we generate corresponding Lean definitions and instance declarations, integrate them using Lean's typeclass mechanism, and construct verified theorems by checking structural assumptions. We incorporate LLM-based generation with feedback-guided refinement to ensure both automation and formal correctness. Experiments on a dataset of optimization problems demonstrate that SITA effectively formalizes diverse instances grounded in abstract structures.