Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

TL;DR

DRIFT presents a four-stage framework—Decompose, Retrieve, Illustrate, then Formalize—to tackle the two core challenges in autoformalization: the complexity of informal statements and the lack of contextual usage for retrieved premises. By breaking statements into atomic sub-queries, retrieving precise dependencies, and supplying exemplar theorems to demonstrate usage, DRIFT substantially enhances dependency retrieval and formalization accuracy across in-distribution and out-of-distribution benchmarks. The approach is model-agnostic and consistently outperforms zero-shot and prior retrieval baselines, with particularly strong gains on ConNF and notable improvements on ProofNet. These findings highlight the importance of structured query decomposition and demonstrative context in bridging informal mathematics and formal libraries like Mathlib, and suggest adaptive retrieval strategies to align with model capabilities.

Abstract

Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean. Current retrieval-augmented autoformalization methods query external libraries using the informal statement directly, but overlook a fundamental limitation: informal mathematical statements are often complex and offer limited context on the underlying math concepts. To address this, we introduce DRIFT, a novel framework that enables LLMs to decompose informal mathematical statements into smaller, more tractable ''sub-components''. This facilitates targeted retrieval of premises from mathematical libraries such as Mathlib. Additionally, DRIFT retrieves illustrative theorems to help models use premises more effectively in formalization tasks. We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval, nearly doubling the F1 score compared to the DPR baseline on ProofNet. Notably, DRIFT demonstrates strong performance on the out-of-distribution ConNF benchmark, with BEq+@10 improvements of 37.14% and 42.25% using GPT-4.1 and DeepSeek-V3.1, respectively. Our analysis shows that retrieval effectiveness in mathematical autoformalization depends heavily on model-specific knowledge boundaries, highlighting the need for adaptive retrieval strategies aligned with each model's capabilities.

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

TL;DR

DRIFT presents a four-stage framework—Decompose, Retrieve, Illustrate, then Formalize—to tackle the two core challenges in autoformalization: the complexity of informal statements and the lack of contextual usage for retrieved premises. By breaking statements into atomic sub-queries, retrieving precise dependencies, and supplying exemplar theorems to demonstrate usage, DRIFT substantially enhances dependency retrieval and formalization accuracy across in-distribution and out-of-distribution benchmarks. The approach is model-agnostic and consistently outperforms zero-shot and prior retrieval baselines, with particularly strong gains on ConNF and notable improvements on ProofNet. These findings highlight the importance of structured query decomposition and demonstrative context in bridging informal mathematics and formal libraries like Mathlib, and suggest adaptive retrieval strategies to align with model capabilities.

Abstract

Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean. Current retrieval-augmented autoformalization methods query external libraries using the informal statement directly, but overlook a fundamental limitation: informal mathematical statements are often complex and offer limited context on the underlying math concepts. To address this, we introduce DRIFT, a novel framework that enables LLMs to decompose informal mathematical statements into smaller, more tractable ''sub-components''. This facilitates targeted retrieval of premises from mathematical libraries such as Mathlib. Additionally, DRIFT retrieves illustrative theorems to help models use premises more effectively in formalization tasks. We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval, nearly doubling the F1 score compared to the DPR baseline on ProofNet. Notably, DRIFT demonstrates strong performance on the out-of-distribution ConNF benchmark, with BEq+@10 improvements of 37.14% and 42.25% using GPT-4.1 and DeepSeek-V3.1, respectively. Our analysis shows that retrieval effectiveness in mathematical autoformalization depends heavily on model-specific knowledge boundaries, highlighting the need for adaptive retrieval strategies aligned with each model's capabilities.

Paper Structure

This paper contains 33 sections, 3 equations, 1 figure, 8 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Methodology
  4. Decompose
  5. Retrieve
  6. Illustrate
  7. Formalize Theorems
  8. Experimental Setup
  9. Benchmarks
  10. Baselines
  11. Implementation Details
  12. Evaluation Metrics
  13. Results and Discussion
  14. Dependency Retrieval
  15. Formalization
  16. ...and 18 more sections

Figures (1)

  • Figure 1: An overview of the Drift framework. Given an informal statement, Drift operates in four stages: ① Decompose: An LLM breaks down the informal statement into atomic, concept-focused sub-queries ($\mathcal{Q}$) (§\ref{['sec:method_decompose']}). ② Retrieve: For each sub-query, a dense retriever identifies foundational dependent premises from a formal library (§\ref{['sec:method_dependency_retrieval']}). ③ Illustrate: A greedy algorithm selects a small set of theorems that demonstrate the practical usage of these retrieved premises (§\ref{['sec:method_theorem_selector']}). ④ Formalize Theorems: Finally, conditioned on all retrieved context, an LLM synthesizes the final formal statement (§\ref{['sec:method_formalize']}).