TLDR: DRIFT is a new framework that helps Large Language Models (LLMs) formalize mathematical statements. It works by breaking down complex statements into smaller parts (Decompose), finding relevant mathematical definitions (Retrieve), showing examples of how these definitions are used (Illustrate), and then using all this information to create the final formal statement (Formalize Theorems). This method significantly improves the accuracy of finding necessary mathematical knowledge and formalizing theorems, especially for complex and unfamiliar mathematical problems, by providing LLMs with better context and usage examples.
Artificial intelligence is making significant strides in many fields, but one area that remains particularly challenging is the automatic formalization of mathematical statements for theorem proving. Large Language Models (LLMs) often struggle with this because they find it difficult to identify and correctly use the vast amount of prerequisite mathematical knowledge and its formal representation in languages like Lean.
Current methods that try to help LLMs by retrieving information from external libraries often fall short. They typically query these libraries using the informal mathematical statement directly. However, informal statements are frequently complex and don’t provide enough context about the underlying mathematical concepts, making it hard for LLMs to find precisely what they need.
Introducing DRIFT: A New Approach to Autoformalization
To tackle these challenges, researchers have introduced a novel framework called DRIFT, which stands for Decompose, Retrieve, Illustrate, Then Formalize Theorems. This framework empowers LLMs to break down complex informal mathematical statements into smaller, more manageable “sub-components.” This decomposition allows for a much more targeted and effective retrieval of necessary mathematical premises from extensive libraries such as Mathlib.
Beyond just retrieving definitions, DRIFT also finds and presents “illustrative theorems.” These are examples that show how the retrieved mathematical concepts and definitions are actually used in practice, helping LLMs to apply them correctly in formalization tasks. You can read the full research paper for more details on this innovative framework. Read the full research paper here.
How DRIFT Works: The Four Stages
DRIFT operates in four distinct stages, designed to systematically guide LLMs through the autoformalization process:
1. Decompose: The first step involves an LLM breaking down the original informal mathematical statement into several smaller, concept-focused sub-queries. Each sub-query aims to isolate a single mathematical idea, making the retrieval process more precise.
2. Retrieve: For each of these individual sub-queries, a specialized retriever identifies foundational dependent premises from a formal mathematical library. This ensures that the exact definitions and axioms needed for each concept are found.
3. Illustrate: Once the core premises are retrieved, a clever algorithm selects a small set of existing theorems that demonstrate how these premises are practically applied. These examples provide crucial context and usage patterns, bridging the gap between knowing a definition and knowing how to use it.
4. Formalize Theorems: Finally, with all the retrieved definitions and illustrative examples in hand, an LLM synthesizes the final formal statement in a language like Lean. This comprehensive context helps the model to structure and integrate the formal components accurately.
Significant Improvements in Mathematical Formalization
DRIFT has been rigorously evaluated across various benchmarks, including ProofNet, ConNF, and MiniF2F-test. The results consistently show that DRIFT significantly improves premise retrieval. For instance, it nearly doubles the F1 score compared to a standard baseline on ProofNet, indicating much better accuracy in finding relevant mathematical knowledge.
Notably, DRIFT demonstrates strong performance even on out-of-distribution benchmarks like ConNF, which contains research-level theorems from a novel mathematical domain not typically seen by the models. On ConNF, DRIFT achieved substantial improvements in logical equivalence (BEq+@10) of 37.14% and 42.25% using GPT-4.1 and DeepSeek-V3.1, respectively. This highlights the framework’s ability to generalize to new and complex mathematical areas.
The research also revealed that the effectiveness of retrieval in mathematical autoformalization depends heavily on the specific knowledge boundaries of each LLM. This suggests that future systems will need adaptive retrieval strategies that can intelligently assess when external knowledge truly complements a model’s inherent capabilities.
Also Read:
- Enhancing LLM Reasoning with Attribution-Based Credit Assignment and Dynamic Exploration
- Multidimensional Feedback for Smarter Language Models
Conclusion
DRIFT represents a significant step forward in automating the formalization of mathematics. By decomposing complex queries and providing illustrative examples, it addresses key limitations of previous methods. This dual approach not only enhances the accuracy of formalization on challenging benchmarks but also offers a broadly applicable strategy for improving how LLMs handle formal mathematical reasoning.
