Automated Formalization via Conceptual Retrieval-Augmented LLMs
Authors: Wangyue Lu
Lun Du
Sirui Li
Ke Weng
Haozhe Sun
Hengyu Liu
Minghe Yu
Tiancheng Zhang
Ge Yu
Venue: ICLR 2026 Poster (2026)
Keywords: Autoformalization
Retrieval-augmented Generation
Primary area: foundation or frontier models, including LLMs

Abstract: Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g., undefined predicates, symbol misuse, and version incompatibility) and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, we propose CRAMF, a Concept-driven Retrieval-Augmented Mathematical Formalization framework. CRAMF enhances LLM-based autoformalization by retrieving formal definitions of core mathematical concepts, providing contextual grounding during code generation. However, applying retrieval-augmented generation (RAG) in this setting is non-trivial due to the lack of structured knowledge bases, the polymorphic nature of mathematical concepts, and the high precision required in formal retrieval. We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4, the standard mathematical library for the Lean 4 theorem prover, indexing over 26,000 formal definitions and 1,000+ core mathematical concepts. To address conceptual polymorphism, we propose contextual query augmentation with domain- and application-level signals. In addition, we design a dual-channel hybrid retrieval strategy with reranking to ensure accurate and relevant definition retrieval. Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers, yielding consistent improvements in translation accuracy—achieving up to 62.1% and an average of 29.9% relative improvement.

Published as a conference paper at ICLR 2026
AUTOMATED FORMALIZATION VIA CONCEPTUAL RETRIVVL-AAGMENTEED LLMs
Wangyue Lu
Lun 2 Sirui Li!
Ke Weng'
Haozhe Sun'
Hengyu Liu
Minghe Yu+
Tiancheng Zhang Ge Yu!
School of Computer Science and Engineering, Northeastern University, Shenyang 110819, China 2 Ant Research, Ant Group, Beijing, China
3 *Department of Computer Science, Aalborg University, Denmark
*Software College, Northeastern University, Shenyang 10881, China
20223246@stu. neu. www.ett.uuuueeuuu...mm.mm.... dulun. dllantgrruppcco {20226504, (tt.::1125)sssuuu.e neu..eu..u edu. cn, sunhz6@mails neu.edu heli@cs. {yuminghe, yuge) neu. edu. on
ABSTRACT
Interactive theorem provers (ITPs) require manual formalization, which is labor- intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g. un- defined predicates, symbol misuse, and version incompatibility) and the seman- tic gap caused by ambiguous missing premises in natural language descrip- tions. To address these issues, we propose CRAMF, Concept-driven Retrieval- Augmented Mathematical Formalization framework. CRAMF enhances LLM- based autoformalization by retrieving formal definitions of core mathematical concepts, providing contextual grounding during code generation. However, ap- plying retrieval-augmente generation (RAG) this setting is non-trivial due to the lack of structured knowledge bases, the polymorphic nature of mathemati- cal concepts, and the high precision required in formal retrieval. We introduce framework for automatically constructing concept-definition knowledge base from Mathlib4, the standard mathematical library for the Lean 4 theorem prover, indexing over 26,000 formal definitions and 1,000+ core mathematical concepts. To address conceptual polymorphism, we propose contextual query augmenta- tion with domain- and application-Ievel signals. In addition, we design dual- channel hybrid retrieval strategy with reranking to ensure accurate and relevant definition retrieval. Experiments on miniF2F. ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers, yielding consistent improvements in translation ac- achievia up to 62. 1% and an average of 29.9% relative improvement.
INTRODUCTION
Automated formalization the process of translating natural language descriptions of mathematical theorems into formally verifiable representations (Weng et al. 2025), ),, such as Lean (Moura & UlI- rich 2021). Coq (Huet al. 1997), Isabelle (Paulson 1994). In the era of large language models (LLMs), it serves as a crucial bridge between informal human reasoning and formal symbolic logic, enabling AI systems to participate meaningfully in mathematical problem solving. Its importance exemplified by DeepMind's AlphaProof, which achieved allver-medal-levw performance in the 2024 International Mathematical Olympiad by leveraging an end-to-end formalization pipeline based on the Lean theorem prover (AlphaProof & AlphaGeometry) 2024). As LLMs become central to auto- mated theorem proving, the accuracy and reliability automated formalization directly impact the overall success of proof generation.
"These authors contributed to the work equllly and should be regarded as co-first authors.
Corresponding author.

---

Published as a conference paper at ICLR 2026
Current mainstream approaches to automated formalization rely on Large Language Models (LLMs) to directly translate natural language into formal mathematical statements (Wu et al. 2022). Typical strategies include few-shot prompting of pre-trained models and fine-tuning
aligned natural lan- muage-formal language (NI.-FI) pairs (Xin et al. 2024). While recent systems, such as Herald (Gao et al., 2024b) and Kimina-Prover (Wang al.] 2025). have shown promising results, they continue to face two fundamental challenges. 1) Model hallucination arises when LLMs generate confident but incorrect formal code. Common failure modes include fabricating undefined concepts in Math- lib (Lean's 's standard library), misusing symbols due to informal reasoning, and producing outdated definitions incompatible with the latest Mathlib version. 2) Semantic gap stems from the mismatch between the ambiguity of natural language and the precision of formal languages. A key difficulty conceptual polymorphism, where identical expressions correspond to different formal definitions depending on context, domain, or abstraction level. This often leads to inaccurate formalizations, especially in applied fields like combinatorics, where essential entities are frequently implicit and hard to recover from surface text. Figure provides concrete examples of these dual challenges.
(x) Hallucination
Instruction
(b) Semantic
Anstruction
does eaist
Mattilll
Input
Mi-tatment
rust balkww ca
repedding the lowill of
Input
Al statment
bh rubgress prserntd anwerr stagoup movv soros ther
Nestic
Jos oo our then eito eachastaad touets
Coiver parerpee
Topelagion
R-statment
RL statment
Nattis
21 or 2i
Autoformaliar
Autoformallzer
Josn il dueiree Ciitccgg warey
unknown constant Subgroup.gementeedi
Mettchal
x
Eraor: failed synthesize TopologkaaSppoce P
U.N.V.
of cores for iiteeett 10- -opo Gulgoesaccoae 2o-1 sany
Thacrec mairs wightitteddd te peape Typart s0400:30 C dn Vo apege
Query
Koowledge Base
Definition
Input
Compllation passed. Semmentics confirmed cornect.
Teeikerdd space
Compilation passed. Semantics confirmed correct.
Autoformalizer
Figure 1: Examples illustrating model hallucination and semantic gap. Panel (a) demonstrates case of autoformalization failure due to the model fabricating undefined predicate in Mathlib, resulting in compilation errors. Panel (b) exhibits a semantic gap arising from the conceptual polymorphism of "ncighborhood" (defined differently in topological versus metric spaces) where the model fails to recognize the appropriate abstraction level, triggering type class synthesis errors during compila- tion. Panel (c) showcases correct formalization results generated by the CRAMF framework, which effectively resolves both issues through structured knowledge grounding and context-awar aware concept resolution.
In -eneral-domain natural language processing, similar challenges, such factual hallucination and context- context-sensitive sensitive ambiguity, are often addressed through Aatrieval-Augmentte Generation (RAG) (Gao et al. 2023b). By retrieving relevant external knowledge ground and guide model outputs, RAG has proven effective improving factual consistency and semantic precision across a range of tasks. Despite this success, the application of RAG mathematical automated formalization remains largely unexplored. This work investigates whether retrieval-based methods can be adapted improve the reliability and accuracy of LLM-driven formalization. However, directly applying RAG in this domain introduces new obstacles. First, unlike encyclopedic knowledge in the general domain, mathematical libraries such as Mathlib lack structured, queryable mappings from natural language expressions to formal definitions, making effective retrieval non-trivial. Second, resolving conceptual polymorphism requires not just retrieving related content, but disambiguating between multiple context-sensitive formalizations, task that standard RAG pipelines are not equipped to handle. These limitations call for domain-specitn retrieval augmentation tailored to the needs of formal reasoning systems.
To systematically address hallucination and semantic gap in Lean-based autoformalization, we pro- pose the Concept-driven Retrieval-Augmented Mathematical Formalization (CRAMF) frame- work. CRAMF enhances formalization accuracy by retrieving precise definitions of core mathe- matical concepts from Mathlib to provide contextual grounding for L.LM-based autoformalizers. At
2

---

Published as a conference paper at ICLR 2026
its core, CRAMF relies structured knowledge base that explicitly maps natural language pressions to their corresponding formal definitions. We define a schema for this concept-definition knowledge base that captures the many-to-many relationships between informal descriptions and formal representations. To support scalability and coverage, we design an automated pipeline that constructs the knowledge hase by aligning Mathlib definitions with diverse, canonical natural lan- guage expressions. To address conceptual polymorphism, CRAMF augments user queries with contextual signals and leverages hybrid retrieval strategy to improve definition disambiguation. By incorporating Nomain-specifie cues and application context, the system enhances its ability to distinguish between multiple candidate definitions of the same concept. combination of symbolic and semantic retrieval, followed by reranking, ensures accurate and context-aware retrieval of formal definitions.
In conclusion, our contributions are as follows:
We propose the Concept-driven Retrieval-Augmennte Mathematical Formalization (CRAMF) framework, which retrieves precise formal definitions of core mathematical concepts to provide contextual grounding for LLM-based autoformalization.
We define structured concept-definition knowledge base covering over 26,000 Math- lib definitions and 1,000+ core mathematical concepts, and develop automated LLM- powered pipeline to construct this resource by aligning formal definitions with diverse nat- ural language expressions,
We demonstrate that CRAMF serves a plug-and-play enhancement for LLM--bssed autoformalizers, consistently improving translation accuracy on miniF2F (Zheng et al.) 2021), ProofNet (Azerbayev al.) [202)), and our proposed AdvancedMath bench- mark achievini up to 62.1% % and an average of 29.9% relative improvement.
2
METHOD
This section presents the proposed Retrieval-Augmente Mathematical Formalization Frame- work (CRAMF). CRAMF operates under a retrieval-augmente paradigm: given a natural language description of mathematical theorem, first retrieves formal definitions of relevant concepts from a structured knowledge base, then supplies them as contextual grounding to an LLM-based autofor- malizer. This enriched context helps the model generate Lean code that is syntactically correct, semantically aligned with the theorem, and compliant with Mathlib specifications. We describe the framework through three main components: concept-definition knowledge base construction, math- ematical concept (Xtra and definition retrieval, which comprises the Dual- Daal-Pathway Hy- brid Retrieval (DHR) module and a reranking module. An overview of CRAMF is illustrated in Figure 2
Concept Knowledge
GRAMF-Gulded Autoformalization Process
Informalioor
Laa code cofinees funet on dedy computes
Informal statement
Dalnitoon
Hdettt 1
Dack-rrrr dis
mumaciio::
Mathilo
Definition
Notural langaae description
Corad Nardametii ratematee
The cerbatins function
Derivative
LLM
Rbutbask
Insruction:
Concept descriition
Concopt
tepir is-loloirr wow.rraiiieeee.. optooooi
MUMAORRT
Bucriove
FaTe Coprinel
Definition info
Concopt info
Semantic vector
Knowledge base
Figure 2: Overview of the CRAMF framework. (a) Construction of the concept-definition knowl- edge base via back-translation and concept extraction from Mathlib definitions. (b) Integration into autoformalization: extracted concepts retrieve relevant definitions to guide formal code generation.

---

Published as a conference paper at ICLR 2026
2.1
CONCEPT DEFINITION KNOWLEDGE BASE CONSTRUCTION
2.1.1 ONTOLOGY SCHEMA DESIGN
To support structured representation and efficient retrieval of Lean-based mathematical knowledge, we define lightweight ontology O and implement a corresponding relational database schema for storage and querying. The ontology is formalized quadruple:
O O= (C(,,P,A,R)
where C denotes the set of entity types, P is the set of attributes, A + P(P) is the attribute map- ping function that assigns to each entity type its associated attributes, and is the set of semantic relations. Here, P(P) represents the power set of P.
To explicitly eapture concept-definition mappings and support retrieval, we define the entity types as:
C O,,
where I' represents abstract mathematical concepts, O denotes formal mathematical definitions ex- tracted from Mathlib, and d consists of natural language annotations associated with those defini- tions. Each entity type is characterized by a set of attributes via the mapping functioon A, which serve as the logical basis for database fields: is characterized by the attribute triple (Ti: Na: Te). repre- senting the concept's name, domain, and explanatory description; θ is characterized by (fr, 0,,0,= 0p). denoting the definition's s identifier, formal expression, and module path; + is defined by the singular attribute &a representing definition's natural language annotation.
The relation set R defines the semantic links between entities:
R1 C l' P()),
R₂ : ④ +
where R1 establishes a one-to-many relationship between entity I and entity θ, signifying that single mathematical concept may correspond to multiple Lean definitions. R2 defines a one-to-one mapping between entity @ and entity Φ denoting that each formal definition corresponds to exactly one unique natural language explanation.
2.1.2 KNOWLEDGE BASE POPULATION
We automate the construction of the knowledge base by instantiating the ontology schema with specific record instances extracted from Mathlib. Guided by the attribute mapping function A. populate the three entity types C = {T. O, } and establish semantic relations R among them. We begin by parsing Mathlib using Lean 4's official documentation tool, doc-gen4, to extract all definitions declared via def, class, or structure. These populate the attributes of the Defimition 0 and Description & entities, including identifiers, formal representations, module paths, and associated annotations.
To instantiate the mathematical Concept entity I, we employ a reverse translation strategy using the pre-trained language model I-tthLMM (Ying et al. (022b)) Each formal definition is passed to the model to generate natural language descriptions. We apply a self-consistency valida- tion procedure improve generation quality, producing three candidate descriptions and selecting the one most semantically aligned with the original annotation. Subsequently, the selected natu- identify the
ral language description processed by a concept extraction model (DeepSeek-VS) underlying mathematical concept and generate an explanatory gloss. This final step completes the construction of the I' entity, Illustrative examples of this end-to-end process are shown in Figure
2.1.3 VECTOR ENCODING AND INDEX CONSTRUCTION
Considering that the MathBERT Peng et al. 2021 model is pre-trained based on large-scale math- ematical corpus, which helps to accurately capture the semantics of mathematical concepts, We employ it to perform semantic encoding on the % field of I and the 9, field of the descriptions in the knowledge base as follows:
4

---

Published as a conference paper at ICLR 2026
Definition
Back-translation
inredaciole, Föurkvsithin Set (Lik)
nonemrp
Soane
hestoerssaaenann E +4[)
input
Back-transiate
Let j te norred vertor space, ordie/ p
elce aoTeerantttoooeeetttttt then ciasstcal.ctorse h
realvakend
else
InternLMM2MMeth-76
Coneder funciin behoeen specee aadd ailociiall cuts denicllee
</>
corretyigg
Docstring
Mathilb
Cosine similarity
dertistive DihaaiveO.hhoiisee possitóe dericattee..
Encoder
Figure The example illustrates reverse translation of Lean's defintion of fderivWithin via InlemLMMplus7BB, with semantic similarity scoring against Mathlib annotations.
V/c (ath
Vd = MothBERT((.))
An efficient vector index is then built using Faiss (Douze et al. 2024). Ultimately, each knowledge unit is represented as the following quadruple:
(7h fr, Ve. va)
where "n the core mathematical concept; 0, is its corresponding Mathlib definition name; va and Ua are the respective semantic vectors.
2.2 CONCEPT EXTRACTION
In CRAMF, mathematical concept (Xtraction(MCEE serves as the bridge between natural language problem descriptions and formal definitions. The objective is accurately identify the core mathe- matical concepts from the input natural language theorem description, providing fundamental query units for subsequent definition retrieval.
Mathematical problems vary in explicitness: some contain explicit concept mentions, while others rely implicit mathematical structures. We therefore employ distinct extraction strategies.
For conventional proof problems explicitly containing mathematical concepts: We leverage the powerful comprehension capabilities of large language models (LLMs) to directly identify and ex- tract the core concepts within the mathematical theorem. For applied mathematics problems with implicit mathematical concepts: Their problem descriptions typically lack explicit mathematical concept keywords. For example, the combinatorial problem "Prove: Among any people, there are always least 3 people who either all know each other are all strangers each other" im- plicitly involves the mathematical concept of a graph. When handling such problems, we introduce an M.--- problem rewriting mechanism. During the concept extraction phase, this mecha- nism performs mathematical modeling and rewriting of the original problem to explicitly express its core mathematical structure before concept extraction proceeds. Details on prompt construction and examples provided in the appendix.
2.3 DEFINITION RETRIEVAL
Due to the conceptual polymorphism of mathematical concepts, the interpretation the same natu- rally described concept can vary actoss different abstraction levels and semantic granularities. With- out providing relevant context, LLMs struggle to confirm the precise formal definition correspond- ing mathematical concept when generating formal statements. To address this, we introduce two-stage retrieval process comprising query enhancement and dual- duat-ayy hybrid retrieval.
2.3.1
QUERY ENHANCEMENT
When a concept has multiple formal definitions, using solely the concept as the query can lead to excessive noise and low recall. We therefore enhance queries via conceptual parsing. Using L.MMs
5

---

Published as a conference paper at ICLR 2026
under strict prompting, we perform conceptual parsing of the mathematical theorem, generating an interpretation of terms based on the extracted core concepts and the existing theorem descrip- tion. The concept is then concatenated with this terminological interpretation to form the query. The model-generated interpretation incorporates domain information and application context for the concept, while also implying dependencies between concepts. Using this as the query enables matching richer semantics during retrieval, helping to mitigate inaccuracies caused by conceptual polymorphism and bridging the semantic gap between natural language descriptions and Mathlib's specialized definitions.
2.3.2 DUAL-PATHWAY HYBRID RETRIEVAL
We adopt collaborative strategy combining hybrid retrieval and reranking, integrating semantic vector retrieval with exact matching mechanisms to ensure retrieval results satisfy both semantic relevance and formal precision. Specifically, the system executes the following two retrieval path- ways in parallel:
Symbol-Level Keyword Matching: The LLM generates search keywords for the extracted core mathematical concept, which used for exact matching against Mathlib definition symbols via regular expressions, forming a base candidate set.
Semantic Similarity Retrieval: The query text, composed of the concept and its inter- pretation, is input into MathBERT encoder calculate its vector similarity with concept explanations in the knowledge base, initially recalling the Top-10 similar concepts. These are then reranked using the bge-reranker-v2-ng (Guo al. 2024) model filter the mantically most relevant Top-5 concepts. The definitions corresponding to these concepts are merged into the base candidate
To further optimize prompt quality, reranking mechanism is introduced. The bge-reranker-v2-m3 (Guo et al. 2024) model performs fine-grained semantic assessment of candidate definitions. By calculating the similarity between the conceptual interpretation within the query and the annotations of candidate definitions, it reranks the candidates. The Top-3 definitions with the highest semantic match are ultimately selected to constitute the context prompt for the automated formalization task.
EXPERIMENTS
In this section, we conduct experiments to address the following research questions: RQ1: How effectively does CRAMF framework improve compilation success rate and formalization accuracy in autoformalizing natural language mathematical theorems Lean 4? RQ2: How does CRAMF framework perform in definition retrieval compared to baseline retrieval methods? RQ3: What are the individual contributions of CRAMF's core components the final formalization performance?
3.1 EXPERIMENTAL SETUP
3.1.1 DATASETS
We evaluate our method on two public datasets (miniFF2 (Zheng al. 2021 and ProofNet (Azer- bayev et al. 2023)) ) and one proprietary dataset (AdvancedMath). AdvancedMath comprises 173 informal proof problems in higher mathematics. selected from the authoritative textbook "Advanced Mathematics (8th Edition)" published by Tongji University. It features standardized problem for- mulations and covers core areas such as spatial analytic geometry, vector algebra, series theory, and ordinary differential equations. In comparison to datasets like miniF2F and ProofNet, Advanced- Math presents a moderate level of difficulty and integrates logical reasoning, symbolic computation, and natural language understanding, making a suitable benchmark for evaluating the comprehen- sive capabilities of formal translation systems. We release this dataset publicly to support future research in this area F
"The dataset available at: htttp::////tthut www.aaa.iaooaaaaacaaaaaaaa

---

Published as a conference paper at ICLR 2026
3.1.2 BASELINE
Autoformalization Models We evaluate the effectiveness of the CRAMF framework against several baseline autoformalization models: the open-source autoformalizers HB (Gao et al. 2024b), Kimina-7B (Wang et al. 2025) and Goode--Formalizer-VV V2-8B (Lin et al. 2025), as well as the power- ful API-based LLMs DeepSeek-V3 V3 (DeepSeek et al. 2024), GPT-40, Gemini 2.5 Flash, and Claude 4.1.
Retrieval Models We evaluate several retrieval methods, including the standard RAG baselines BM25 Robertson et al. 2009), Rewrite-Retrieve Read (Ma et al. 2023), and HyDE (Gao et al. 2023a), as well as the LeanSearch (Gao et al. 2024a) and LeanExplore (Asher 2025 engines, which provide semantic search for Lean 4 declarations and mathlib4. We also include Dependency Retrieval (DR) (Liu et al., 2025), an open-source conoformalizaiinnorieneee model that employs dependency-basedt retrieval mechanism, to comprehensively compare definition retrieval capabilities across multiple datasets.
3.1.3 EVALUATION METHODS
Autoformalization Evaluation Given the prohibitive cost and limited scalability of manual eval- uation for large-scale experiments, we selected the evaluation pipeline from the Lean WorkBook project (Ying et al. 2024a). whereas manual assessment (Sidhu et al. 2024), despite offering deeper qualitative insights, was deemed impractical. Formalized outputs verified by the Lean com- piler. Results that compile successfully are then back translated into natural language descriptions using the semantic consistency between the back-translated statements and the original informal statements.
model (Ying al. (0024b). Finally, DeepSeek- V3 assesses the
Retrieval Performance Evaluation We evaluate retrieval quality using two metries: Average Con- tribution Score (ACS) and Relevant Definition Hit Rate (HitRate@K)) K).
1) Average Contribution Score (ACS) measures the overall relevance of retrieved definitions the target problem. Each retrieved definition is assigned a score from 0 to 3 based on its contribution to the formalization process. A score of 3 (Exact Match) indicates that the definition appears in the final formalized code, compilation succeeds, semantic consistency assessment passes, and the gen- erated Lean 4 expression closely aligns with the original problem. A score of 2 (Strong Relevance) is given when the definition is not used in the final code but is semantically or mathematically related to the problem statement, as judged by large language model. A score of (Weak Relevance) is assigned when the definition shares topical relevance but lacks direct semantic connection (also evaluated by an LLM). A score of 0 (Erroneous Reference) indicates that the definition appears in the code but either fails to compile or fails the semantic consistency assessment.
Scores of 3 and are assigned automatically using a combination of regular expression matching and the outcomes of compilation and semantic consistency verification. Scores of 2 and I are assessed using DeepSeek-R1: see the Appendix for prompts. Given a sample set T = {ti, f22 f2.,..f,, ), where each problem t; has set of retrieved definitions D;- {daa, d:2. dik }, the ACS is defined as:
D2
ACS
Score (dij, 4.)
Σ
Dr
where Score(diy, 4,) E {0, 1,2,3) denotes the contribution level of definition dy to problem t,.
2) Relevant Definition Hit Rate (HitRate@ K) measures whether at least one high-quality defini- tion appears among the Top-K K retrieved results for each problem. Specifically, we check whether any of the Top-K K definitions achieve score of 3. Formally, this metric is defined as:
HitRate@K
ni Σ
I
max Score 44) =
where n is the total number of problems and Z[.] is the indicator function (1 if the condition holds, O otherwise). In our experiments, we set K = 3. This metric captures the proportion of problems for which the Top- K retrieved definitions contain at least one that is strongly relevant or an exact match.
7

---

Published as a conference paper at ICLR 2026
Table 1: Compilation Pass Rate@ 10 of each base model (Orig.) versus the same model augmented with CRAMF on three datasets. RG (Relative Gain) represents the relative improvement rate.
MiniF2F
ProofNet
AdvancedMath
Model
Base
+CRAMF
RG
Base
+CRAMF
Base
+CRAMF
RG
Deepseek- V3
52.3%
69.3%
+32.5%
39.8%
53.1%
+33.4%
31.7%
48.2%
+52.1 %
GPT-4o
70.1%
82.7%
+18.0%
48.0%
62.6%
+30.4%
48.5%
59.1%
+21.9%
Gemini 2.5 Flash
82.4%
89.3%
+8.4%
70.9%
75.1%
+5.9%
79.3%
82.1%
+3.5%
Claude 4.1
95.1% %
98.0%
+3.0%
81.1%
85.6%
+5.5%
98 98.8%
99.4%
+0.6%
Herald-7B
79.1%
93.6%
+18.3%
60.9%
79.4%
+30.4%
80.0%
90.2%
+ 12.8%
BBB
98.8%
99.2%
+0.4%
87.4%
94.1%
+7.7%
98.8%
100%
+1.2%
Godel-V2-8B
99.6%
100.0%
+0.4%
85.6%
87.4%
+2.1%
98.8%
100%
+1.2%
Table 2: Formalization Accuracy Rate@1 of each base model (Orig.) versus the same model augmented with CRAMF on three datasets. RG (Relative Gain) represents the relative improvement rate.
MiniF2F
ProofNet
AdvancedMath
Model
Basc
+CRAMF
RG
Base
+CRAMF
RG
Base
+CRAMF
RG
Deepseok- V3
36.9%
47.1%
+27.6%
23.6%
37.0%
+56.8%
19.8%
32.1%
+62.1 %
GPT-4o
49.6%
60.1%
+21.2%
29.9%
42.2%
+41.1%
22.8%
34.7%
+52.2%
Gemini 2.5 Flash
72.1%
82.0%
+13.7%
57.0%
63.1%
+10.7%
43.9%
50.9%
+15.9%
Claude
83.6%
92.6%
+10.8%
72.2%
79.7%
+10.4%
57.2%
65.9%
+15.2%
Herald-7B
49.2%
63.1%
+28.3%
44.4%
55.1%
+24.1%
39.3%
51.4%
+30.8%
Kimina-7B
80.3%
84.8%
+5.6%
65.0%
69.3%
+6.6%
61.3%
66.5%
+8.5%
Godel-V2-8B
88.1%
95.1%
+7.9%
73.0%
80.2%
49.9%
57.8%
68.2%
+ +18.0%
3.2 AUTOFORMALLZATION PERFORMANCE (RQ1)
Our evaluation assesses CRAMF's impact on autoformalization models through two metrics: Com- pilation Pass @ate@ 10 (CPR @ 10) and Formalization Accuracy Rate (FAR 10). Comparative results (Table D and Table demonstrate that CRAMF universally enhances model performance, though the extent of improvement is architecture-dependder
Particularly notable are the substantial gains observed in the general large model DeepSeek- V3 with- out domain-specific fine-tuning, indicating that CRAMF effectively fills formalization knowledge gaps in general-purpose models through precise definition retrieval, constructing a "plug-and-play" formal knowledge bridge that substantially lowers the domain entry barrier. On the AdvancedMath dataset involving multiple complex concepts, the relative improvement rates for both compilation pass rate and formalization accuracy reach their highest values at 52. and 62. 1% respectively. The significant improvement in compilation pass rate confirms that injecting core mathematical concept definitions enables large models to express formal symbols with greater precision, while the enhancement in formalization accuracy reflects deeper semantic comprehension of mathematical problems.
3.3 KNOWLEDGE BASE AND RETRIEVAL PERFORMANCE (RQ2)
To assess the efficacy of the concept-definitio knowledge base and the hybrid retrieval strategy CRAME, we evaluate its performance accurately retrieving core mathematical definitions for theorem autoformalization.
Table and report the average contribution score (ACS) and the Top-3 hit rate (HitRate @3) of different retrieval frameworks across three datasets. As shown in both tables, CRAMF signif- icantly outperforms all baselines, achieving an average improvement contribution and up a 15 wewp-peeteeeepooiiee
more than 0.5 points in increase in HitRate@2 over the best- perforrinn baselines. Notably, CRAMF maintains robust performance on the AdvancedMath dataset, under- scoring its strong generalization capability in complex mathematical contexts.
8

---

Published as a conference paper at ICLR 2026
Table 3:
Average contribution scores retrieval methods on three
Table Top-3 hit rate of relevant defini- tions (HitRate@3)) for each retrieval frame- work across three datasets.
(ACS) of
datasets.
Method
MiniF2F ProofNet
AdvancedMath
Method
MiniF2F
ProofNet AdvancedMati
BM25
0.91
0.94
0.83
BM25
11.3%
14.5%
9.1% 1
R3
1.38
1,45
1.31
R3
19.6%
21.1%
15,4%
HyDE
1.55
1.61
1.52
HyDE
32.4%
35.5%
30.7%
LeanExplore
1.42
1.51
1.35
ExpoEe
31.5%
37.7%
23.8%
LeanScarch
1.58
1.63
1.56
LeanScarch
36.8%
42.3%
35.1%
DR
1.39
1.47
1.26
DR
32.6%
33.8%
28.5%
CRAMF
2.07
2.14
1.93
CRAMF
44.2%
50.6%
42.9%
Table 5: Ablation results of CRAMF submod- ules evaluated by FAR 10.
Table 6: Effect of structured problem rewriting on FAR@ @ 10 over 241 combina- torics problems in CombMath.
Method
MiniF2F
ProofNet
AdvancedMath
CRAMF
63.1%
55.1%
51.4%
Method
CombMath
w/o MCE
58.2%
49.8%
44.0%
CRAMF 63.1%
w/o DHR
48.5%
36,8%
37.1%
w/o ReWrite
54.3%
w/o Rerank 54.3%
47.5%
43.9%
In contrast, BM25 relies on surface-level keyword matching, making difficult distinguish between the semantic variations of the same concept across different levels of abstraction. The Seerite-Reerieve-RReee approach improves upon BM25 by enhancing recall implicitly mentioned concepts through query rewriting, yet it still falls short of satisfying the symbolic precision required by Lean. While HyDE achieves better ACS than the preceding baselines, it is prone to hallucination, often retrieving incorrect definitions that ultimately limit its practical utility. Although LeanSearch and LeanExplore serve as semantic search engines tailored for the Lean environment, their retrieval results primarily return theorems rather than definitions. While they achieve higher HitRate @3 than traditional RAG methods, they still exhibit limitations in handling cross-domain and polymorphic concepts. On the other hand, Dependency Retrieval (DR) leverages dependency associations among formal objects in the Mathlib for retrieval. Although this design can capture topological connections between definitions, is inherently constrained by surface-level syntactic structures. The depen- dency graph struggles to model the deep semantic correspondence between natural language and formal concepts, resulting in suboptimal retrieval performance despite being explicitly trained for autoformalization. These limitations highlight the advantages of CRAMF's structured knowledge base and hybrid retrieval mechanism in ensuring both semantic relevance and formal accuracy.
3.4 ABLATION STUDY (RQ3)
To dissect the individual contributions of key submodules within the CRAMF framework, particu- larly considering the condition-triggeres problem rewriting mechanism in our retrieval pipeline, we conduct structured ablation study across two experimental settings. 1) On three general datasets, we evaluate the impact of three core components: Mathematical Concept Extraction (MCE), Dual- Pathway Hybrid Retrieval(DHRR) and reranking module. 2) We assess the effectiveness of the rewrit- ing mechanism in handling problems characterized by high representational abstraction and implicit terminology using CombMath] Using Herald-7B (Gao al., 2024b) as backbone generation model, We summarize the ablation results on the general datasets in Table 5 The removal of the DHR module Icads to a substantial decline of 15.7% in average FAR, underscoring the necessity of simultaneously capturing semantic relevance and symbolic precision in mathematical formal envi- ronments. The MCE module also proves indispensable, with its removal causing a 6-7 percentage point reduction in FAR, demonstrating that providing domain knowledge and application contexts for mathematical concepts effectively resolves definition ambiguity. Furthermore, as shown in Ta-
'The dataset of 241 combinatorics problems is derived from Combinatorics: The Art of Counting (Sagan, 2020), authoritative source covering core subdomains like enumerative combinatorics and combinatorial design.

---

Published as a conference paper at ICLR 2026
ble 6 activating the rewriting module yields 8.8% improvement in FAR, validating the utility of our conditionally-triggee rewriting strategy for semantic modeling mathematically complex scenarios.
4 RELATED WORKS
4.1 AUTOFORMALIZATTOO
Autoformalization refers the process transforming informal mathematical statements into for- mally verifiable representations (Jiang et al. [023 Poiroux et al. [2244] Wang et al. 2020 Tian et al.
2025 Li et al. 2025). Existing approaches can be broadly categorized into bule-based and LLM- based methods. Rule-based methods leverage explicit logical and syntactic rules ( (Weng al. 2025
often adopting controlled natural languages (e.g.. Mizar (Rudnicki) 1992), ForThel. (Vershinin & Paskevich 2000)) grammatical frameworks (e.g., GF (Pathak 2024)) construct abstract syntax trees that are then translated into formal code. In contrast, LLM-based approaches utilize few-shot prompting (Wu al. 2022) fine-tuning aligned natural language-formal language (NL-FL)
pairs (uuejun et al. 2025).
4.2 RETRIEVAL-AUGMENTER GENERATION
Serieval-Augmentee Generation (RAG) enhances LLM outputs by integrating external knowledge retrieved in response to the input query, thereby reducing hallucinations and factual errors (Li et al.) 2024). In the context of formal reasoning, RAG has been applied mathematical autoformalization and verification tasks. Azerbayev al. (2023) propose augmeetel-agmmeeted formalization method that selects prompt-relevant statements to improve proposition generation. RAutoformalizer Liu al. (2025) adopts vetrieval-basee augmentation support statement-level formalization. Similarly, ReProver Yang et al. 2023) incorporates a premise selection module that filters relevant auxiliary statements from large formal corpora aid theorem generation. In closely related vein, (Tao et al. (2025) introduce a lightweight premise retrieval model trained on Mathlib4, which employs tokenizer specifically designed for formal language and fine-grained similarity measure to enhance retrieval accuracy in Lean-bass based theorem proving.
5 CONCLUSION
This paper proposes CRAME, a concept-driven retrieval-augmented framework for mathematical formalization. By leveraging structured knowledge base from Mathlib4 and tailored retrieval pipeline, CRAMF effectively mitigates model hallucinations and semantic inprecision, signifi- cantly improving formalization accuracy across diverse benchmarks. Future work may extend to more complex mathematical domains and explore cross-library, multi-step reasoning, and feedback- incorporated retrieval augmentation strategies.
REPRODUCIBILITY STATEMENT
To ensure the reproducibility of our work, have included the complete source code in the sup- plementary materials. An anonymized version of the code also available at the following link: https://giit thub. com/ www.kaaawiiia..... CRAMF The detailed experimental setup, hyperparam- eters, and prompts used for the large language models are provided in the appendix.
ACKNOWLEDGMENTS
This research was funded by the National Natural Science Foundation of China (Nos. 62272093, 62137001)
REFERENCES
Team AlphaProof and Team AlphaGeometry. Ai achieves silver-medal standard solving interna- tional 178 mathematical olympiad problems. DeepMind blog, 179:45, 2024.
10

---

Published as a conference paper at ICLR 2026
Justin Asher. Leanexplore: A search engine for lean 4 declarations. arXiv:2506. 1085, 2025.
arXiv preprint
Zhangir Azerbayev. Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leww mathemat- ics (2023). arXiv preprini arXiv:2302.124: 2023.
AI DeepSeek, Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Cheng- gang Zhao, Chengqi Deng, Chenyu Zhang, et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437, 2024.
Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Pierre- Emmanuel Mazaré, Maria Lomeli, Lucas Hosseini, and Hervé Jégou. The faiss library. arXiv preprint arXiv:2401.08281, 2024.
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. arXiv preprint arXiv:2403. 13310, 2024a.
Guoxiong Gao, Yutong Wang, Jiedong Jiang. Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. arXiv preprini arXiv:2410. 2024b.
Luyu Gao. Xueguang Ma, Jimmy Lin, and Jamie Callan. Precise zero-shot dense retrieval without relevance labels. In Proceedings of the 61 Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 7762-1777 2023a.
Yunfan Gao, Yun Xiong, Xinyu Gao, Kangxiang Jia, Jinliu Pan, Yuxi Bi, Yixin Dai, Jiawei Sun, Haofen Wang, and Haofen Wang. Retrieval-augmented generation for large language models: A survey, arXiv preprint arXiv:2312.10997, 2(1), 2023b.
Jun Guo, Bojian Chen, Zhichao Zhao, Jindong He, Shichun Chen, Donglan Hu, and Hao Pan. Bkrag: A bge reranker rag for similarity analysis of power project requirements. In Proceedings of the 2024 6th International Conference on Pattern Recognition and Intelligent Systems, pp. 14-20, 2024.
Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant tutorial. Rapport Technique, 178:1 13, 1997.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311 11223311..333 1.03755, 2023.
Jiarui Li, Ye Yuan, and Zehua Zhang. Enhancing 11m factual accuracy with rag to counter hallu- cinations: A case study on domain-specific queries in private knowledge-baad basees.. arXiv preprint MrXi::240311044, 2024.
Sirui Li, Wangyue Lu, Xiaorui Shi, Ke Weng, Haozhe Sun, Minghe Yu, Tiancheng Zhang, Gen- sitskiy Yu., Hengyu Liu, and Lun Du. Msc-180, A benchmark for automated formal the- orem proving from mathematical subject classification. ArXiv, abs/2512.18256, 2025. URL
semant htt.:/awww...cccoo...ooooooooooa :1:20077111
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint 1:Xiv:2508.036/1 2025.
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards faithful metric and a dependency retrieval-base approach. In The Thirteenth International Conference Learning Representations, 2025.
Xinbei Ma, Yeyun Gong, Pengcheng He, Hai Zhao, and Nan Duan. Query rewriting in retrieval- augmented large language models. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 5303-5315, 2023.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction-CAle 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
11

---

Published as a conference paper at ICLR 2026
Shashank Pathak. Gflean: An autoformalisation framework for lean via gf. arXiv preprint arXiv:2404.01234, 2024.
Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994.
Shuai Peng, Ke Yuan, Liangcai Gao, and Zhi Tang, Mathbert: A pre-trained model for mathematical formula understanding. arXiv preprint (tt:::20050003770 2021.
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut, Improving autoformalization using type checking. arXiv preprini arXiv:2406.07222, 2024.
Stephen Robertson, Hugo Zaragoza, et al. The probabilistic relevance framework: Bm25 and be- yond. Foundations and Trends@ in Information Retrieval, 3(4):333-389 2009.
Piotr Rudnicki. An overview of the mizar project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp- 311-330, 1992.
Jasdeep Sidhu, Shubhra Mishra, Aryan Gulati, Devanshu Ladsaria, and Brando Miranda. An evalu- ation benchmark for autoformalization in lean4. In The Second Tiny Papers Track at ICLR 2024, 2024.
Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Learning an effective premise re- trieval model for efficient mathematical formalization. In 2nd Al for Math Workshop@ ICMI. 2025, 2025.
Yuchen Tian, Ruiyuan Huang, Xuanwu Wang. Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, and Lun Du. Evolprover: Advancing automated theorem proving by evolving formalized problems via symmetry and difficulty. arXiv preprint arXiv:2510.00732, 2025.
Konstantin Vershinin and Andrey Paskevich. torthel-the language of formal theories. Interna- tional Journal of Information Theories and Applications, (13::120-12,, 2000.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprini arXiv:2504. 1154, 2025.
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs, pp. 85 98, 2020.
Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang Aut- oformalization in the era of large language models: A survey, arXiv preprint arXiv:2505.2344 23486, 2025.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in neural informa- tion processing systems, 35:32353-32368. 2022.
Huajian Xin, Daya Guo, Zhihong Shao, ZZ Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Advancing theorem proving in Ilms through large-scale synthetic data, In The 4th Workshop Mathematical Reasoning and Al at NeurlPS 24, 2024.
Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haox- iong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, et al. Mathesis: Towards formal theorem proving from natural languages. arXiv preprint arXiv:2506.074 070450 2025.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. Advances Neural Information Processing Systems, 36:21573- 21612, 2023.
Huaiyuan Ying, Zijian Wu, Yihan Geng. Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in Neural Information Processing Systems, 10110088888-88666 2024a.
12

---

Published as a conference paper at ICLR 2026
Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong. Kuikun Liu, Ziyi Wang, et al. Internlm-mate math: Open math large language models toward verifiable reasoning, arXiv preprint arXiv:2402.06335, 2024b.
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. Minif2f: cross-system benchmark for formal olympiad-level mathematies. arXiv preprint arXiv:2109.001 10, 2021.
A ADDITIONAL EXPERIMENTAL RESULTS
A.1 STATISTICAL SIGNIFICANCE TESTS
To verify whether the performance gains brought by the CRAMF framework are statistically sig- nificant across diffferent models and datasets, conduct the Wilcoxon signed-rank test to compare each model's performance with and without CRAMF.
The Wilcoxon signed-rank test is non non-parametric statistical method used for analyzing differences between two paired samples. It is particularly suitable for our setting: evaluating the same model under two conditions (Base +CRAMF)
per-problem basis.
We encode the performance on each sample (mathematical problem) as a binary outcome: if at least of the Top-10 generated results passes the semantic consistency check, the sample is considered successful (assigned 1); otherwise, is considered unsuccessful (assigned O). These paired binary results are then used assess the performance difference.
We use FAR @ 10 as the evaluation metric. Each question in a dataset constitutes one sample, and each sample has two associated binary values (Base vs. Base+CRAMF). The statistical test proceeds as follows:
Compute the difference for each paired sample.
2. Discard pairs with zero difference; rank the remaining pairs by absolute difference.
3. Calculate the sum of ranks for positive and negative differences; the Wilcoxon test statistic is the smaller of the two.
4. Given a significance level of = 0.01, compute the corresponding p-value.
A.1.1 RESULTS
As shown in Table all p-values are below the significance threshold a = 0.01, indicating that the observed improvements statistically significant across all evaluated settings. The CRAMF frame- work achieves statistically significant improvements on most model-dataset combinations. General- purpose models such DeepSeek-V V3 and GPT-4o benefit the most, indicating that CRAMF ef- fectively supplements their lack of mathematical domain knowledge. Even for high- regh-perfoming customized models like Kimina-7B, CRAMF still yields lightweight but significant gains. These results demonstrate that CRAMF provides systematic enhancement to mathematical formalization, rather than accidental variation.
A.2
CASE STUDY
This subsection demonstrates the efficacy of CRAMF in improving automated formalization curacy through comparative analysis of baseline failure cases versus CRAMMF-uggentted success cases.
A.2.1 EXAMPLES FROM THE COMBINED DATASET THAT REQUIRE TRIGGERING THE REWRITING MECHANISM
This part demonstrates the operational workflow of the rewriting mechanism when handling mathe- matical problems lacking explicitly stated concepts.
13

---

Published as a conference paper at ICLR 2026
Wilcoxon signed-rank results comparing Base and +CRAMF across models and datasets. Each row corresponds to one model-dataset pair. The Base (%) and +CRAMF (%) columns show the @ 10 performance without and with CRAMF, respectively. n indicates the number of samples (math problems) in the dataset. The Wilcoxon column gives the signed-rank test statistic (smaller the rank sums), and the p-value column reports the corresponding p-value. All y-values are below the significance threshold 0.01, confirming that the observed gains are statistically significant.
Table 7:
Model
Dataset
Base (%)
+CRAMF (%)
Wilcoxon
p-value
DeepSeek- V3
miniF2F
244
36.9
47.1
78
2.7e-04
DeepSeek-V.
ProofNet
373
23.6
37.0
1834
2.0e-08
DeepSeek-V3. V3
AdvancedMath
173
19.8
32.1
586
8.1e-06
GPT-4o
miniF2F
244
49.6
60.1
1121
6.3e-04
GPT-4o
ProofNet
373
29.9
42.2
1905
1.7e-07
GPT-4o
Math
173
22.8
34.7
524
4.1e-05
Herald-7B
miniF2F
244
49.2
63.1
595
3.0e-09
Herald-78 7B
ProofNet
373
44.4
55.1
820
1.0e-10
Herald-7B
MdvancedMath
173
39.3
51.4
231
2.0e-06
Kimina-77 7B
miniF2F
244
80.3
84.8
66
4.5e-04
Kimina- 7B
ProofNet
373
65.0
69.3
106
1.6e-04
Kimina- 7B
AdvancedMath
173
61.3
66.5
45
1.3e-03
The Case for Rewrite mechanism
NL-statement:
Prove that among any 10 people, if there do not exist 3 people who are all mutually unacquainted, then there must exist people who all know each other. Likewise, if there do not exist people who are all mutually acquainted, then there must exist people who are all mutually unacquainted.
Rewrite:
Let be complete graph where each edge colored red (acquaintance) or blue (non-aqquaintance) Prove that: If there no blue triangle the graph, then there must exist red If there triangle, then there must
blue.
Abstract concept: Complete Graph, Edge-coloring, Ramsey theory, Monochromatic Subgraph, monochromatic triangle
Figure 4: Example from the rewriting mechanism
Figure demonstrates the need for the rewriting mechanism when mathematical concepts are im- plicit. The original informal statement lacks formal terms like "grap" or "Ramsey theory". Rewrit- ing models it as a complete edge-colored graph, enabling the extraction of key abstract concepts and bridging informal language with formal mathematical representation.
A.2.2 THE CASE THAT FAIL TO COMPILE IN THE LEAN COMPILER
This part presents failure cases in automated formalization that fail Lean compilation, alongside comparative cases demonstrating successful compilation after CRAMF integration.
14

---

Published as a conference paper at ICLR 2026
Baseline Formalization
NL-statement:
Let f:R R be a continuous periodic function with period 7 Prove
that:
1. J. [())do S f(t)
2. L: f(a)do =n (())dz, nEN
FL-statement:
theorem int_ ____addd________________________ eq_ext (f: IR > (R) (T: IR) (a IR) (n: N) Function CoattionCoontiuuuus f f= (fun (x T)) - ʃ (x IR. a..a
+, (x: R. 0..T, fx := sorry
Compilation error: unknown identifier
Figure 5: Baseline formalization failure case.
Figure 5 shows without retrieval augmentation of relevant concepts and definitions, the model attempted formalize the concept of function continuity by inventing an identifier Func- tion. Continuous based solely on its natural language interpretation. However, since this identifier does not exist the Mathlib library, the compiler raised error indicating that the symbol could not be resolved.
CRAMF-Augmented Formalization
Context:
"name": "ContinuousOn",
"comments": "A function between topological spaces is continuous on subset 's 'when it's continuous at every point of 's' within 's'."
"definition": "@(fun__ppae __opp_]p]]]]]p def ContinuousOn (f: > Y) (s Set X) Prop
x s, ContinuousWithnnAt xs
FL-statement:
theorem integral_ eq_ intervallnteeral [NormedAtdCCommGroup E] (NormedSpace R E] (f: > E) (T R) (h ContinuousOn (Set.lcc
0 TT)) f (x: (8) Set.Icc T, (x R) in (Set.lco 0 T), fx sorry
Compilation Result: Pass
Figure DRAMMFaugmentie success case.
Figure 6 illustraaes that after incorporating the correct definition corresponding to function continu- ity, namely ContinuousOn, the model able to generate syntactically and semantically valid formalization based on the retrieved contextual information. As a result, the generated Lean code compiled successfully.
15

---

Published as a conference paper at ICLR 2026
Baseline Formalization
NL-statement:
Prove that if is normal subgroup of G prime index P, then for all G either K & H or G IIK and K:KNH
FL-statement:
theorem normal of index _i__i____s___ prime (G Type*) [Group G] (H K Subgroup G} (hH H.Normal) (hG Group.index H G p) :K H VG= H K) A (K in.index p sorry
Compilation error: unknown constant 'Group.index'
Figure 7: Baseline formalization failure case.
Figure illustrates that due to the absence of necessary contextual knowledge or definitional sup- port, the model failed correctly reference the Mathlib implementation of the concept "index of subgroup". and instead produced the undefined constant Group. index. Since this identifier does not exist library, the Lean compiler was unable to resolve it, resulting compilation failure.
CRAMF-Augmented Formalization
Context:
"name": "Subgroup.index",
"comments":
The index a subgroup as a natural number.
Returns '0' if the index is infinite."
"definition": @ rrd_iddi "The index of an additive subgroup as natural number. Returns 0 the index infinite.") "]
noncomputable def index : N :=rat.card (G H)"
FL-statement:
theorem exists
exists_subeeeeeete subgroup of _a__ooo_nnddee index Type*) [Group G] (n N) (hn Nat.card G) H:: Subgroup H.index sorry
Compilation Result: Pass
Figure 8: CRAMF-augmentne success case.
Figure shows that with the support of the CRAMF framework, the model was provided with both the precise definition of the subgroup index, Subgroup index, and accompanying semantic annota- tions. Consequently, during formalization, the model correctly referenced the well-defined constant Subgroup index, enabling the compiler resolve H. indde and pass type checking.
A.2.3 THE CASE THAT FAIL. THE SEMANTIC CONSISTENCY TEST
This part presents cases where the formalization results pass Lean compilation but fail the semantic consistency test. We provide detailed analysis of the underlying causes and further demonstrate the effectiveness of the CRAMF framework by comparing these results with those generated using CRAMFF-nnhaced inputs.
16

---

Published as a conference paper at ICLR 2026
Prompt for Rewrite mechanism
NL-statement:
Prove that the improper integral J. diverges when ps1.
converges when p>1, and
FL-statement:
theorem J (x: R) in Set.loi a, /x p sorry
htt.dd/rooweeeattteeeeeee (a:: (p:p :
Compilation result: pass
Back translation:
Prove that x²
0 for 1<
Semantic test result:
different.
Figure 9: Baseline formalization failure case.
Figure shows that without relevant contextual definitions, the model generated a Lean-compilable statement that failed capture the full semantics of the original problem. It only addressed conver- gence for > 1, omitted divergence for S 1, and used the incorrect interval (a, +o0) instead of (0,y). These omissions caused semantic inconsistency in the back- tark--ranslttoon test.
CRAMF-Augmented Formalization
context:
"name": Fellter.Tendst",,
"comments": " "Filter.Tendstee the generic 'limit of function' predicate. 'Tendsto f l2' asserts that for every 'Ia' neighborhood 'a', the 'f -preimage of 'a' is an 'l'' neighborhood."
"definition": "def Tendsto (f: a >> B) (l Filter a) (lz Filter B) :=\n h.map ft
FL-statement:
theorem integral eq_ intervallntegral
(V > 1, L: R, Tendsto (A y J x in (0).., p/x*p) atTop (V L)) An (V ps 1,s1,-a1 3 IR, Tendsto (A y => J in (0).., 1/x*p) atTop
(Nr L)) := by sorry
Compilation result: pass
Back-translation:
dr converges if p>> land diverges if p p
Prove that x²
Semantic test result:
same.
Figure 10: TRAMF-auumente success
17

---

Published as a conference paper at ICLR 2026
Figure 10 shows the CRAMF-augmentt formalization, which contrasts with the baseline result shown In Figure By introducing the key concept of function limit' using the precise definition Filter: and its semantic context, the model correctly expresses convergence behavior, distin- guishes between the convergent case (p > 1) and divergent case (p s 1), and uses the appropriate interval integral S= This better captures the nature of the improper integral described in the original natural language. As a result, the formalization both compiles and preserves semantic align- ment with the original problem.
Baseline Formalization
NL-statement:
Prove that the lim for any constant c.
FL-statement:
theorem const_lim lim (c: BJ (Xo :R: (Ve30...666 [x-Xol < - |c cl <) =
Compilation result: pass
Prove that the constant sequence converges
Semantic test result:
different.
Figure 11: Baseline formalization failure case.
CRAMF-Augmented Formalization
Context:
"name": "Filter.Tendstor
"comments": "Filter.Tendste the generic 'limit a function' predicate. 'Tendsto f la' asserts that for every 'lz' neighborhood 'a', the 'f -rreimage 'a' is an 'I'' neighborhood."
"definition": "def Tendsto (f: a >> B) (h Filter a) (l: Filter B) :=\n
1,.map fs
FL-statement:
theorem conddttocoons_nhdssss (c a) (Xo a} [TopologicalSpace a] Telddto (fun => c). Xo) (nhds c) := sorry
Compilation Result: Pass
nackttranslation:
Prove that the constant function/ (x) = eis continuous at point
Semantic test result: same.
Figure 12: TRAMF-augmente success
18

---

Published as a conference paper at ICLR 2026
Figure 11 shows different failure case. In the original natural language description, the limit is taken as - 2o, where the expression under consideration is a constant function f(z) c. That is, the function is independent of z, and the goal is to prove that the limit of constant function at any point equals the constant itself. However, in the model's s translation, it misinterpreted the problem as concerning the limit of sequence and failed recognize the underlying mathematical concepts of "constant function" and "function limit." Consequently, the back-transie mack-translation deviated semantically from the original statement, and the semantic test was passed.
By contrast, Figure 12 illustrates that with the integration of the CRAMF framework, we identified the core mathematical concept of function limit" from the original proposition and explicitly pro- vided its corresponding definition from the Mathlib library. With this contextual support, the model generated correct formalization and was able translate back into the constant function is con- tinuous at any point." Mathematically, continuity of a constant function at every point is equivalent the existence of the function's s limit at every point and that the limit equals the function value. Therefore, the semantic equivalence was preserved.
The above case studies demonstrate that the CRAMF framework not only enables accurate extraction of implicit mathematical concepts, but also effectively identifies their semantically aligned defini- tions in Lean 4. By providing essential contextual information to the autoformalization models, CRAMF significantly reduces both compilation failures and semantic inconsistencies.
B EXPERIMENT SETUP DETAILS
This section documents the precise hardware configurations and software dependencies used across experiments. We ensure reproducibility by specifying model parameters, runtime environments, and system specifications.
B. MODEL PARAMETER CONFIGURATION
This section details the experimental inference configurations and software dependencies, docu- mented in Table and Table
Table Inference configurations for all models.
Model
Deployment Con-
Sampling Parame-
figuration
ters
dtype=
temperature=0.7
Herald-7B
max tokens=1024
n=10
lensor_parallelssiz--
temperaturc=0.6
top-p=0.95
Kimina-7B
max max_Looens=2048
n=10 repetition repetition.penalyye 1en
dtype="bfloat
lemperature=0.11
InternI.M M-Mtth--
max 100
tensor parallel size=1
B.2 RUNTIME ENVIRONMENT CONFIGURATION
To ensure consistency and reproducibility of experimental results, all models were evaluated under the same hardware and software setup, detailed below. All experiments were conducted on server equipped with:
GPU: 4XNVIDIA A800 80GB PCLe
GPU memory: 80GB per card (total 320GB)
Operating mode: PCIe Gen4, NVLink not enabled
19

---

Published as a conference paper at ICLR 2026
CPU: AMD EPYC 7R32 (128 cores 256 threads)
System memory: ITB DDR4 ECC RAM
The software stack used for all experiments is summarized in the Table
Table Software versions and configuration used in the experiments.
Category
Version Configuration
Operating System (Ubuntu)
22.04 LTS (Kernel 6.5.0-44-generic)
GPU Driver (NVIDIA)
535. 17104
CUDA
12.2
Python
3.10.12
PyTorch
2.1.0
vLLM
0.3.2
Transformers
4.36.2
Lean Compiler
4.20.0-re5 (x86.64-linux-gmu)
Elan Version Manager
4.1.2
Mathlib4
(canprovrr/can4444..00000.
C PROMPT
This section details all prompt templates employed for core tasks, including problem rewriting, con- cept extraction, concept analysis, autoformalization, back-translation, and semantic scoring. Each prompt is explicitly structured to guide LLMss formalizing mathematical problems or analyzing concepts under striet output constraints.
C.1 PROMPT FOR REWRITE MECHANISM
For mathematical problems lacking explicitly stated concepts, employ the DeepScek-RI model to perform mathematical modeling and problem rewriting via the following structured prompt tem- plate, rendering them amenable to formalization:
Prompt for Rewrite mechanism
You mathematics expert specializing mathematical modeling and analysis of applied mathematical problems (e.g., combinatorial mathematics).
When given user's problem description:
Perform mathematical modeling by rewriting the problem to explicitly express all involved mathematical concepts (e.g., sets, functions, equations, probability)
2. Preserve the core requirements of the original problem.
Use formal mathematical language in English.
Output ONLY the rewritten problem text without any explanations additional content.
Rewrite the following mathematical problem, explicitly formalizing all mathematical concepts: (problem)
Figure 13: Prompt for Rewrite mechanism.
20

---

Published as a conference paper at ICLR 2026
C.2 PROMPT FOR BACK-TRANSLATION
The prompt for reverrn-n Lean4 formal specifications into natural language descriptions using the InternLM-Math-711 model is provided below.
Prompt for Back-translate
[UNUSED TOLP__TOEE___L__ 1_66]_4eerrrrr
Convert the formal statement into natural language:
"llean (code)
Figure 14: Prompt for Rewrite mechanism
C.3 PROMPT FOR CONCEPT ANALYSIS
We use DeepSeek- V3 to perform concept analysis existing mathematical concepts, with the fol- lowing prompt template:
Prompt for Concept analysis
You are a mathematics expert specialized in mathematical terminology and concise explanations. Provide professional one-sentence explanation for the following mathematical concept. Requirements:
1. Explanation must be concise while preserving key information.
2. Use standard mathematical terminology.
3. Output ONLY the English explanation without any additional content.
Example format:
Input: maximal value
Output: A local maximum a function at a point a its value f(a) that all other f(x) within some neighborhood of a.
Concept explain: (concept)
Figure 15: Prompt for Concept analysis.
C.4 PROMPT FOR CONCEPT EXTRACTION
For concept extraction from mathematical definitions or problems when building knowledge bases, use DeepSeek- V3 with this prompt:
21

---

Published as a conference paper at ICLR 2026
Prompt for Concept extraction
Analyze the given mathematical theorem description and:
1. Extract fundamental mathematical concepts (e.g.,
"derivative", "integral", "vector space", "group theory").
2. Identify the most relevant mathematical domain (e.g., "Calculus", "Algebra", "Geometry").
Return JSON format: f"concepts": ["...",... ...J, "domain": "...""
Analyze this mathematical theorem description: [description]
Figure 16: Prompt for Concept extraction.
C.5 PROMPT FOR SEMANTIC SCORING
To evaluate retriever performance, we score semantic relevance between definitions and mathemat- ical problems using deepseek-RI.
Prompt for Semantic relevance scoring
You are mathematical relevance assessment expert. Your task is evaluate the semantic relationship between mathematical definitions and problem statements based on strict scoring criteria. Provide J5ON-formatted output with score and rationale.
For the problem statement: {problem_statemen
Evaluate the relevance of this definition: (mathematical )
Scoring criteria:
1. points (strong relevance):
Demonstrates direct semantic connection to the problem domain.
Exhibits clear mathematical significance.
2. point (weak relevance):
Shows thematic relationship to problem domain. Lacks direct semantic linkage. Lacks formal mathematical utility.
Figure 17: Prompt for Semantic scoring.
C.6 PROMPT FOR AUTOFORMALIZATION
The prompt for automated formalization in the Hearld and Kimina models is shown below.
22

---

Published as a conference paper at ICLR 2026
Prompt for Autoformalization
[UNUSED SOOUSE 146]user
Task: Convert following problem into LEAN
ceatural_langueee s JUNUSE__TOKEN_AA
[UNUSED TOKEN 146jassistant
Here is the formal statement in LEAN 4:
llean
theorem
Figure 18: Prompt for Autoformalization.
C.7 PROMPT FOR AUTOFORMALIZATION WITH CRAMF
The prompt augmented with pertinent definitional information presented below.
Prompt for Autoformalization with CRAMF
[UNUSED JUNUEEDTOOKEN TOKEN_146Juser
Task: Convert the following problem into LEAN 4 code. Use the mathematical definitions provided below for reference, but NOT translate the definitions themselves.
Problem to translate: (problem)
Reference definitions (for context only):
(context_entries]
[UNUSED_TOKEN 145]
[UNUSED TOKEN 146]assistant
Here is the formal statement in LEAN 4: "lean4 theorem
Figure 19: Prompt for Autoformalization with CRAME
D LARGE LANGUAGE MODEL USAGE
This paper was prepared with the assistance of large language model. Our use of the LLM was strictly limited to the linguistic polishing of the manuscript. The process was as follows:
We completed a full draft of the paper, containing all key contributions.
Selected passages where the phrasing was perceived to unclear or inelegant were identi- fied.
These passages were input into the LLM with instructions to suggest alternative phrasings for improved clarity and flow, while strictly preserving the original technical meaning.
We critically reviewed, modified as necessary, and approved every suggestion before its incorporation into the final manuscript.
23

---

Published as a conference paper at ICLR 2026
The LLM played role in the conception of the research, the formulation of hypotheses, the design and execution of experiments, data analysis, or the interpretation of results. Its function was analo- gous to that of sophisticated proofreading tool. We hereby affirm that they solely responsible for the entire scientific content and the accuracy of all statements in this work.
E ANALYSIS OF SYSTEM LATENCY AND CONTEXT BUDGET
We systematically examined the performance of the CRAMP framework in terms of system latency and context budget, aiming to comprehensively evaluate its efficiency and scalability in practical deployment.
E. DELAY ANALYSIS OF EACH MODULE OF THE SYSTEM
We conducted fine-grat fin-grained breakdown the end-to-end latency CRAMF under batch size of 1, using hardware setup of 4 x NVIDIA A800 80GB GPUs. The results are summarized in the Tō We report the mean, standard deviation, minimum, and maximum latency each CRAMF module to comprehensively characterize their delay distribution and performance variability.
Table 10: Latency Breakdown of Individual Modules in the CRAMF Framework.
Module
Mcan(ms)
Std(ms)
Min(ms)
Max(ms)
Concept Extraction & Parsing
2261.63
181.26
2002.48
2903.49
Symbol-Level Keyword Matching
124.18
35,46
103.20
191.17
Semantic Similarity Retrieval
363.16
20.14
326.89
407.95
Rerank
14,40
47.43
7.69
485.81
Generation-Herald-7 Herald-7B
1752.11
295.40
1070.58
2220.34
Coneration-GPT-...
9621.92
1080.51
8414.50
11440.51
Generation-Kiming
7633.74
5234.67
4118.43
19675.50
Generation -ectrioon--eSSee-k---- V3
6903.24
444.06
6443.82
7998.04
Table 11: End-to-End Latency of CRAMF Integrated with Different Generation Models.
Model
End-to-End Latency (ms)
Hcrald-7B
4515.48
GPT-4o
12385.29 29
Kimina-7B
10397.11
DeepSeek-V3
9666.61
E.2 CONTEXT BUDGET ANALYSIS
We further count the contextual token usage of each model on different datasets before and after using CRAMF enhancement, shown in Table 12] The results show that although CRAMF does increase the context length, the maximum token usage is within 4.3 k, which is completely within the context window bearing range of the current LLMs.
Table 12: Token usage for each model and dataset before and after using CRAMF enhancement.
Dataset
Condition
Min Tokens
Max Tokens
Base
140
386
AdvancedMath
+CRAMF
253
4,256
Base
136
299
MiniF2F
+CRAMF
222
1,310
Base
131
281
Proo|Net
+CRAMP
4,085
24

---

Published as a conference paper at ICLR 2026
Through reasonable modular design, CRAMF achieves significant improvement in formal accu- racy and achieves a good balance of efficiency and effectiveness under the premise of introducing limited time delay and controllable context overhead.
25


Reviews:
[{"review_id": "MGtzcVKKP4", "reviewer": "Reviewer_bRZa", "summary": "This paper proposes CRAMF, a retrieval-augmented framework that enhances LLM based automated formalization in theorem provers such as Lean 4. \nThe method builds a structured concept-definition knowledge base from Mathlib4 by aligning formal definitions with natural language expressions through reverse translation, concept extraction, and embedding via MathBERT. CRAMF retrieves relevant formal definitions for a given theorem through a dual pathway hybrid retrieval.", "questions": "1. could the authors report latency and context budget\n2. How sensitive are results to KB noise?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The motivation of model hallucination and conceptual polymorphism is sound, and the solution through the integration of retrieval and concept-level grounding is persuasive.\nThe ontology-based KB design is novel in the formal reasoning domain and technically sound\nExperiments are comprehensive, covering multiple datasets (miniF2F, ProofNet), models (GPT-4o, DeepSeek-V3, Herald-7B), and ablations, and the newly released AdvancedMath benchmark adds value to the community.\nThere are consistent gains across heterogeneous base models", "weaknesses": "1. The conceptual extraction and rewriting modules rely heavily on opaque LLM prompting, I'm curious about the reproducibility and generalization.\n2. comparison to premise/statement retrieval specialized for Lean is missing, which makes it hard to situate CRAMF against strongest formal-specific retrievers.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "XR63kK1JIs", "reviewer": "Reviewer_UEGf", "summary": "This paper presents CRAMF, a retrieval-augmented framework that enhances LLM-based automated formalization for theorem proving in Lean 4. CRAMF builds a structured concept-definition knowledge base from Mathlib4 (over 26,000 definitions and 1,000 core concepts) and retrieves relevant definitions to reduce hallucinations and semantic gaps during autoformalization. Experiments on miniF2F, ProofNet, and a new dataset show consistent improvements, with up to 62.1% accuracy gain.", "questions": "Please refer to the Weakness section.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "1. The paper precisely identifies two major obstacles in automated formalization—model hallucination and the semantic gap arising from ambiguous or incomplete natural language premises.\n2. This paper introduces a concept-level retrieval-augmented generation (RAG) mechanism and builds a concept–definition knowledge base from Mathlib4.\n3. This paper demonstrates through experiments on miniF2F, ProofNet, and the newly proposed AdvancedMath benchmark that CRAMF can be seamlessly integrated into LLM-based autoformalization pipelines, consistently enhancing translation accuracy", "weaknesses": "1. The paper is primarily system-oriented and lacks formal justification or complexity analysis of why the hybrid retrieval pipeline improves semantic grounding. For example, the mapping from informal expressions to formal concepts could benefit from a more rigorous evaluation of ontology precision and recall.\n2. The experimental comparison focuses mainly on RAG-style retrievers (e.g., BM25, HyDE), without including other autoformalization-specific retrieval systems\n3. While the retrieval strategy is well adapted to formal reasoning, its methodological foundation largely follows existing RAG frameworks. The paper’s novelty lies primarily in domain adaptation to mathematical formalization rather than introducing fundamentally new retrieval theory or mechanisms.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "aip7qZZBax", "reviewer": "Reviewer_bPuu", "summary": "This paper proposes CRAMF, a concept-driven retrieval-augmented framework for automated statement formalization in Lean 4. It builds a concept–definition knowledge base from Mathlib4 and uses hybrid retrieval with reranking to provide context for LLMs. Experiments on miniF2F, ProofNet, and a new AdvancedMath dataset show improved compilation and formalization accuracy across models.", "questions": "- Does “Formalization Accuracy Rate@10” in Table 2 refer to the probability that at least one of the ten outputs passes the semantic consistency check, or to the proportion of successful outputs among the ten? It would also be helpful to clarify whether the metric is calculated on all runs or only those that pass compilation.\n- The notion of “concept” is somewhat vague. What exactly is its relationship with Mathlib definitions, classes, or structures? Is it a one-to-one mapping, or a more abstract layer? How do “concepts” influence the retrieval process?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "- The paper applies RAG to statement formalization tasks, and the retrieved contextual information effectively improves model performance.\n- Code and benchmark data are provided in supplementary material, supporting reproducibility.", "weaknesses": "- Lack of novelty. It is already well established that RAG improves performance on knowledge-intensive tasks, and similar ideas have been explored in auto theorem proving and auto formalization in Lean, e.g., ReProver [1], LEGO Prover [2], and recently Hilbert [3]. It is unsurprising that RAG also works in statement formalization. Moreover, key components such as reverse translation of Mathlib4 entities, query enhancement, and dual-pathway hybrid retrieval have already been used in Mathlib retrieval systems like LeanSearch [4] and LeanExplorer [5].\n- The range of models evaluated is limited. More recent and stronger models such as Gemini-2.5-pro, GPT-5, Claude-4.1, and Goedel-Formalizer-V2 (8B/32B) should be included for comparison. Their inclusion would strengthen the experimental section. It should also be noted that Kimina-7B is trained on miniF2F and ProofNet, making comparisons on these benchmarks less fair.\n- Formalization accuracy is evaluated only through automated checks, without human expert verification, which weakens the reliability of the results.\n- More explanation is needed for the AdvancedMath dataset. Although it is included in the supplementary material, its motivation and basic characteristics should be summarized in the main text. It seems all problems come from a single source and focus on calculus, which should be clarified.\n\n[1] Yang, Kaiyu, et al. \"Leandojo: Theorem proving with retrieval-augmented language models.\" Advances in Neural Information Processing Systems 36 (2023): 21573-21612.\n\n[2] Wang, Haiming, et al. \"Lego-prover: Neural theorem proving with growing libraries.\" arXiv preprint arXiv:2310.00656 (2023).\n\n[3] Varambally, Sumanth, et al. \"Hilbert: Recursively Building Formal Proofs with Informal Reasoning.\" arXiv preprint arXiv:2509.22819 (2025).\n\n[4] Gao, Guoxiong, et al. \"A semantic search engine for Mathlib4.\" arXiv preprint arXiv:2403.13310 (2024).\n\n[5] Asher, Justin. \"LeanExplore: A search engine for Lean 4 declarations.\" arXiv preprint arXiv:2506.11085 (2025).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "gh94iSSoEf", "reviewer": "Reviewer_AM7R", "summary": "This paper focuses on the task of automatic formalization in theorem proving, which currently faces two major challenges: model hallucination and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, the authors propose a framework called CRAMF (Concept-driven Retrieval-Augmented Mathematical Formalization). The framework consists of three main components: (1) construction of a concept definition knowledge base, (2) mathematical concept extraction, and (3) definition retrieval. Experimental results demonstrate that CRAMF can effectively extract information useful for formalization, thereby improving overall accuracy.", "questions": "Please refer to the Weakness section.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper is very well-written, easy to follow and well-organized.\n\nThis paper introduces a framework for automatically constructing a concept-definition knowledge base based on Mathlib4, addressing the problem of a lack of structured knowledge bases in the automated formalization domain.\n\nThis paper introduces the CRAMF-Guided Autoformalization process, which first extracts math concepts from question and then retrieve definitions from pre-defined knowledges. Then, based on the informal statement and definition, realize autoformalization, thus improving the accuracy.\n\nExperiments on different datasets show the effectiveness of the CRAMF framework. Through the ablation study, it also shows the reasonability of each module in this framework.", "weaknesses": "Although the CRAMF method substantially improves both retrieval accuracy and auto-formalization performance, I still have some concerns. \n\nThe paper uses MathBERT for semantic encoding, but it is not clear whether the authors have compared it with other encoding models that might achieve better performance. \n\nIn addition, regarding the baselines, there already exist several retrieval approaches for Lean based on natural language, such as LeanSearch and LeanExplore. It would strengthen the paper if comparisons with these methods were included.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)