DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

1. Problem Statement

The paper addresses the challenge of autoformalization: translating informal mathematical statements (natural language) into machine-verifiable formal statements (e.g., in Lean 4). While Large Language Models (LLMs) have improved in informal reasoning, they struggle with formalization due to:

• Knowledge Gaps: LLMs often lack precise knowledge of formal library definitions (e.g., Mathlib) and their specific syntactic usage.
• Retrieval Limitations: Existing Retrieval-Augmented Generation (RAG) methods for autoformalization typically treat the entire informal statement as a single "monolithic" query. This approach fails because:
  1. Informal statements are dense and multifaceted, making them poor queries for retrieving specific, atomic definitions.
  2. Even when correct definitions are retrieved, models often lack the contextual knowledge required to use them correctly (e.g., syntax for type coercions, namespace qualifications, or argument binding).
• Static Fine-tuning Issues: Fine-tuning models on static libraries leads to hallucinations when libraries are updated (renamed/deprecated objects), necessitating dynamic, test-time retrieval strategies.

2. Methodology: The DRIFT Framework

The authors propose DRIFT, a four-stage framework designed to bridge the gap between informal concepts and formal syntax. The process is visualized in Figure 1 of the paper:

Stage 1: Decompose

Instead of querying the entire statement, an LLM (the Decomposer) breaks the informal statement into a set of atomic, concept-focused sub-queries ($Q$).

• Mechanism: For each sub-query, the model generates a natural language description of a specific concept (e.g., "A prime number $p$ of the form $4t+3$") and a predicted formal representation (e.g., p : ℕ with Nat.Prime p).
• Purpose: This transforms a complex retrieval problem into focused searches, aligning the query granularity with the indexed documents in the formal library.

Stage 2: Retrieve

A dense passage retriever (based on BGE-M3, fine-tuned on dependency retrieval tasks) identifies dependent premises from the formal library (e.g., Mathlib) corresponding to each sub-query.

• Mechanism: The retriever encodes the sub-queries and library objects into a shared embedding space. It selects the top-1 most similar premise for each sub-query, aggregating them into a set $R_{DRIFT}$.
• Advantage: This ensures that the retrieval targets specific logical dependencies rather than semantically similar but irrelevant theorems.

Stage 3: Illustrate

Retrieving definitions is insufficient without knowing how to use them. This stage selects a small set of illustrative theorems ($T$) that demonstrate the practical application of the retrieved premises.

• Mechanism: A greedy algorithm selects up to $m$ theorems (where $m=3$ in experiments) from the library. The selection maximizes the coverage of the retrieved premises $R_{DRIFT}$ while prioritizing theorems semantically similar to the original problem.
• Purpose: These theorems act as "scaffolding," providing concrete examples of syntax, type coercions, and argument binding patterns required to integrate the premises correctly.

Stage 4: Formalize Theorems

The final LLM (Formalizer) generates the formal statement ($FS$) conditioned on the assembled context:
$$C = \text{Instruction} \oplus R_{DRIFT} \oplus T \oplus \text{Informal Statement}$$
The model synthesizes the final Lean code using the retrieved definitions and the usage patterns observed in the illustrative theorems.

3. Key Contributions

1. Novel Framework: Introduction of DRIFT, which uniquely combines query decomposition (to handle statement complexity) with contextual illustration (to handle syntactic usage), moving beyond monolithic retrieval.
2. State-of-the-Art Performance: DRIFT establishes new SOTA in dependency retrieval and autoformalization across diverse benchmarks, particularly on Out-of-Distribution (OOD) tasks.
3. Insight on Model Boundaries: The paper reveals that retrieval effectiveness is heavily dependent on the gap between a model's parametric knowledge and the statement's complexity. It highlights the need for adaptive strategies that assess when external knowledge is truly necessary.

4. Experimental Results

The framework was evaluated on three benchmarks: ProofNet (in-distribution), MiniF2F-test (self-contained/low dependency), and ConNF (out-of-distribution, novel mathematical domain).

• Dependency Retrieval:

  • DRIFT nearly doubles the F1 score compared to the DPR baseline on ProofNet (27.68% vs 13.77% with Claude-Opus-4).
  • It significantly improves recall by decomposing queries, allowing the retrieval of precise atomic definitions that monolithic queries miss.

• Autoformalization (Formal Correctness):

  • ConNF (OOD): DRIFT shows massive gains. Using GPT-4.1, it improved BEq+@10 by 55.57% over zero-shot and even surpassed the Oracle baseline* (which has ground-truth dependencies but no usage context). This proves that how definitions are used (illustrated by DRIFT) is more critical than just having the definitions.
  • ProofNet: Consistent improvements over zero-shot and the strong DPR (RAuto) baseline across all models (GPT-4.1, DeepSeek-V3.1, Goedel-V2-8B).
  • MiniF2F-test: Performance gains are smaller or mixed. This benchmark has very low library dependencies (avg 0.43). The paper notes that in low-dependency regimes, retrieval can act as a "distractor," causing models to over-complicate simple problems.

• Ablation Studies:

  • Removing the Illustrate module significantly drops performance on complex benchmarks, confirming that usage examples are crucial.
  • Removing the Decompose module (reverting to monolithic retrieval) sometimes recovers performance on simple benchmarks but fails on complex ones, highlighting the trade-off between precision and noise.
  • Synergy: The "Illustrate" module acts as a scaffold that helps models navigate the diverse (and potentially noisy) information retrieved by the decomposition step.

5. Significance and Future Directions

• Paradigm Shift: DRIFT shifts the focus from simple "retrieval of similar theorems" to "retrieval of dependencies + retrieval of usage patterns."
• Robustness: It demonstrates that RAG can outperform even imperfect Oracle baselines (which have ground-truth dependencies) by providing the necessary syntactic context.
• Adaptive Retrieval: The results suggest that future systems should be adaptive, dynamically deciding whether to retrieve based on the problem's complexity (e.g., skipping retrieval for self-contained problems like MiniF2F to avoid distraction).
• Agentic Workflows: The authors suggest that future work should integrate DRIFT into agentic frameworks where models can iteratively refine attempts based on compiler feedback (Typecheck errors), using retrieval to fix specific syntactic gaps.

In conclusion, DRIFT effectively solves the "knowledge vs. usage" bottleneck in mathematical autoformalization by decomposing complex queries and providing concrete syntactic scaffolding, leading to significant improvements in generating correct formal proofs.