Improving Autoformalization Using Direct Dependency Retrieval

TL;DR

This paper introduces DDR, a novel retrieval-augmented framework for statement autoformalization that enhances dependency retrieval accuracy and scalability, significantly improving formal library dependency identification from natural language descriptions.

Contribution

The paper presents DDR, a new method for direct dependency retrieval that outperforms existing approaches in precision, recall, and scalability for autoformalization tasks.

Findings

DDR achieves higher retrieval precision and recall than SOTA methods.

The dependency retrieval dataset contains over 500,000 samples.

Autoformalizer with DDR shows better accuracy and stability in experiments.

Abstract

The convergence of deep learning and formal mathematics has spurred research in formal verification. Statement autoformalization, a crucial first step in this process, aims to translate informal descriptions into machine-verifiable representations but remains a significant challenge. The core difficulty lies in the fact that existing methods often suffer from a lack of contextual awareness, leading to hallucination of formal definitions and theorems. Furthermore, current retrieval-augmented approaches exhibit poor precision and recall for formal library dependency retrieval, and lack the scalability to effectively leverage ever-growing public datasets. To bridge this gap, we propose a novel retrieval-augmented framework based on DDR (\textit{Direct Dependency Retrieval}) for statement autoformalization. Our DDR method directly generates candidate library dependencies from natural language mathematical descriptions and subsequently verifies their existence within the formal library via an efficient suffix array check. Leveraging this efficient search mechanism, we constructed a dependency retrieval dataset of over 500,000 samples and fine-tuned a high-precision DDR model. Experimental results demonstrate that our DDR model significantly outperforms SOTA methods in both retrieval precision and recall. Consequently, an autoformalizer equipped with DDR shows consistent performance advantages in both single-attempt accuracy and multi-attempt stability compared to models using traditional selection-based RAG methods.