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 statements lack direct mappings to mathematical theorems and lemmata, nor do those theorems translate trivially into the formal primitives of languages like Lean. 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 42.25% and 37.14% 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.

翻译：将数学陈述自动形式化为定理证明语言（如Lean）仍是大语言模型（LLMs）面临的重大挑战。LLMs难以识别和利用所需的数学先验知识及其在形式语言中的对应表示。当前基于检索增强的自动形式化方法直接使用非形式化陈述查询外部库，但忽视了一个根本性局限：非形式化陈述缺乏与数学定理和引理的直接映射，而这些定理也无法轻易转化为Lean等语言的形式基元。为解决这一问题，我们提出DRIFT这一新颖框架，使LLMs能将非形式化数学陈述分解为更小、更易处理的"子组件"，从而促进从Mathlib等数学库中针对性地检索前提。此外，DRIFT还检索图示性定理，帮助模型在形式化任务中更有效地使用前提。我们在多个基准测试（ProofNet、ConNF和MiniF2F-test）上评估DRIFT，发现其持续提升前提检索效果——在ProofNet上F1得分较DPR基线几乎翻倍。值得注意的是，DRIFT在分布外基准ConNF上表现强劲，使用GPT-4.1和DeepSeek-V3.1时BEq+@10分别提升42.25%和37.14%。我们的分析表明，数学自动形式化中的检索有效性高度依赖于模型特定的知识边界，这凸显了根据各模型能力定制自适应检索策略的必要性。