Consistent Autoformalization for Constructing Mathematical Libraries (2024)

Abstract: Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation capabilities of Large Language Models (LLMs), including in formal languages, are lowering the barriers for autoformalization. However, LLMs alone are not capable of consistently and reliably delivering autoformalization, in particular as the complexity and specialization of the target domain grows. As the field evolves into the direction of systematically applying autoformalization towards large mathematical libraries, the need to improve syntactic, terminological and semantic control increases. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality. The empirical analysis, across different models, demonstrates that these mechanisms can deliver autoformalizaton results which are syntactically, terminologically and semantically more consistent. These mechanisms can be applied across different LLMs and have shown to deliver improve results across different model types.

## introduction mathematical reasoning constitutes an essential aspect of human intelligence @xcite . it centers on symbolic-level reasoning, as manifested through systematic, abstract and and step-wise logical inference. mathematical reasoning models has been clustered under two types: deep learning models @xcite @xcite and formal models @xcite @xcite @xcite . mathematical reasoning in large language models (llms) predominantly uses statements expressed in informal mathematical statements. more recent models have aimed towards bridging both informal and formal mathematical reasoning @xcite @xcite , where the material (content-based) inference strengths of llms are complemented by external formal/symbolic reasoning methods such as automated theorem provers (e.g. isabelle @xcite and @xcite ), which can systematically assess the logical validity of the reasoning process @xcite , facilitating llms to perform controlled and consistent inference. however, formal and verifiable mathematical reasoning with theorem provers requires the manual formalization of logical formulae from informal statements, in order to build the supporting mathematical libraries, knowledge bases (kbs) which express previous axioms, definitions, theorems and proofs, a process that demands considerable effort and domain-specific knowledge. a prototypical case in point is the liquid tensor experiment @xcite , an initiative aimed at formalizing analytical geometry results from scholze & clausen, requiring a community coordinated effort of experts. contemporary llms have demonstrated considerable efficacy @xcite @xcite for supporting autoformalization efforts within an in-context learning paradigm, being largely evaluated in less specialized domains and tasks. existing methods are still limited in delivering a method for systematically and consistently building large formal and specialized mathematical libraries. the essence of the challenge is twofold: (i) specialization and out-of-distribution (ood) drifts: as one moves towards more specialized and newer domains to be autoformalized, figure 1 : the overall framework consists of three stages: stage 1 contains one round for retrieval augmented autoformalization; stage 2 contains one round for denoising; stage 3 is composed of several iterative rounds to refine the code based on syntax errors. for better illustration, we change \<in>, \<nat>, \<lsq>, @xmath0 to their latex version ∈, n, ≤, +. the ground truth code is lemma (in int0) int_zf_1_5_l7a: assumes "a\<@xmath1. this work targets the overarching research question: 'how to systematically support the creation of consistent and coherent formal mathematical libraries from informal mathematical statements?'. in order to address this task, we decompose this broader aim into the following research questions: rq1: 'to what extent contemporary llms are capable of formalizing specialized mathematical statements into formal representations for mathematical libraries?'; rq2: 'which metrics can be used to assess the quality of the formalized outputs?'; rq3: 'which mechanisms can be used to extend the autoformalization properties of llms to achieve better generative control and enhance terminological, syntactic and semantic consistency and coherence?'. to address these research questions, we propose a novel framework (see figure 1 ) that leverages llms with most-similar retrieval augmented generation (ms-rag), denoising steps and iterative feedback-guided syntax error refinement cycles (auto-sef) to deliver a syntactically consistent and semantically coherent autoformalization. to assess the effectiveness of our proposed framework, we construct a supporting dataset for the task of mathematical library autoformalization (mathlibform) and build a supporting empirical analysis methodology guided by a critical selection of a set of automated metrics. we conduct a systematic empirical analysis with a diverse sample of state-of-the-art llms, in order to compare and contrast their autoformalization properties and the impact of the proposed library autoformalization mechanisms. our results demonstrate that leveraging llms with ms-rag and auto-sef, combined with denoising strategies, can significantly enhance the syntactic correctness of formalization results, reaching improvements from 5.47% to 33.58%. in summary, the contributions of the paper are: ## proposed approach in this section, we start by defining the target task and then describe the proposed mechanisms for improving autoformalization. autoformalization: an autoformalization is a transformation function which maps an informal mathematical statement s in the domain of natural language and latex symbols s into a formal mathematical statement ϕ, under a formal language f, f : @xmath2, such that for every @xmath3, there exists a ϕ ∈ f where f (s) = ϕ. semantic correctness: a transformation f (s) = ϕ is semantically correct if there exists a model m such that: ## conclusion this paper examined the effects of using rag for autoformalization with llms and explored methods to refine formalization results. our experiments demonstrated the effectiveness of incorporating a retrieval process for autoformalization. further experiments indicated that denoising and iteratively refining syntax errors can enhance autoformalization quality. we evaluated results on different llms and found that smaller llms with instruction fine-tuning benefited more from the proposed methods, pointing in the direction of serving as a mechanism for reducing the formal performance gaps between larger and smaller models. we also built a dataset and assessed metrics for evaluating autoformalization, which could serve as resources/methodological contributions for formal mathematical reasoning tasks. we believe combining the semantic similarity metrics with the syntactic correctness metric is a reasonable proxy for semantic correctness.