SITA: A Framework for Structure-to-Instance Theorem Autoformalization

TL;DR

This paper introduces SITA, a framework that automates the formalization of concrete mathematical theorems from abstract structures using large language models and Lean proof assistant, improving efficiency and correctness.

Contribution

SITA provides a systematic, modular approach for auto-formalizing theorems by bridging abstract theories and concrete instances with LLM-guided generation and verification.

Findings

Effective formalization of diverse instances in optimization problems

Integration of LLMs with feedback for correctness

Successful application in Lean proof assistant

Abstract

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.