Automated Formalization via Conceptual Retrieval-Augmented LLMs

TL;DR

CRAMF is a retrieval-augmented framework that improves automated formalization in theorem proving by grounding LLMs with a large, structured knowledge base of formal definitions, significantly enhancing accuracy.

Contribution

This work introduces CRAMF, a novel retrieval-augmented formalization framework that constructs a large knowledge base from Mathlib4 and employs advanced retrieval strategies to improve LLM-based formalization.

Findings

Achieves up to 62.1% accuracy improvement in formalization tasks.

Constructs a knowledge base with over 26,000 definitions and 1,000 core concepts.

Demonstrates consistent accuracy gains across multiple benchmarks.

Abstract

Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g., undefined predicates, symbol misuse, and version incompatibility) and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, we propose CRAMF, a Concept-driven Retrieval-Augmented Mathematical Formalization framework. CRAMF enhances LLM-based autoformalization by retrieving formal definitions of core mathematical concepts, providing contextual grounding during code generation. However, applying retrieval-augmented generation (RAG) in this setting is non-trivial due to the lack of structured knowledge bases, the polymorphic nature of mathematical concepts, and the high precision required in formal retrieval. We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4, the standard mathematical library for the Lean 4 theorem prover, indexing over 26,000 formal definitions and 1,000+ core mathematical concepts. To address conceptual polymorphism, we propose contextual query augmentation with domain- and application-level signals. In addition, we design a dual-channel hybrid retrieval strategy with reranking to ensure accurate and relevant definition retrieval. Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers, yielding consistent improvements in translation accuracy, achieving up to 62.1% and an average of 29.9% relative improvement.