LoC-Decomp: LLM Autoformalization via Logical Concept Decomposition and Iterative Feedback Correction
Authors: Jiangze Shi
Zhiwei Zhang
Baoquan Ma
Shuai Zhao
Ye Yuan
Guoren Wang
Venue: ICLR 2026 Poster (2026)
Keywords: Autoformalization
Automated theorem proving
Large language model
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: Loc-Decomp is a novel framework that enhances LLM-based autoformalization by integrating semantic consistency checks and iterative refinement, achieving a 91.16% success rate on the miniF2F dataset.

Abstract: Autoformalization—the process of converting natural language mathematical statements into machine-verifiable formal code—plays a critical role in ensuring the reliability of mathematical reasoning generated by large language models (LLMs). Recent studies show that LLMs exhibit strong potential in automating this process, producing formal code for systems such as Lean 4, Coq, and Isabelle. Despite prominent advances, existing LLM-based autoformalization methods remain limited: they lack the ability to provide reliable semantic consistency checks to ensure that the formal code accurately preserves the meaning of the original statement. Furthermore, such methods are unable to support iterative improvement through corrective feedback. To address these limitations, we propose Loc-Decomp, a novel framework that integrates an automatic semantic consistency checker and the Lean 4 compiler to iteratively refine LLM-generated formalizations, ensuring both semantic consistency and syntactic correctness. Our approach introduces three key innovations: __(1)__ A structured and COT-like formalization template that decomposes complex formalization tasks into modular, foundational components, and systematically assembles them—like building blocks—into a complete formal expression. __(2)__ A semantic self-checking mechanism based on a divide-conquer-merge strategy to detect subtle inconsistencies between the formalization and the original statement. __(3)__ An iterative feedback-driven refinement loop that leverages both semantic and syntactic error signals to guide the LLM in progressively improving the formal output. By integrating these innovations, Loc-Decomp significantly enhances the accuracy of LLM-driven formalization, reduces reliance on human intervention, and moves closer to truly reliable automated reasoning. Extensive experiments on high-school-level and undergraduate-level datasets demonstrate that our approach achieves a significantly higher formalization success rate compared to baseline methods and state-of-the-art (SOTA) models. On the PutnamBench dataset, for instance, our method attains a success rate of 93.09\%, representing an improvement of 18 percentage points over the previous SOTA SFT-based model.

Published as a conference paper at ICLR 2026
LOC-DECOMP: LLM AUTOFORMALIZATION VIA LO- GICAL CONCEPT DECOMPOSITION AND ITERATIVE FEEDBACK CORRECTION
Jiangze Shi', Zhiwei Zhang*; Baoquan Ma², Shuai Zhao', Yuan', Guoren Wang! 1 School of Computer Science, Beijing Institute of Technology Lab of UAVs, National Computer System Enginering Research Institute of China {jzshi, zwzhang, shua zhao, yuan-ye edu en; baoquan ma ma@buaa. cn; wanggrbit@126.. com;
ABSTRACT
Autoformalization process of converting natural language mathematical state- ments into machine-verifiable formal rode-plays critical role in ensuring the reliability mathematical reasoning generated by large language models (LLMs). Recent studies show that LLMs exhibit strong potential in automating this process, producing formal code for systems such as Lean 4, Coq, and Isabelle. Despite prominent advances, existing LLM-based autoformalization methods remain lim- ited: they lack the ability to provide reliable semantic consistency checks to ensure that the formal code accurately preserves the meaning of the original statement. Furthermore, such methods are unable to support iterative improvement through corrective feedback. To address these limitations, we propose Loc-Decomp, a novel framework that integrates an automatic semantic consistency checker and the Lean 4 compiler to iteratively refine LLn--genrated formalizations, ensuring both semantic consistency and syntactic correctness. Our approach introduces three key innovations: (1) A structured and COT-like formalization template that decomposes complex formalization tasks into modular, foundational components, and systemat- ically assembles them-like like building blocks-ing into a complete formal expression. (2) A semantic self-checking mechanism based on seriide-oonuer-nnne to detect subtle inconsistencies between the formalization and the original state- ment. (3) An iterative deedback-driver refinement loop that leverages both semantic and syntactic еrror signals to guide the LLM in progressively improving the formal output. By integrating these innovations, Loc-Decomp significantly enhances the accuracy of LLM-driven formalization, reduces reliance on human intervention, and moves closer to truly reliable automated reasoning. Extensive experiments on high-schin nigh-school-leve and undergraduate-leww datasets demonstrate that our approach achieves a significantly higher formalization success rate compared to baseline methods and tiite-of-theaate (SOTA) models. On the PutnamBench dataset, for instance, our method attains a success rate of 93.09%, representing an improvement of 18 percentage points over the previous SOTA SFT-based model.
strategy
INTRODUCTION
Statement formalization (Wenz et al.) 2025 Gonthier 2007 Szegedy| 2020) denotes the process of converting mathematical statement into formal language such Lean 4, Coq, or Isabelle (de Moura et al. 2015) Bertot & Castéran 2004 Paulson 1994) which constitutes necessary step the verification of mathematical reasoning in theorem provers(Zhou al. (024)). A successful formalization must not only satisfy syntactic correctness, as verified by compiler checks, but also ensure semantic consistency by faithfully preserving the meaning the original statement. However, this task is widely recognized as highly labor-intensive, owing to the inherent flexibility and ambiguity of natural language, which pose significant challenges to automation (Yang et al. 2024).
"Corresponding Author

---

Published as a conference paper at ICLR 2026
Recent studies leveraging large language models (LLMs) (Achiam et al. 2023 Team et al. 2023
Liu et al. 2024| Azerbayev et al. 2023b) for autoformalization have shown promising progress and achieved notable results on relatively simple statements. These approaches include both prompt engineering with candidate scoring using general-purpost L.MS and methods based on supervised fine-tuning domain-specific datasets (Li et al. 2024a] Ying al., (024). However, when deal- ing with more complex mathematical statements such as those in probability, combinatorics, or geometry (Trinh et al. 2024) there is still considerable room for improvement. Key challenges include accurately detecting subtle semantic inconsistencies and effectively leveraging these detected inconsistencies to refine the formalization.
To address these two challenges, we proposed an automated LLM-based formalization framework built upon Logical Concept Decomposition (LoC-Decomp), which integrates a modular formalization template, an automatic semantic consistency check (ASCC) method, and an iterative refinment method within Lean 4. Specifically, we instruct the L.LM to generate Lean 4 code conforming to a predefined template that decomposes the formal statement into multiple declaration segments,therebe enabling a semantically complete breakdown. A divide-conquer-mergg based back-translation process is then applied to more accurately capture subtle semantics in Lean 4. Subsequently, segmented and holistic discrepancy detection by prompting the LLM to identify potential semantic inconsistencies within individual segments and the entire statement. The detected discrepancies then evaluated against predefined criteria by L.I,, and rectification suggestions are also provided along with the evaluation procedure. Utilizing these discrepancy descriptions and recommendations as well as compiler еπrоr messages, an iterative refinement strategy is implemented to achieve both semantic consistency and syntactic correctness.
perform both
As in previous works, we conducted extensive experiments on widely used mathematical datasets, AATT-5000Cighhmaan et al., 2024) and miniF2F(Zheng et al., 2022) for example, to evaluate the effectiveness of our proposed approach. The results indicate that after incorporating the Loe-Decomp Lean template and few-shot examples, the single-round (pass@) I) formalization success rate on the miniF2F dataset reached 77.25%. With the further integration of seman- tic consistency checks, compiler verification, and iterative feedback refinement, the pass rate on miniF2F increased to 90. Experimental results and code are available at https: liaation.
In summary, the main contributions of this paper are as follows:
We introduced LoC-Decomp. a COT-like Lean 4 template that breaks down the formalization process into multiple steps, with theoretical guarantee of expressiveness.
2. We introduced a novel semantic consistency checking method by decomposing the formalization code. This approach enables LLMs to accurately detect semantic inconsistencies between the formalized code and the original problem in complex scenarios.
3. We presented iterative feedback- based method for semantic and syntactic correction, allowing the L.M to leverage identified semantic inconsistencies from the previous step or compiler-generated syntax errors to iteratively refine the Lean 4 code.
4. We conducted extensive experiments on two widely adopted datasets and evaluated the results using automatic evaluation metric supplemented by human assessment, which collectively demonstrate the effectiveness of the proposed approach.
2 BACKGROUND AND RELATED WORK
Formal Reasoning: Recently, a number of studies have emerged that employ formal provers such Lean 4, Coq, and Isabelle validate the reasoning processes of LLMs (Yang al. 2023)
(Wang et al. 2024: Li et al.) 2024b. Lin et al.) 2025a Alfarano et al., 2024 Huang et al. 2024). As pointed out in (Yang et al.) 2024). leveraging rigorous formal provers to provide feedback can
effectively mitigate data scarcity and counteract hallucinations. Automated theorem provers represent one of the building blocks of this approach: given formal proposition, they require the LLM to output proof process, which is then verified using formal proof system. BFS- (Xin et al.
All these results are under the ASCC-3-MV metric with DeepSeck-Ve V3 as base model, see section 4 for more information.
2

---

Published as a conference paper at ICLR 2026
2025) through optimized Best-First Search framework enhanced by expert iteration and policy refinement. Deeppeekk-rovert (Ren et al., 2025) introduces a cold-start reinforcement learning procedure that integrates informal mathematical reasoning with formal proof steps through recursive theorem-proving pipeline.
Autoformalization: Unlike theorem proving, autoformalization does not generate proofs for theo- rems; rather, it converts natural language statements into formal specifications (Weng et al. (025). Autoformalization thus acts bridge between informal and formal mathematics.Trade based autoformalization methods (Pathak, 2024) are limited by their manual design, fragility to unseen constructs, and poor semantic disambiguation. In contrast, methods based on Large Language Models (LLMs) offer greater flexibility and are capable of capturing subtle or rare linguistic pat- terns that might be overlooked by human experts during rule design. I.L.-based autoformalization primarily follows two research directions: fine-tuning on synthetically generated data (Tiang et al. 2025 2023b Azerbayev al. 2023a) and prompt-based (in- (in-context learning) approaches. Some reserchers observed that auttoiinformalization is easier than autoformalization (Wu et al. 2022). This observation has motivated subsequent work that employs LLM-based back-translation to verify the correctness of formalized outputs (Li et al. 2024a). Another line of research, parallel to work, explores the use of Retrieval- Aatiaal-Augmeeee Generation to improve the formalization abilities of large language models (Liu al., 2025a). A training based evaluation method is proposed by Lu al. (2024a) to detect misalignment in formalization, but this method can only provide a numerical score without targeted revision suggestions. For feedback refinement, several studies have utilized compiler сπгог messages to improve the formalization results generated by LLMs et al. 2025b; Lu et al. 2024b Zhang et al. 2024). The work of KELPS (Zhang et al. 2025) introduced an intermediate lan- guage to facilitate concept decomposition; however, it did not integrate this decomposition idea into semantic consistency checking. And FIMO(Liu et al.) 2023) was the first introduce a mechanism that integrates semantic feedback with syntactic error correction. However, significant limitation is that their semantic feedback mechanism required manual vemenvement, In summary, an automated approach that integrates semantic inconsistency feedback with compiler errors to simultancously achieve semantic consistency and syntactic correctness remains unexplored.
rule-
3 LOC-DECOMP BASED ITERATIVELY REFINEMENT FRAMEWORK
As shown in Figure 1 our proposed autoformalization framework consists of three modules: (1) template-based formal translation (FormalTrans) (2) automatic semantic consistency check and iterative rectification (ASCC-R), and (3) compiler check and iterative rectification (CpC-R).
The core idea of our approach is as follows:
1. Construct a Lean 4 template that guides the LLM to generate formalization code in Shain-of-Thoughh-nnssppp
stepwise manner (corresponding to the FormalTrans module).
2. Perform fine-grained semantic consistency checking through a divide-and-congue strategy to detect nuanced semantic inconsistencies (corresponding to the ASCC-R module).
3. Employ an iterative rectification method that jointly addresses semantic inconsistencies and compilation errors (corresponding to the joint iteration of the ASCC-R and CpC-R modules).
At the core of our approach lies divide-conquer-mergg strategy for semantic consistency checking. By decomposing the formalized code into logical components through our LoC-Decomp template, we enable ane-grained tack-translttion and verification of each semantic unit against the original problem statement. This component-level decomposition allows for precise identification and localization of semantic inconsistencies, which then serve as targeted feedback for iterative correction. Coupled with compiler error checking, this creates closed loop where semantic and syntactic issues alternately detected and rectified through iterative refinement.
Processing a formalization task follows an iterative workflow across three interconnected modules. First, the FormalTrans module synthesizes a prompt from the problem statement, task requirements, few-shot examples, and the LoC-Decomp template, then invokes the LLM to generate initial Lean code which adheres to the template. Second and third, the ASCC-R and CpC-R modules jointly execute alternating semantic and syntactic refinement: ASCC-R detects inconsistencies through back-
3

---

Published as a conference paper at ICLR 2026
Translate NI.
Previous Original Problem
To General Purpose LLM Or Fine-tuned LM
Without further
Method
In Natural Language
Deterted ASCA and rectity nest raund Rectiiial
Our Method
Original Problem
Template-Rased FormulTruns Module
ASCC-R Module(2
CpC-R Module
In Natural
Language
Rectified
Template Besed
Iieratice Check And Reciifiatien
Formal Transtation
Figure I: Overview of our Loc-Decomp based iteratively refinement framework (bottom) and an overview of previous moth) In comparison with previous methods that select one from multiple generated candidates, our approach introduces iterative feedback and refinement, eliminating the need to generate multiple candidates and gains cumulative knowledge from each iteration.
translation and proposes targeted modifications, while CpC-R identifies and resolves compilation errors. Each module operates iteratively within its domain-ASce until semantic consistency is achieved (or the semantic iteration limit K-sem is reached), while CpC-R runs an inner syntax loop until compilation succeeds (or the syntactic iteration limit K K-syn is reached). These inner loops form Sem-Syn iteration unit; multiple such units constitute outer loop that continues until the code passes both checks consecutively or the maximum iteration limit is reached.
runs an inner semantic loop
3.1 FORMAL TRANSLATION MODULE
Import Nathith..
Ieport Mathi
Inductive was Indureive type where cnun_1 enue
audllary
Anciliary Types Auxiliary
structure PySyaten Whire
(
Formalize the following problem into lean4 adhereing the template provided.
User Prompt:
Muthmoricsl system
F:
sol_sum.o.
sun_pnnddy:sooeeeppo boeys
contimuuu (KGRB((F:BHR)
la Ix- c A If
def constratee(e:Sppree)) <our_bory
5.f-Xxx
function constraint [stSyatinn Prop
[(a)
x
b.
It
Constraints
oise
def htt.:uusucccssatttteteeo
hrop
continnous.
def sol, (onstrsint (s: Propoe
<exor. <sxor_bocy> bocys
def solution constroint (s15yston) Prop
s.5ol_
continumux
proolon (sol: semetye))))) trep.
problzs (sol Trop
System,
5 Systom,
Problem Statement
_oc_constesint
conti nontinuous_comm
solution constraint
solution. construint sotution 5-507 s.5o1_su9_._
solutton 5.501,
Lagiecal-Decomppsitionn--a Template
Output Formalization
Figure 2: Formalization template and a concrete example. The left is our proposed Template with place holders, and the right is an example for formalizing a problem about the property a continuous piecewise function. Please note that the example shown in this figure was manually designed to demonstrate the template structure. For examples generated by large language models (LLMs), we refer readers to Appendix F
The FormalTrans module serves the entry point of our framework, responsible for transforming mathematical problems in natural language into structured Lean 4 code. Unlike prior approaches that directly formalize problems as Lean 4 theorems, we introduce novel template-based approach that de-
4

---

Published as a conference paper at ICLR 2026
composes the formalization task into sequence of semantically meaningful components including mathematical objects, constraints, and the problem statement) as shown in Figure 2 This de- composition mimics Chain-of- Thouuhh (CoT) reasoning process, guiding the LLM to construct formalizations step-by-step rather than attempting to generate the complete code in a single pass. By breaking down the complex formalization task into manageable subtasks, our template enables LLMs to organize the Lean 4 content in more structured manner, thereby enhancing performance as demonstrated in our experiments. The formulation of the template is kind of based on Discourse Representation Theory, which is introduced to mathematical formalization by (Ganesalingam 2013).
detailed explanation for this template is available in A.I
To make sure the template is fully complied with, a verification method is required. Since this template framework imposes requirements heyond the syntax rules of the Lean compiler, a lightweight parser is implemented to serve as template verifier. If the requirements are not met, it returns corresponding feedback to prompt the L.LM to regenerate the code. This process iterates until all conditions are satisfied or the maximum iteration limit is reached. We emphasis that although this template is demonstrated using Lean 4, it can be easily adapted to other theorem provers like Coq or Isabella, detailed discussion is provided in A.7 and details about the parser and the feedback strategy available in A.2
Since such template imposes additional requirements top of Lean syntax, the set of all Lean 4 code that satisfies the template forms a proper subset of all Lean 4 code that meets the syntactic requirements. This implies that Lean 4's expressive power may be constrained under this template, as certain formal declarations might not be convertible into the template's structure. To provide theoretical guarantee for the expressiveness of the template, we propose the following theorem and provide its proof in the A.4
Definition 3.1. LoC-Decomp counterpart: For a complete Lean 4 proposition string(by complete we mean that this string contains proposition defined by theorem or lemma and all it's dependencies), we define its LoC-Decomp counterpart as string that is semantically equivalent to the Lean 4 proposition and satisfies the LoC-Decomp template requirements. Here, satisfying the LoC-Decomp template requirements means that the string can be accepted by our parser that encodes the syntactic rules of the template.
Theorem 3.1. For any complete Lean proposition string, there exists at least one LoC-Decomp counterpart.
3.2 AUTOMATIC SEMANTIC CONSISTENCY CHECK MODULE
To verify semantic consistency between the formalization and the original statement, our ASCC module employs a mack-translation component that converts Lean 4 code into natural language while preserving semantic nuances. This back-translated description, presented alongside the formal code, enables the LLM to assess semantic alignment between the natural language problem and its Lean representation, as illustrated in the top half of Figure 3
Direct translation of complete Lean 4 code into natural language is unreliable for complex mathemat- ical statements, as LLMs struggle to detect subtle semantic logic in a single pass. To address this limitation, employ a divide--onnqer-merge strategy: (1) divide the Lean 4 code into semantically self-contained segments where each encapsulates complete, independent units of meaning [ (2) conquer by translating each segment independently via the LLM; and (3) merge by integrating the translated segments into a cohesive natural language description based on their logical relationships. Detailed discussions of the divide and merge mechanisms are provided in Appendix
As shown in the bottom half of Figure 3 we leverage the back-translated natural language description to verify semantic consistency between the formalization and the original problem. This comparison allows us to detect discrepancies that may indicate formalization errors. We employ four-stage strategy: identifying all potential discrepancies, evaluating the significance of each discrepancy,
"This template applies to both solving and proof-oriented problems. The main text focuses solving-type problems, but the framework can be adapted to proof-type problems with minor adjustments (see A.5). 'The term "semantically self contacont refers to segments in which all necessary semantic compo- nuchs-such& as definitions premises-art are explicitly contained within the segment itself (i.e., the segment can pass the compiler check).
5

---

Published as a conference paper at ICLR 2026
Back Translation
NL decippton for probiem dalomant
Jtretture Pylystee
NL d..dornitionn for fanction conmmnt This oonaranee defizce plowwise function...
Syste descrptunt
<NL docription the conjunction conemrra
lngical
problin
Original Cade
Divide by parer ())
Conquer (2)
Marge
Identify critical discrepancies
dismpuancion omggial priblam
Use deteriiee Eiseepancy
oniical.
place matheratiial problen.
or dicorppnncis
Disergancy ofitaa
Probien: <SL lazd--
discrepencies
Discrquacy
LIM discepancios
Per Constraint
User Deterins wetsrr tha dicrepancy do csid und proside some nommmeediiion rectidy the lcac4 codk.
discrepancy
Diserepancy Find Out (4)
find out (5)
('Mnerrgarry, joint or "ot"""""" commmmmndooon....... ")
Automatic Semantic Consistency Check
Disereganey determination
(ASCC)
provide recommcndation
Figure 3: Back translation by divide-conquer merge strategy and the automatic semantic consistency check.
synthesizing critical discrepancies to determine an overall consistency level, and re-examining each discrepancy in cases not fully consistent if any discrepancy is confirmed, the output is deemed semantically inconsistent. Specifically, (4) segmented and holistic discrepancy detection are employed to identify differences between the formalization and the problem description. The former targets subtle, localized inconsistencies, whereas the latter focuses on overall, structural issues; (5) Collective evaluation of identified discrepancies to classify them critical or acceptable based on predefined criteria, followed by determining an overall consistency level according to all critical discrepancies, the consistency level include: Fully consistent, Consistent without loss of generality. Inconsistent; (6) Individual re-evaluation of each discrepancy if the code is not fully consistent; and (7) For each confirmed discrepancy, the LLM must provide correction suggestions, and the formalization judged not fully consistent. If any of discrepancy exist, the formalization is inconsistent. Detailed explanations of each step and judge criteria as well as consistency level definitions are available in Appendix B and prompt used are provided in Apppendix This consistency-checking mechanism enables us to provide targeted discrepancy information and recommendations, allowing the LLM to rectify the Lean 4 code (as described in following section).
3.3 JOINT SYN-SEM ITERATIVE RECTIFICATION
As shown in Figure The iterative rectification procedure is an alternating process of the semantic inconsistency correction and compilation error (i.e., syntax error) correction. Each approach utilizes error feedback to prompt the LLM to reassess its prior output and produce a revised solution. The primary distinction lies in the source of the feedback: semantic error information derived from semantic consistency checks, while compilation error information is provided by the compiler.In both cases, once error information is obtained, is appended the context supplied the LLM for revision. The updated output then undergoes another round of semantic consistency verification or compilation checking. This iterative cycle continues until the code passes both checks consecutively or the maximum iteration count is reached.
More specifically, our approach involves an iterative process that alternates between semantic and syntactic correction, with the objective of steering the formalization toward semantic con- sistency and syntactic correctness. For a semantically inconsistent formalization, we first run an inner semantic loop, where semantic corrections are made and re-validated iteratively until success or until reaching the maximum semantic iterations (K (K)sem). After passing semantic validation, it enters the inner syntactic loop, undergoing compilation checks and syntactic fixes until it com- piles successfully or exceeds the allowed syntactic iterations (K- (K-syn). One inner semantic loop followed by inner syntactic loop forms Sem-Syn Iter Unit. If the formalization fails pass

---

Published as a conference paper at ICLR 2026
Another round
Semantic errer rectilied
PASS
somantic loop
Inconsistent
Sem-Syn Iter Unit
ASCC-1
PASS
Consisteat Formalization
Formalization
ASCC-I Module
CpC-R Module
Consistency Check
Syntactic crrur rectifled
OUTER LOOP
ONE ROUND
Figure 4: Joint Syn-Sem iterative rectification
both checks consecutively within one unit, it triggers another Sem Sem-Syn Iter Unit: this multi-unit process the OUTER LOOP, which can run up to N times. After the OUTER LOOP, a final validation for both semantic and syntactic errors is performed-this entire sequence, including most outer loops plus the final check, constitutes one ROUND. Failed cases proceed to the next ROUND, with the entire process repeating for up M rounds. A detailed description of this process is provided in Algorithm [ In this algorithm, the function ASCC(-) returns the result of the ASCC check, denoted as ASCCLevel, which can take one of three values: Fully Consistent, Consistent Without Loss of Generality, or Inconsistent, Here, ASCC-R(-) refers to the ASCC check with rectification, and CpC-R(-) denotes the compiler check with rectification.
Algorithm 1 Iterative check and rectification
Input:
problem, Lean4; Output: pectifiedLeany ASCC:
ASCCLevel t ASCC(Lean4), m O:
compiler check not pass) and < M do 2: while (ASCCLevel = Inconsistent
3: while (ASCC = null or Inconsistent) and iteration limit not reached do
4: while ASCCLevel * F Fullycon.sistent and iteration limit not reached do
5: Lean4T + Informalization Lean4);
6: LeanA, ASCCLevel <- ASCC-R(LeanddTNNN) LeanA, problem):
7:
end while
8: if ASCCL + Inconsistent and compiler check not pass then
9: while compiler check not pass and iteration limit not reached do Lean4 Cpe-R(Leand);
11: end while
ASCCLevel null;
13: end if
end while
15: recti fiedLeee Leand, m +- m + 1;
16: end while
17: return rectifiedLeand,
EVALUATION
4.1 EXPERIMENTAL SETUP
Datesets: To evaluate our methods, we employed two widely used public Matasets-MAAT. Lightmnn et al. 2024) and 2ini et al. 2022) as well as two custom datasets: MATH- ASCC-Eval-Is 150 and MATH-Level5-500 The MATH-500 dataset comprises 500 problems sampled et al. 2021) dataset, covering a variety problem types and diffi-
from the MATH- SANTH-12500 (500((endryyeee culty levels. The miniF2F dataset contains 488 problems sourced from AIME, AMC, and IMO petitions, which is specifically designed for autoformalization by converting solve-type problems into proof-type problems. To evaluate the performance of our method more complex mathematical prob-

---

Published as a conference paper at ICLR 2026
lems, we also adopted DutnamBench(TToukkee et al. 2024 and ProofNet(Azerbayey et al. 2023a as test datasets for further evaluation. PutnamBench and ProofNet contain 522 and 371 undergraduate- level mathematical problems respectively, presenting additional challenges for the autoformalization by L.Mss.
The MATH-ASCC-EvaaL
dataset comprises 150 problems sampled from MATH-500 across difficulty levels, each accompanied by Lean 4 formalizations and human annotations (91 positive, 59 negative). The negative cases predominantly contain subtle errors, making this dataset suitable for evaluating automated consistency-checking methods (see Appendix Appendix E for details). In contrast, the MATH-Leve15-50 subset consists of 50 randomly selected level-5 problems from MATH-500, designed to assess the formalization capability on challenging problems.
Models: Experiments were conducted using three open source LLMs LLMs-including DeepSeek-V3. V3, KIMI-K2 and Qwen3-235B( (Liu et al.) 2024, Yang et al. 2025 Kimi Team et al. 2025 to validate the effectiveness of the proposed method across different LLMs.
Baseline: For fair comparison with our method, we implemented several baseline methods for three tasks. For the semantic consistency checking task, we introduced two baselines: (1) SC-Baseline, where the LLM is provided with both the original problem and its corresponding Lean 4 code then prompted to assess semantic consistency; and (2) Cee-Baeliie-BaaTTTee supplies back translation of the Lean 4 code. For the pass @ I formalization task, developed (3) Baseline, which employs basic few-shot prompt to guide the LLM in formalizing the given problem. For the iterative formalization task, we designed (4) Baseline-iter, which implements method identical to ours but employs a basic semantic checker like the SC- IC-Baseline. To compare our method with the Supervised Fine-Tuning based models, we designed SFT-Baseline by selecting Ren DeepSeek-Provee V2verr-V((5) Ren et al. (025)) as the base model, and other configurations are exactly the same with the are provided in the Appendix
which additionally
iterative
The prompts and detailed configurations for these baseline methods
Metrics: For the semantic consistency evaluation, we assessed the ASCC method on the MATH- ASCC-Eval-150 dataset as well as the
dataset using recall, precision, and F1- Fcoor. For the back translationi task, we assess the metric of translation success rate by human evaluation. For the iterative rectification task, the primary evaluation metric was the ASCC-3-MV pass rate determined through majority voting over three rounds of ASCC- suppleeupleeentee by human- evaluated pass rates. In addition to ASCC-3-MV, we also report the ASCC-3-SV pass rate- aase- on single veto over three rounds of ASCC as a reference metric, due to its high precision but low recall.
Implementation: multi-round iterative testing, we set the maximum iteration numbers as K-sem = 2, K-syn = 3, N 5, .M 3. Across all evaluations, the temperature parameter was set to 0.7 for ASCC and 0.3 for all other requests, consistently applied to all LLMs. And all the baseline methods conducted with ReepSeek-V3.
4.2 EXPERIMENTAL RESULTS
ASCC-3 Evaluation. We first evaluate the alignment between the ASCC and human judgment criteria for assessing formalization semantic consistency, As shown in Figure 5 on the MATH-ASCC-Eval 150 dataset, the ASCC-3-MV metric achieves precision of 0.90, a recall of 0.82, and a Fl-score of 0.86. Compared to the baseline, precision shows significant improvement the method's capability to accurately identify errors. Although precision slightly decreases relative to ASCC-3-SV, recall remains at reasonably high level. We therefore conclude that ASCC-3-MV aligns most closely with human evaluation criteria. Owing to its strong performance in detecting negative instances, we propose ASCC-3-MV as standard for evaluating the performance of our methods, while still providing ASCC-3-SV as a more stringent reference.
key focus, as it reflects
@ 1 with the template and few-shot examples. As ablation study, we evaluate our approach without the iterative rectification process to assess the contribution LoC-Decomp template to the overall pass rate. The results in Table I iidicaae that even without iterative rectification, our method still achieves a relatively high pass rate. We attribute this performance to the ofaun-of-thoughhe template and the use of few-shot examples based on classification. This comparison confirms that
8

---

Published as a conference paper at ICLR 2026
ASCC-3-MV
ASCC-3-SV
SC-Baseline
SC-Baseline-Baad Baakiinns
Human Labul
Pos
Pos
Pos
Pos
2
Neg
Neg
3
50
Neg
45
Neg
41
12
Neg Predicted Label
Pos
Pos
Neg
Neg Predicted Label
Pos
Pos
Neg
Predicted Label
Predicted Label
P: 0.90 R: 0.82 F1: 0.86
P: 0.95
R: 0.56 F1: 0.70
P: 0.68
0.99 F1:
0.70
F1:
Figure 5: Confusion matrix of the ASCC-3-MV, ASCC-3-SV, SC-Baseline and SC-Baseline- BackTrans (basline with back translation) evaluation result.
our iterative rectification strategy results in clear performance improvement, with increases in all evaluated items.
Table 1: Results without iterative rectification
DeepSeck-V3
KIMI-K2
Qwen3-235B
Items
MV
SV
MV
SV
MV
SV
MATH-500
63.20
44.80
60.20
43.40
65.40
45.60
miniF2F
77.25
54.30
78.57
60.29
76.90
60.29
Joint Syn-Sem iterative rectification evaluation. The results of the iterative rectification method are summarized in Table 2 where MV denotes the ASCC-3-MV pass rate, and SV denotes the ASCC- 3-SV pass rate. The best pest-performing method is underlined. After three iterations, our approach achieved a ASCC-3-MV pass rate of 84.00% on MATH-500 and 90.16% on miniF2F when combined with DeepSeek- V3,, representing the highest performance among all three models evaluated. The result with iterative correction demonstrates a significant improvement over pass@ 1, which confirms the effectiveness of our proposed method
Table 2: Iterative rectification round-3 results
DeepSeek-V. V3
KIMI-K2
Qwen3-235B
Items
MV
SV
MV
SV
MV
SV
MATH-500
84.00
61.60
77.80
55.60
75.60
57.80
miniF2F
90.16
57.00
91.60
72.90
80.25
61.07
Human evaluation. As a supplement to the ASCC-3-MV and ASCC-3-SV metrics, we performed human evaluation the MATH--Level5-50 dataset. For comparison, three baseline methods as outlined in Section 4.1 were implemented. The results indicate that, using only template guidance and few-shot examples, our approach achieves formalization pass rate that exceeds the baseline by 18% under human evaluation. After three rounds of iterative refinement, the pass rate further increased 84%, surpassing the baseline by 30%. Even when compared models fine-tuned with expert iteration, our method achieves higher pass rate. The results are summarized in Table 3 where "Ours-no-iter" refers to our LoC-Decomp method without iterative rectification, and "Ours-iter" denotes the version with iterative rectification. A case study illustrating the rectification process is provided in Appendix
were
Evaluation undergraduate-leve problems. For undergraduate- mathematical problems, our experimental results indicate that under the ASCC-3-MV evaluation standard, our method still demonstrates notably high accuracy rate, further evidencing the universality and generalizability of our approach. See Table and Table for the results.
Addittiona experimental results about the iterative process available in Appendix G

---

Published as a conference paper at ICLR 2026
Table 3: Human evaluation MATH--Leve1-550
Items
Ours-no-iter
Ours-iter
Baseline
Baseline-iter
SFT-Baseline
pass rate
70.00
84.00
52.00
54.00
66.00
Table Results without iterative rectification on PutnamBench and ProofNet
DeepSeek-Ve V3
KIMI-K2
Items
MV
SV
MV
SV
PutnamBench
48.37
31.71
53.66
35.16
ProofNet
38.42
27.79
43.05
29.16
Table 5: Iterative rectification round-3 results on PutnamBench and ProofNet
DeepSeek-V V3
KIMI-K2
Items
MV
SV
MV
SV
PutnamBench
81,50
58.33
72.36
48.78
ProofNet 67.03
48.50
70.57
52.59
Comparative Analysis. To compare our method with existing approaches, we selected DeepSeek- Prover-V2-671B, IB, Fordde-Formalizor- Formaliiooo----32BB.Li evaluation. To ensure a fair comparison, we adopted the conventional LLL evaluation framework. The results are summarized in the Table 6
al. (2025)). and Kimina-Autoformaliiee--7 for
Table 6: Performance comparison of different theorem provers
Items
Ours
DeepSeek-Pree Prover
Kimina- Kimina-Auto AutoFormalizor
MATH-500
96.60
84.60
90.20
63.40
mini-F2F
97.54
87.18
93.28
87.23
PutnamBench
93.09
75.41
78.66
61.99
ProofNet 73.57
83.10
71.39
61.31
notable observation is that our method's performance on the ProofNet dataset is significantly lower than that of DeepSeek-Provent method on ProofNet only 74%, considerably lower than the over 95% pass rate achieved on other benchmark datasets. Manual inspection indicates that most compilation failures type class instances (e.g., "failed to synthesize" errors). We hypothesize that this issue is related to ProofNet's heavy reliance advanced Mathlib usage patterns. Since the current method does not incorporate retrieval-aure -auieeee---uummetedddde generation (RAG) mechanism, the large language model struggles accurately retrieve and incorporate relevant Mathlib definitions, thereby compromising compilation success. It should be noted that this limitation is not an inherent flaw of the method itself, but rather an orthogonal challenge that can be effectively addressed by integrating RAG-based extensions.
Analysis reveals that the compilation check pass rate of our
due unresolved
LIMITATION
Human evaluation in this study was conducted on a dataset of limited scale, constraint commonly encountered in this field due to the labor-intensive nature of such evaluations. While this is consistent with the practices of related works that face similar scalability challenges, expanding the size of the dataset in future research could further strengthen the reliability and generalizability of our proposed approach.
10

---

Published as a conference paper at ICLR 2026
THE USE OF LARGE LANGUAGE MODELS
This study utilized Large Language Models (LLMs) two distinct roles:
assistive tool enhance the language quality and clarity of the manuscript. The initial draft was entirely authored by the researcher, after which the LLM provided suggestions improve sentence fluency, grammar, and academic tone. All conceptual contributions, arguments, and factual assertions originated from the author. The final manuscript was thoroughly reviewed and approved by the author, who takes full responsibility for its content.
1. Language Polishing and Editing: LLMs employed
LLM Research Subject: key aspect of this research involves the evaluation of LLM capabilities. The outputs generated by the model were systematically analyzed as primary focus of the study. The corresponding methodology elaborated in the main text.
REPRODUCIBILITY STATEMENT
To ensure the reproducibility our work, have made our complete codebase, along with the raw experimental results and detailed instructions for setting up the environment, publicly available. All materials have been submitted to an anonymous repository for blind peer review and will be retained upon publication.
ACKNOWLEDGMENTS
This research was funded by the National Key Research and Development Program of China (Grant No. 2024YFE020900)), the NSFC(Grant No. U23B2019, Grant No. U2441237).

---

Published as a conference paper at ICLR 2026
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, 1lge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et Gpt-4 technical report. arXiv preprint arXiv:2303.08877, 2023.
Alberto Alfarano, François Charton, and Amaury Hayat. Global дуарuпоv functions: long standignn open problem in mathematics, with symbolic transformers. Advances in Neural Information Processing Systems, 37:93643-99361 2024.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-lovel mathematics. CoRR, abs/2302.12433, 2023a. doi: 10.8550/ARXIV.3300.2433. URL https:///oii.ogg 10. 4.558850//aa /0tp5///axiivvm
Zhangir Azerbayev, Hailey Schoelkopf. Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023b.
Yves Bertot and Piere Castéran. Interactive Theorem Proving and Program Development Coq 'Att: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS doi: 000007997883-662-7776666 URL
Series. Springer, 2004. ISBN 978-3-642-05880-6
attps://dolt org/ 10. 1007 / 662---6622222 07964-5
Leonardo Mendonça de Moura, Soonho Kong. Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction CADE-25- 25th International Conference on Automated Deduction,
Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer
Science, pp. 378-388, Springer, 2015. doi: 1111007/978-3-31-2110000
URL https:
10. 1007/978 3 319 21401-111100 26
Mohan Ganesalingam. The Language of Mathematics: A Linguistic and Philosophical Investigation. Lecture Notes Computer Science. Springer Berlin, Heidelberg, edition, 2013. ISBN 978-
3-642-37011-3, doi: 00.10077998-3344--37011 978-3- 642 37012-0
URL
Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Asian Symposium on Computer Mathematics, pp. 333-333. Springer, 2007.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2 (00.v:221333.0 103.03870333. 2021.
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. Mustard: Mastering uniform synthesis of theorem and proof data, 2024.
/tattts://arxiv..oom wttp:////bb///.//////932
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:231 03755, 2023a.
Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Munti-language diversity benefits autoformalization. In Proceedings the 38th International Conference on Neural Information Processing Systems, NIPS '24, Red Hook, NY, USA, 2025. Curran Associates Inc. ISBN 9798331314385.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023b. URL hhttps://open: wwwiopereeiieee review.eww.... net. Forummmmmm SM 9EAovKMC
Kimi Team, Yifan Bai, Yiping Bao, Guanduo Chen, Jiahao Chen, Ningxin Chen, Ruijue Chen, Yanru Chen, Yuankun Chen, Yutian Chen, Zhuofu Chen, Jialei Cui, Hao Ding, Mengnan Dong, Angang Du, Chenzhuang Du, Dikang Du, Yulun Du, Yu Fan, Yichen Feng. Kelin Fu, Bofei Gao, Hongcheng Gao, Peizhong Gao, Tong Gao, Xinran Gu, Longyu Guan, Haiqing Guo, Jianhang
12

---

Published as a conference paper at ICLR 2026
Guo, Hao Hu, Xiaoru Hao, Tianhong He, Weiran He, Wenyang He, Chao Hong, Yangyang Hu, Zhenxing Hu, Weixiao Huang, Zhiqi Huang, Zihao Huang, Tao Jiang. Zhejun Jiang, Xinyi Jin, Yongsheng Kang. Guokun Lai. Cheng Li, Fang Li, Haoyang Li, Ming Li. Wentao Li, Yanhao Li, Yiwei Li, Zhaowei Li, Zheming Li, Hongzhan Lin, Xiaohan Lin, Zongyu Lin, Chengyin Liu, Chenyu Liu, Hongzhang Liu, Jingyuan Liu, Junqi Liu, Liang Liu, Shaowei Liu, T. Y. Liu, Tianwei Liu, Weizhou Liu, Yangyang Liu, Yibo Liu, Yiping Liu, Yue Liu, Zhengying Liu, Enzhe Lu, Lijun Lu, Shengling Ma, Xinyu Ma, Yingwei Ma, Shaoguang Mao, Jie Mei, Xin Men, Yibo Miao, Siyuan Pan, Yebo Peng, Ruoyu Qin, Bowen Qu Zeyu Shang, Lidong Shi, Shengyuan Shi, Feifan Song. Jianlin Su, Zhengyuan Su, Xinjie Sun, Flood Sung, Heyi Tang, Jiawen Tao, Qifeng Teng, Chensi Wang, Dinglu Wang, Feng Wang. Haiming Wang, Jianzhou Wang, Jiaxing Wang, Jinhong Wang. Shengjie Wang. Shuyi Wang, Yao Wang, Yejie Wang. Yiqin Wang, Yuxin Wang. Yuzhi Wang, Zhaoji Wang. Zhengtao Wang. Zhexu Wang, Chu Wei, Qianqian Wei, Wenhao Wu, Xingzhe Wu, Yuxin Wu, Chenjun Xiao. Xiaotong Xie, Weimin Xiong, Boyu Xu, Jing Xu, Jinjing Xu, L. H. Xu, Lin Xu, Suting Xu, Weixin Xu, Xinran Xu, Yangchuan Xu, Ziyao Xu, Junjic Yan, Yuzi Yan, Xiaofei Yang. Ying Yang. Zhen Yang, Zhilin Yang. Zonghan Yang. Haotian Yao, Xingeheng Yao, Wenjie Ye, Zhuorui Ye, Bohong Yin, Longhui Yu, Enming Yuan, Hongbang Yuan, Mengjie Yuan, Haobing Zhan, Dehao Zhang, Hao Zhang, Wanlu Zhang, Xiaobin Zhang, Yangkun Zhang, Yizhi Zhang, Yongting Zhang, Yu Zhang, Yutao Zhang, Yutong Zhang. Zheng Zhang, Haotian Zhao, Yikai Zhao, Huabin Zheng. Shaojie Zheng. Jianren Zhou, Xinyu Zhou, Zaida Zhou, Zhen Zhu, Weiyu Zhuang, and Xinxing Zu. Kimi k2: Open agentic intelligence. 2025. URL https: /taps://axxii or /tg//b//////oo 20534.22333
Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Aut- oformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024a. URL
https://ceee https://cpenreview net
Zenan Li, Zhi Zhou, Yuan Yao, Xian Zhang, Yu-Feng Li, Chun Cao, Fan Yang, and Xiaoxing Ma. Neuro-symbolic data generation for math reasoning. Advances in Neural Information Processing Systems, 37:23488-23515, 2024b.
Hunter Lightman, Vineet Kosaraju. Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twelfth International Conference on Learning Representations, 2024. URL httpp:: http:::///peeervveeee
net. w1
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Grodel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025a.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang. Yihan Geng, Jiawei Ge. Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025b. URL https:
7/arxiv. org/ abs/ 2508 03613
Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. Deepseek-v3 technical report. arXiv preprint arX44:2412.19437, 2024.
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. Fimo: A challenge for- mal dataset for automated theorem proving, 2023. URL htt.https//// //ar//i////vvvv///// wwwpii..rrg/bboa org/abs/2309
04295
Qi Liu, Xinhao Zheng. Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards faithful metric and dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025a. URL httpp/
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data, 2025b. URL htttps://aaat org/ abs 05567
13

---

Published as a conference paper at ICLR 2026
Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. Formalalign: Automated alignment evaluation for autoformalization, 2024a. URL
abs/2410. 10135
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang. Jing Tang, and Zhijiang Guo. Process-driven autoformalization in lean 4, 2024b. Utthtts:::/arat
org/ abs 2406. 01940
Shashank Pathak. Gflean: An autoformalisationn framework for lean via gf, 2024. URL https
7/arxiv. wtt.oorgg//bbaooooeoeee 01234
Lawrence C. Paulson. Isabelle A Generic Theorem Prover (with contribution by T. Nipkow), volume 828 of Lecture Notes in Computer Science. Springer, 1994. ISBN 3-540-58244-4, doi: 10.1007/BFB0003044. URL https:ss:s :ttp::://doi..o http:////.i...r/.../// 1007 1000//F0000005001
Z. Z. Ren, Zhihong Shao, Junxiao Song. Huajian Xin. Haocheng Wang. Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma. Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover--e Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL htttt:/ss///rxx
org 2504 21801
Christian Szegedy. promising path towards autoformalization and general artificial intelligence. In International Conference on Intelligent Computer Mathematics, pp. 3-20. Springer, 2020.
Gemini Team. Rohan Anil, Sebastian Borgeaud, Jean-Baptist Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew Dai, Anja Hauth, Katie Millican, al. Gemini: a family of highly capable multimodal models. arXiv preprint arXiv:2312. 12. /805, 2023.
Trieu H. Trinh, Yuhuai Wu, Quoe V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995) 2024. ISSN 1476-4687 doi: 10310 141586-023-06747-55 URL/ttps://6oioor///D0
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem provers putnam mathematical competition, 2024. URL http::ttt///.mm /ttppi:///aavv../// org/ /aads//2447..m 240. 11214
prroverm-poovers on the
Peiyi Wang, Lei Li. Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce LLMs step-by-step without human annotations. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar (eds.), Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 0926-933,, Bangkok, Thailand, August 2024. Association for Computational Linguistics. doi: 10. 18653vv// 2024.acl-long.511 URL htt.httt:://at antho logy oro.orgg/22222 http:/2224.ccl1111...
Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Autoformalization the era of large language models: A survey, 2025. URL https 7/arxiv. org/ abs/
Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS '22, Red Hook, NY, USA, 2022.
Curran Associates Inc. ISBN 7781713871088.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang WU, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. BFS-prover: Scalable best-first tree search for LLM-based automatic theorem proving. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (eds.). Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pp. 22588-325999 Vienna, Austria, July 2025. Association for Computational Linguistics. ISBN 979-9- 1779--889976-25---1 //aclanchology. wwg.://..oooooooo
doi: 10.18653/v112000 1/201//2c2-ooooo 1565/
URL https
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin
14

---

Published as a conference paper at ICLR 2026
Yang. Jiaxi Yang. Jing Zhou, Jingren Zhou, Junyang Lin, Kai Dang, Keqin Bao, Kexin Yang, Le Yu, Lianghao Deng, Mei Li, Mingfeng Xue, Mingze Li, Pei Zhang, Peng Wang. Qin Zhu, Rui Men, Ruize Gao, Shixuan Liu, Shuang Luo, Tianhao Li, Tianyi Tang, Wenbiao Yin, Xingzhang Ren, Xinyu Wang, Xinyu Zhang, Xuancheng Ren, Yang Fan, Yang Su, Yichang Zhang, Yinger Zhang, Yu Wan, Yugiong Liu, Zekun Wang, Zeyu Cui, Zhenru Zhang. Zhipeng Zhou, and Zihan Qiu. Qwen3 technical report, 2025,
abs/ 09388
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: theorem proving with -aumenedd language models. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS '23, Red Hook, NY, USA, 2023. Curran Associates Inc.
Kaiyu Yang, Gabriel Poesia, Jingxuan Hc, Wenda Li, Kristin Lauter. Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: new frontier in ai, 2024. URL https:
arg/abs/2uun 2412. 16075
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jaayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. URL httptttss///ppeeeeeeeee wwteeeewwwwwweeeeeeeeeeeeeeeeeee
net. ftre/forumit id=Vcw3vz
Jiyao Zhang, Chengli Zhong. Hui Xu, Qige Li, and Yi Zhou. Kelps: A framework for verified multi- language autoformalization via semantic-syntacti alignment, 2025. URL pesttps:/arxae
arg/abs/2507. 08665
Lan Zhang, Xin Quan, and Andre Freitas. Consistent autoformalization for constructing mathematical libraries. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen (eds.), Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 4020-4033, Miami, Florida, USA. November 2024. Association for Computational Linguistics. doi: 10.18653/v1/ 2024.emnlp-main 233. URL httpp:ss//cllaaacooooooo.oo
emn emnlp-main. 2333/
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022.
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't trust: gerify-grounding Ilm quantitative reasoning with autoformalization. arXiv preprint 40X 2024.
15

---

Published as a conference paper at ICLR 2026
APPENDIX A DETAILED DISCUSSION ABOUT FORMALIZATION TEMPLATE
A.1
TEMPLATE DETAILS
The LoC-Decomp template departs from prior approaches that formulate Lean 4 formalizations as t hhoorem declarations with sorry placeholders. Instead, we represent the original statement as predicate named probl This design enables LLMs to organize Lean 4 content in a structured, step-by-step manner, thereby enhancing formalization quality.
that builds upon series of previously declared definitions.
The template is grounded in a key conceptual insight: any mathematical problem investigates the properties of mathematical system-a collection of objects along with constraints that govern their properties and relationships. We represent such system using Lean 4 st structure named MySystem, which encapsulates all relevant mathematical objects, along with a series of predicates that describe the constraints and properties of this structure. The problem itself is then formulated as a predicate that examines a specific property of this system.
Take solve-type problems for example, the template comprises the following six sequential steps:
Environment Declaration. A fixed, predefined setup imports basic Mathlib dependencies, opens namespaces, and defines some notations.
1 import Mathlib
2 -->>declare_ seveclare_envrrmentt
3 open Real InnerProductGeomettry Matrix Topology Filter ENNReal Polynomial Classical Complex
4 notation "R""n EuclideanSpace (Fin n)
5 notation "M[" ", n "]" => Matrix (Fin m) (Fin n) R
6 notation "g" x ", "3" => Qinner R
7 variable (V : Type} [NormedAdddCmmGroup v] [InnerProducttpace & v]
noncomputable section
10 \-Lean4 Code Here-\
11
12 end
Figure A-6: The environment defined in the template. All Lean code resides within this environment, so in what follows, we will simply omit it.
Auxiliary Types Declaration. The LLM may declare custom types (e.g., structures, inductive types) to model complex concepts, leveraging Lean 4's dependent type system without unnecessary restrictions. Since Lean 4's expressiveness stems from its rich type system, this step imposes minimal sagurrement--allovinng any type declaration that facilitates formalization while preserving the template's overall structure.
3. Mathematical System Declaration. A ructure named MySystem is declared to abstractly model the problem, containing all mathematical objects (e.g., functions, equations, geometric shapes, groups) along with their types. This step serves the foundation for formalization, requiring the LLM to identify and declare every relevant object- from concrete entities like sequences and matrices abstract structures like groups and topologies thereby creating comprehensive representation of the problem's 's mathematical context.
4. Auxiliary Functions/Preedicates
Declaration. Helper functions predicates are defined to simplify subsequent constraint expressions. These auxiliary definitions capture recurring patterns or complex relationships, promoting modularity and readability in the formalization.
16

---

Published as a conference paper at ICLR 2026
5. Constraints Declaration. The LLM declares predicates that define the logical constraints and rela- tionships among objects in MySystem. Each constraint predicate predicate-named with the wconstraaii suffix for cparity-specifes properties or connections that mathematical objects must satisfy, thereby encoding the problem's 's logical structure in a verifiable form.
predicate problem. problem_statemmee stant over a free variable solution. Unlike prior approaches using theor em declarations with sorry placeholders, we reformulate solving-type problems propositional func- tions: for any instance of MySystem the conjunction of all constraints implies a proposition about the solution variable. This design establishes a direct formal correspondence between the Lean representation and the original problem's 's semantics, where the predicate holds precisely when the provided solution is valid.
6. Problem Statement Declaration. The overall problem is formalized
A.2 DETAILS ABOUT THE PARSER AND THE RECTIFICATION STRATEGY FOR TEMPLATE COMPLIANCE
The parser have implemented will parse Lean code according to the template. In the auxiliary type declaration section, no additional requirements will be imposed, ensuring the Lean 4 type system remains fully intact. The system declaration section requires that the Lean 4 code must define a st struture named MySystem using the declaration section mandates that functions must be defined with the def keyword, and parameters are strictly prohibited from being of the MySystem type (to emphasize the auxiliary nature of these functions). The constraint declaration section requires definitions with the def keyword, and parameters must strictly be of the My em type (highlighting constraints the system). The problem statement section requires definitions with the def keyword and must be an implication expression under universal quantification like "V sys MySystem, consists of all constraint conditions, and the consequent a predicate term related to the free variable solution (or proof.ooooooooo loooooooolllooooooooooooooo 1 for proof-type problems).
keyword. The auxiliary function
where the antecedent
the generated Lean 4 code does not conform to the template, a rectification mechanism is activated. This mechanism provides error feedback from the parser and prompts the L.LM revise the Lean code by appending the error information to the context. Whenever new Lean code is generated, undergoes parsing and semantic rectification, or syntactic rectification. Some parser error information are as follows:
reriaaadiin--rrrellesssee of the current stage, whether is formalization,
you can only declare one struc- Error occurred, constraints must be declared by using def.
Error: in the step of dec declare.mate www.eeettttttttaattaseeee ture named MySystem.
Error: in the step of declare the problem statement you can only declare one predicate named proble problem em statement.
Error, the antecedents in the problem statement's implication must contain all the constraints declared in the constraint declaration section.
A.3 EXPLANATION FOR NONCOMPUTABLE SECTION
Within the domain of high school mathematics, natural language mathematical descriptions (i.e., classical mathematics) are typically grounded in first-order predicate logic-a framework that differs significantly from the dependent type theory underpinning Lean 4. A key practical distinction lies in the treatment of function domains: classical mathematical definitions often implicitly specify the domain through contextual cues and the expression of the function itself, whereas Lean 4's type system requires explicit and precise domain declarations.
This difference considerably complicates the formalization of classical mathematical texts. Since the domain is frequently left implicit in the original discourse, translating such content into Lean requires inferring the domain-4 process that be non-trivial for more complex functions and is sometimes the explicit goal of certain mathematical exercises. However, this act of deduction may introduce semantic discrepancies if not carefully aligned with the original intent.
17

---

Published as a conference paper at ICLR 2026
In the present work (as opposed to prior approaches), employ a strategy commonly adopted in the formalization classical mathematics: placing relevant declarations within noncomputable section. This allows to avoid prematurely imposing constructive computational constraints- such as enforcing specific function Monains-unless they are directly stated in the original text. The approach maintains mathematical rigor, domain constraints remain logically inherent in the definitions and can be formally derived and verified during the formalization process.
is important to emphasize that this method does circumvent the core challenges of formalization; rather, by utilizing feedback from Lean 4's type system (provided to the LLM during interaction), we can iteratively and efficiently render these implicit elements explicit while respecting the original mathematical meaning.
A.4 PROOF OF THEOREM 3.1
Here, we complete the proof of Theorem 3.1 by providing a method to convert any complete Lean proposition into LoC-Decomp template and demonstrating that the result generated by this method is equivalent to the original Lean 4 proposition.
Without loss of generality, the assumption here is that the proposition be converted is defined by theorem and named as cheoremea.. www.ttt.coovvrre along with a series of dependency declarations existing in the context. And the template selected here is the proof type template. The conversion process involves placing all the aforementioned dependency declarations into the auxiliary type section. In the mathematical system declaration section, the MySystem structure contains only one object: proo f-goal. We then need to transform the and name as theorem converted, prop, which can be done manually or simply call Il Iicheck theorem to convert to get the corresponding type that is exactly the proposition of the theo- rem. The constraint declaration section includes only one constraint, proof_gov 1 __const ra int, theorem..coverteed.ae
into a proposition
which states that sys pwoo declaration section, the implication premise contains solely www.oo.ooa...oon.too implication conclusion is sys wys.proof.goo...ooo proof.goal.
In the problem statement and the
Once such a conversion is performed, the resulting output will conform to our template and can be accepted by the designated parser. Then we have to prove that the probl bobblemmsttteeent is logically equivalent to the theorem converted prop, and we prove this by Lean 4 itself. For adopted generic sorry placeholder express a proposition. Since
the sake of universality, proof operates at the meta level, this proposition can be replaced with any proposition, and our proof can pass the verification of the Lean compiler. See code [ for detailed information.
18

---

Published as a conference paper at ICLR 2026
Code 1: Convert theorem to it's Loc-Decomp counterpart and prove the equivalence
aabeclaro__axiliarryy
--Al1 the dependent declarations should be declared here.
-->>declare - mathemattical__ssten structure MySystem where proof_goal : Prop
-->>declare pe>xeclare_auxiliate functions, or predicates
def theorem converted prop Prop := sorry
-h sorry place holder can be replaced by any proposition.
def proof__gaal_contrraateee (sys:MySystem) Prop :=
sys.procf_goal aeeorem_converte__prrg
--> htteecaarr_ttc_prooleeetteeee
def grooblemsstatemet Prop
sys : MySystem, proof_geal Lcagaaal_cnstranit sys +
sys.proof_goo
theorem equivalence : problem statement
Sthoree_convertee prop by
constructor
intro h unfold problen_statement let sys : MySystem := choorem_converted_ppr
h
have constraint :
sys : by
unfold proof__oal_constraaee
rfl
have h_sys_proof_goal sys.proof_goal sys constraint.
exact p_sys_proof__oo
intro h h_constraint rw [h_constraint] exact
Although this conversion not elegant, it theoretically ensures that our template does not impair Lean 4's expressive power in any way.
A.5 MINOR MODIFICATION PROOF PROBLEMS
When handling proof-type problems, the sol-objecd ject is replaced by proof-gee f-ooal of type Prop, which corresponds to the proof objective in the original problem. Similarly, the solution- constra nt. is replaced by proof goal const ra i nt, which defines the proof goal con- cretely. The free variable so solution on removed from the probl sem_statement. as proof-type problems do not require any free variables. In this context, the consequence in the problem statement corresponds to sys proof...... f-goalllll-- for all problems. With these minor adjustments, the template becomes suitable for proof type problems, and our parser remains effective in detecting any violations of the template. The framework only requires preliminary check the problem type to determine which template to use. See figure 6 for example.
19

---

Published as a conference paper at ICLR 2026
-=>odeclare, tirr, typex
--adderiars, aucil Eirry types
-No sovzltery types needed for tois pronten.
--to ausr types needed for this problee.
--oodhclare, www.socheeiiill.poeooooo structure MySystan
--addesiare, wwchmertiiee rystem
stracture RySysten whare
(a b R)
b. : RD
[ B
7
sol_,um,a__
proof_gool
18 Sodectare, aovillory, fonctions, oz predicates
10 endectorv, autilfory, Dont Liois, Or or.orddicatess
11 def cortinuns, polto ON RD if R) Prop
11 def continious at (Aa R3 (E R R) Prop 1n
3,2 xX.
[fx-
Y 3,0
[f fx]
14 ->odeclare, constratats
16 --andectore -osdetorrccnsserstne consersines
15 def function, e<presston_constree constraint (sysi9/5ysten) : Prop 2n
15. def finction, cupresssio__ccnstraiii (sys:HyGysten) Prop
x
5ys.t
sys.a
sys.a
18 else if 5 x then x- 3px.5
10 e'se xxx. 5 ther x
29 +law
19 w.se 2 kys.b
28
def alebol www.ointnnttss..ommoo construint Gaschosyyste)) R, cont inuoux paint Xs sys.f
Def-g' shalssbblooooooouuuu consteuint (sysolidystie) continumu, eI puintt Ne sys.f
22
23
23
24 def solution celution_ccnstteant constraint (syschyaystee) Prop
def peoof goal, constraint (sys:Hyyystee) Peop
3ys.5ol_sur.o.>
sys.b
(sys.a
.-2vdeclarc_ che_probiee statesent 27
27 --axdectare, tRC tnc_prablee statewnnt
28 def problou stw.ssttoonn: (solucion RJ 1.00p--
18. def problen statemont Prop
sys MySysten,
MySystee,
function_e<preet
constraint sys
funce exgressson_cconteesitttt sys
zicbal continurus censtraint sys 31
31 g.obrl contimuzus conttraint sys A
32
solution_ constevint
32
proof_ppot. conntraint 5y5
solution
sys.pronf
Figure A-7: Converting the example formalization into proof type
kibala
dectare Larr oypes +)
(e cactang_wodtdarry.o tyyps +)
(r aarillary reeded far thdx preplar. +]
(r As auzzidary typae coandd for ctder problem, x)
avetary watloestticall +)
(e seeteve www.waatteooitttt.cmmm syadon +]
hydysten
Tesord tySyyben : Type :e
8 R:
6 R:
Traal mext"
R > 101_sur_u
detunition continunus at potet "rast (raa) real) beol" shere "cantinunur, stuttet
www.aarrrrt....r...... atrrerieee_essrettttaaeeeee x)
letinition continoos.
(9e0d. 1250. yx. be xel If +xx) x.*
coritrattttttttttttss. deftattton funcrfos wtw.saaaaeeeseetssrttttttt 11 *hySystee acol*
Rubs
"furction wwwps/esssoncccocmo constratat
saeetvttse befinition funttfon constraatt Myfyctee) Proz feratt
(tx.
3
then
9v52)*
if tgt.doo Die Eoys (a) + 33
definition slotol wtw.ntttioooss.oosstttttttt wonstraist "Nyšysten bost"
in ast Ctpe.abor 6.223 (rtoutee 20 Usn Ce st olse C2 eys. (t3).
"ststal, wwntirowrr..oneeetttooo (vsulreat, continitos.at.oiin sys)>*
Zerinittznn paaatt_ontrrooocccooo conntraies furs Hydostun) : frop foratt by B, contivassssat.uu pcant (t).
deflaition sotation constratet "HySysten
"soluttis. cosetraint
sevinition sotatinn toys hySystea) : trop 1* sys. tesl_oe b. sxe. oys.
dectovy the erobien atacement tertanition atatsmnt (sclotion fro forall svs *syystes, www.tin.asresiia..oootte
definition prosliee statesent *reat bool"
constraset eye
sotation, constraint
sotartin_caretratne aye sotution (usl,
Figure A-8: Template suitable for Isabella and Coq example
20

---

Published as a conference paper at ICLR 2026
A.6 DISCUSSION ON FEW-SHOT EXAMPLES
In this work, we adopt a few-shot in-context learning approach with a set of manually curated examples. Our collection comprises 38 Lean 4 codes that conform the formalization template and cover a variety of problem These examples are drawn from the MATH-12500 dataset (Hendryeks et al. (02I), with only blank overlapping with the MATH-500 dataset. For each problem, we first determine its domain and then retrieve approximately
functions, probability, combinatorics, and geometry.
16 relevant examples from that domain use as few-shot demonstrations. In our baseline methods, the same set of few-shot examples is used, with the only modification being that the Lean code transformed to a theorem with sorry.
A.7 EXAMPLES FOR ISABELLA AND COQ
Our proposed framework is not only compatible with Lean but also be adapted other theorem provers such as Isabelle and Coq-given the provision of a suitable parser and minor prompt modifications. This flexibility stems from the template-based design of framework, which can be applied to any proof assistant that supports a type system, the definition of structures (such as 'record' in Coq). as well as predicates and functions.
For Coq, which- like Lean 4- supporrss dependent type theory, the adaptation process is relatively straightforward In the case of Isabelle, which uses a simple type system, certain expressive features may be limited; however, these remain sufficient for handling high-school-leve mathematical prob- lems. We illustrate the adaptation of our template both Isabelle and Coq using a simple example: the same piecewise function problem discussed in the main text.
21

---

Published as a conference paper at ICLR 2026
APPENDIX B ASCC WORKFLOW DETAILS
The procedure consists of the following steps:
First, supply the LLM with segmented segments of the Lean 4 code along with their corresponding natural language translations. The model is then prompted to identify any discrepancies between auxiliary functions or constraints and the original problem, under the assumption that all other components are correct.
Second, the complete Lean 4 code and its full natural language description are provided, and the LLM is instructed to detect any potential inconsistencies between the two.
Third, all identified discrepancies are compiled and presented the LLM, along with the original problem and the Lean 4 code. The model is then asked to assess whether each discrepancy is critical or acceptable based on predefined criteria.
Fourth, the LLM is required to evaluate the overall consistency level by considering all critical discrepancies that have been identified.
Finally, if the code is deemed not fully consistent, each individual discrepancy is isolated and reevaluated by the LLM confirm its validity. For each confirmed discrepancy, the model must provide specific recommendations to amend the Lean 4 code. The formalization is considered inconsistent if any discrepancy is judged to be genuine.
B. ASCC JUDGE CRITERIA
Criterion 1:
Object Omission
Not all mathematical objects in problem original are reflected in the Lean 4 code or their types mismatch. As long the objects are correctly reflected, some redundancy in the Lean code are acceptable.
Criterion Semantic Alteration
The definitions, properties, relationships of any mathematical object from problem original are not exactly preserved the Lean 4 code. Some redundancy is permitted as long the core semantics are constrained correctly.
Criterion 3: Constraint Incompleteness
The constraints expressed in problem formal fail to comprehensively represent all explicit and implicit constraints present in problem original.
Criterion 4: Over Simplification
The Lean code conducts concrete computation derivation that simplifies the original problem, leading to a semantic inconsistency.
B.2 ASCC CONSISTENCY LEVEL DEFINITIONS
Consistency levels
Fully consistent
Fully consistent by the final criterion.
Consistency levels 2: Consistent without loss of generality
Consistent without loss generality: The Lean code formalizes the problem by analyzing representative cases. In each of these cases, the final criterion are fully satisfied, and the general case follows through straightforward deduc- tion.Or the formalization rely equivalent conversions, such as transforming canonical equations into general form. In such cases, the formulation can be regarded consistent without loss of generality.
Consistency levels 3: Inconsistent
Any criterion breaked can lead to this, long not Consistent without loss of generality.
22

---

Published as a conference paper at ICLR 2026
APPENDIX C DIVIDE AND MERGE DETAILS IN BACK TRANSLATION
We adopted a hierarchical approach to decompose the Lean code into multiple self-contained segments. The system segment includes all auxiliary types and the MySyst em structure; the auxiliary function segments comprise each auxiliary function along with its de- pendencies and the system segment; the constraint segments encapsulate each constraint together with its related auxiliary functions and the system segment. The problem statement itself is not processed separately, as the semantic meaning of the problem statement can be fully constructed from the segments described above. The divide strategy simplifies the complex back translation task into several simpler subtasks. Ensures that each segment can be accurately translated in isolation without relying outer contextual information from other parts of the code, thereby reducing ambiguity and errors during the LLM processing phase.
Divide:
After translating all segments, the natural language description of the Lean 4 code could, in principle, be obtained by simply concatenating them and adding a statement of their logical relationships. However, such direct approach would result in a tediously long output, which could distract the L.M during the subsequent semantic check step. Instead, we perform conjunctive combination of the constraints in natural language. This is achieved by sequentially merging pairs of constraints and instructing the LLM to restate them cohesively, leveraging the fact that their logical relationship in the original problem statement is simply conjunction. The final translation of the Lean 4 code consists of three core components: a system description, a auxiliary functions description, and constraints description, which are integrated with a description of their logical relationships
Merge:
23

---

Published as a conference paper at ICLR 2026
APPENDIX D HUMAN EVALUATION CRITERIA FOR SEMANTIC CONSISTENCY
The detailed criteria for manual inspection are as follows:
1, Whether the formalized problem discusses the same mathematical objects as the original problem (redundant auxiliary objects are allowed, and individual objects may be expressed as sets);
2, Whether the logical constraints of the original problem are correctly expressed (under the current constraints, all object properties and relationships are consistent with the original problem); if certain constraint expressions are not generally correct but are correct in the current context, they are still considered valid;
3, Whether the truth value of the formalized problem statement corresponds exactly to that of the original problem taalem--hattte is. for given set of concrete objects (including solution in the case of a solve-type problem), the formal statement holds true if and only if the original problem true;
4. We impose no additional requirements on the form of the solution (c.g., some problems require solution in degrees, but solution in radians are also considered correct as long as they are practically equivalent). This is because Lean 4 has limited support for symbolic computation, making it difficult to satisfy certain formal requirements (e.g., requiring expressions be in simplest form).
5, Consistent without loss of generality: The Lean 4 code formalizes the problem by analyzing representative cases. each such case, the final criterion fully satisfied, and the general case follows through straightforward deduction. A Alternatielyy the formalization may rely equivalent conversions- ssushssuhhha as transforming canonical equations into general form- or the expression may hold only in the current specific context, even if not generally valid. In these situations, the formulation can be regarded as consistent without loss of generality.
->2adecianc, auxi tiary Larryyyyyee types
The Lean4 code only expresses the horizontal asymptote in the positive infinity direction and overlooks the horizontal asymptote at negative infinity, However, in this problem, the horizontal asymptotes at negative infinity and positive infinity are the same, so we consider this to be a consistent representation without loss of generality.
auxdliary types for probles
3 --bodeciare, --Sxdeciarc_natheeee www.eeetticallyyeeeeee... system
structure NySysten f R R b R
18
--aodectams Lareectane auxitiary functions or predicates
11.
def has, www.eeeiallssyyoootttteeeeeeeeee
(4. PEop
12
y [L R), (c R),
14 def has
(f
R
RD
R) Peop 28
(f
16 --oddeciare, constraints
def function,
constraint (ays MySysten)
18 sys.f - x >> (2 (x"2 5 +. x 144
def versicsl_symptoes_ccom
(sys MySyston) Prop
28 has, has_vercical_ssyypooooe has_verrice__smmooote_.tt
sys. sys.a A
22 sys.a - sys.b
def Inrizan'al, wtw___apttt___mmmem conntrwint (sys MySysses) Prop has eespottte_syyttteeuutt sys.f sys.c
Problem:
The graph of (x) 12-5x-14
2x
25 def solution constraint (sys MySystes) Peop
26 sy5.5ol, sun sys.a sys.b sys.
27 ->ddectare, the www.ooroootttttteooooeeee statonent
has vertical asymptotes and b, and horizontal asymptote y = c. Find a + b + c.
def probles_statanee (solution R) Prop
29 Y MySysten,
sys
31 vertical_ verticel_esymptoter consstraet sys
horizon:al_esyyoeee sesnpooote_onstrrinn sys
33 solution consteaint sys -
solution sys.sol_som
Figure D-9: Case study for consistency without loss of generality.
24

---

Published as a conference paper at ICLR 2026
APPENDIX E MATH-ASCCC-EVL-1550 DATASET EXPLANATION IN DETAIL
We construct the MATH-ASCC-EVAL-1155 dataset through the following steps:
1. Using the method proposed in Section3.1 with DeepSeek-V3. V3, we perform a pass @ / NL2Lean4 formalization procedure. The generated Lean code is then evaluated by ASCC-1, and each instance is categorized based on (level, ASCC- result) pairs.
2. From the above outcomes, we randomly sample the following from each category:
10 instances of (level 1, ASCC-I pass)
10 instances of (level 1, ASCC-1 not pass)
10 instances of (level 2, ASCC-1 pass)
10 instances of (level ASCC- not pass)
10 instances of (level ASCC-1 pass)
10 instances of (level ASCC-1 not pass)
20 instances (level 4, ASCC-1 1 pass)
20 instances of (level 4, ASCC-1 1 not pass)
25 instances of (level 5, ASCC-I 1 pass)
25 instances of (level 5, ASCC-1 1 not pass)
3. We conduct human evaluation based on predefined criteria to determine the ground-truth consistency between each problem and its corresponding Lean 4 code.
4. After human evaluation, the final dataset consists of 97 positive cases and 53 negative cases.
In MATH-ASCCCEval-L500 the negative cases contain subtle semantic inconsistency, which are hard to detect. Some cases are as follows:
Case studies for nuanced semantic inconsistencies in MATH-ASCC--Evll-a
25

---

Published as a conference paper at ICLR 2026
In the following problem, the Lean4 code on the right fails to capture the fact that points B, C, and D are collinear and points A, C, and F are collinear. This information implicit in the original problem, resulting in incomplete constraints in the Lean4 and inconsistency with the original problem. ASCC-3-MV successfully captured this semantic discrepancy.
--ddeelare aucitiary Eypey
structure Triangle shere
C R"2
-oddectare wwthenrrica
structure mySysten where
Trtargle
14 E 123
11 s2L
--adec
cross_sroduct
14. V v.1 K.W
15. def trisngle_aren aree (t Trisngte) 2T
16.
1.A
[erovxprratact AC]
19 def peraltet (v a RP2) : Peop ie cross_prodict V
20 ->ggeclrr constrofats
MySystee) Prop triongte_aree PySystee)
parattel_constratnn
sys.ARC.n 1y5.406.
2-
1et OE 2" sys.E - -9y.0
parallel Ab
Pydystom)
27
RyS.48C.C AYS.
Problem:
20
1et. 80 >- sy5.0 D SyS.AAC,
20
[00j
[0c]
The area of
30
solution_ www.sossstttttt..
PySystee)
ABC is square centimeters.
avs.anl area CBE trianzle area
ayaut)
>>d0ctove www_ppoot.. StotonnnT
AB|DE. BD = 4BC. What is the number of square centimeters in the area of A CDE?
14. def pooblen_statemee isolation Prop
16 aeca, constroint
37 peraltet constraint sys
10 an, natio natinn constraint sys
19 solutiin,constriiin
solution sys.sol..ree_com
Figure E-10: Case study 1 to illustrate the nuanced inconsistencies in MATTHASCCC-EVa--155
The constraint the red box does not require that all x satisfying the condition are in the possible_x set, but only mandates that elements in possible_r must satisfy the condition. This is inconsistent with the semantics the original problem. ASCC-3- 3-M successfully captured this semantic discrepancy.
-->odectare auxiliary types
auxiliary types needed for problem
--oodectare ->>dectare_ettheaaticcl system
structure MySysten where
possible_x Set sol_values Set
-->odectare_ auxiitirr_xiiirrr__eoaa functions, _r__oorr________ def cubic_expression 3) R := x 24x
poritierr_functionn...
12
-->ddeclare constraints
13 def quadratic_ eee.eequttio cequatio__contrraiii constraint (sys MySysten) Prop :=
14
v x c possposs, x"2 x -
15
16 def colution_constroing (sys MySysten) Prop :=
Problem:
17 sys.sol_valure *
If ~ is the value of x²3 2x 1?
0, what
18 [y x posppossib, cubic_ exprrssiepesssnnn x]
19
20 -->adectare the_probled proppleesssttteeeet statement
21 def problen_statee statement (solution Set R) : Prop
22 v sys MySysten,
23 quadratic equation constraint sys
24 soluttion_conttrinnt
25 solution sal_sollalles
Figure E-11: Case study 2 to illustrate the nuanced inconsistencies in MATH-ASCC--Eal-IR
26

---

existing Nathtib functions Published as a conference paper at ICLR 2026
APPENDIX F CASE STUDIES FOR ITERATIVE RECTIFICATION ON MATH-50
As illustrated in Figure F-13 the top half of the diagram demonstrates the output of our method during the iterative rectification process. The left portion shows the generated result prior to rectification, which is inconsistent with the original problem. This inconsistency arises because the triangle constraint does not prohibit the points from being collinear. As illustrated in the right portion of the figure, the ASCC successfully detected and corrected this discrepancy (among others) in subsequent iterations, whereas the baseline method made the same error without detecting The LLM response generated by DeepSeek-Ve 3 is as F-12
("discrepancies":
"The arthacenter incorrectly defined the vector of the triangle's vertices, violating the correct geonetric definition of the orthocenter altitudes.", "The circunradius constraints or the solution, despite being required the original problen.",
intersection point of the included the MySysten structure but
any
"The solution sol_sun_squaree is calculated purely geonetrically without being expressed in terms of a, b, c, and R as required by the original problen. Additionally, the orthocenter calculation is incorrect.",
"The orthocenter Н is not uniquely determined by the given constraints, violating the Exhaustion Principle of Predicate Satisfaction. The placeholder definition "sys. vec_add (vec_add C) does correctly compute orthocenter."). "recomeendations":
"Replace the placeholder definition the orthocenter with a correct geonetric definition. For example, use the fornula for the orthocenter in terns of the vertices and the circumradius, or implement function that computes the intersection point of the altitudes. The corrected definition should comply with the Mandatory Lean4 Template.",
"Add constraint that relates to the triangle ABC, such defining it as the circumradius the triangle. exanple, add constraänt "circunradius, constraint" that triangle's side lengths angles enforce this relationship.",
computes
"Nodify the selution_constraant express sol_sun_squares terns of a, b, c, using the known formulla (9R* (a' + b² c²)/2). Also, implement a correct orthocenter calculation.",
"Replace the placeholder definition with correct computation of the orthocenter. For exampte, the arthocenter triangle. Here is corrected definition: "eean
computed the intersection point of the altitudes of the
def orthocenter_comm coonstrrnnnn (sys:NySystem) Prop 1=
let (A, B, C) := sys. triangle
1et altitude_A :=
Compute the altitude fron to BC
let altitude_B B :=
Compute the altitude fron to AC
intersection_point altitude_A altitude_B Assuning a function compute intersection points
Note: implementation altitude intersection point computations depend on the available geonetric functions the Mathlib ")b "consistency_Level!! "Level_3"}
Figure F-12: LLM response during ASCC check
27

---

Published as a conference paper at ICLR 2026
Problem:
Let G and H denote the centroid and orthocenter of triangle ABC, respectively. Let F be the midpoint of GH.Express AF2 + BF² + CF2 in terms of the side lengths a, b, and circumradius of triangle ABC.
Our method
auytifory 'ypes
stoucturs Teiangle alsce
RT2
RTS
--oodccterc, wachonortcol systoe
Structure Mysyscen whire
Levengie Trasngle
3 5 RT2
31
10
RT5
11
F RTF
32
15
6
14
50l,
Con Deeguan
--odeecters, anditirry, foncrdens, orediccats
find widpote: W722 div Cver,
dist_sq R722
Q.9
20
Bevdx dy-dy
knds +23
28 de telargte_consteetttt constraint 1sy5 9/y5:e23 teop 1-
Rectified to
Sot 16, b, 3 sys, trlange
20
sya.s x Beat.agrt (diat_aq D.C)
31 sya.b x Real.sgrt (diat_34 A.
spe.r Res1. (cint oq 4. Voneenneeeeeee
30
Tet 15, 3 sy9 srinntin
Sys.u + find, conteole B.C.
wrw.ccaster.cco cowattreinttttt................. (aseeR/ssste)) Prop
THE 15, sya.triangte
apdysted)
SEnvEsFEed arthscencer calovlatese (elacehoterr)
(vec_ads C)
find_nidpoiet
sye.tstangle
SyS 50", sqares
5 eist.99 sys.t dist.30 Sy5.
->adeelorr, pre.prsbies_seeee Statonret
2000lAR, staattmannttt (solution Prop
sys.
cow.ttaatttttttttttttc.....e..t. 655
59
artncconter constriint 9p5
51
ridacint, constralet 535
solution, conntraist aps-
53
solution syx. sqtarr
Baseline method
theoren condroid_or www.ortccceteeeniiiiittt.oppmmme
(ABCGHF: R*2) babeRt R)
(solution : R)
(h_triangle 3 (A 8 : R*2), A 8 8 A-
(h_ centroid G = (1/3 : R) (A+ ())
4.
thoorthocenter let AB :- B A;; let AC i- C- let BC :- C B;
<(1 A), BC = g(H B), AC3 0 A 4(H C), AB3 0)
(h_ midpoint (1/2 : R) (G H))
7. (h_side_ Lengghsss a dist B C A = dist C c = dist A B)
8. (h_circumradius Let AB := B - A; let AC C= A;
R dist A dist B C dist C / (2 |848, ACH))
10 solution (dist F)*2 + (dist F)"2 (dist C F) := by sorry
11
Figure F-13: Case study 3 to illustrate the rectification process compared to baseline
28

---

Published as a conference paper at ICLR 2026
APPENDIX G ADDITIONAL EXPERIMENTAL RESULTS
To further eliminate potential biases from the dataset and the base model used for data generation, we performed manual annotation 50 samples randomly selected from the outputs of KIMI-K2 on the miniF2F dataset. The sample set comprises 25 cases labeled as correct by ASCC-3-MV and 25 cases labeled as incorrect.
The annotation results show that among the samples deemed correct by ASCC, all passed human verification. In contrast, among those marked as incorrect by ASCC, 9 were judged as correct by human annotators. This finding aligns with the conclusions drawn from ASCC-Eval-1500 the ASCC method exhibits a low false positive rate and relatively high but acceptable false negative rate. These results, presented in Table 7 indicate that ASCC serves stringent evaluation criterion, which advantageous for our objective identifying errors for feedback and correction. Moreover, they further afirm that the accuracy metric derived from ASCC-3-MV provides a reliable and credible assessment.
Table 7: Evaluation of ASCC-3-MV results generated by KIMI-K2
Items
ASCC-positive ASCC-negative
Human-posine
25
9
Human- negatvve
16
We also conducted comparative experiment using Bidirectional Equivalence(BEg) the evaluation metric. The evaluation was limited to the LoC-Decomp method with KIMI-K2 as the base model, along with the best-performing baseline in the LLM-as-a-judge setup, Goodel-Autoformalizz 32B. The results are summarized below in Table g
Table 8: Evaluation using BEq on mini-F2F
Items
LoC-Decomp Gocdel-Autofrmaliian--2222
mini-F2F
62.82
54.91
The BEq-based evaluation reveals notable differences in absolute pass rates compared to the LLM-as- a-judge approach, which is expected given the probabilistic nature of LLM judgments and the current limitations automated theorem proving. Nevertheless, in terms of relative performance, the BEq results align with those from L.LM-as-a-judge: our method continues show clear advantage fine-tuned specialized models.
Detailed experimental setup: To perform BEq evaluation, it is necessary to formulate bidirectional implication theorem and supply its proof, as illustrated below:
Code 2: Lean theorem to prove the bidirectional equivalence
theorem bidirectional wewpanallleivvvaeeeeeeeeee
gencrated_prooosit..nn + miniF2f
: by
Here, miiniF2..riiginal.prooo dataset, while www.errrdddpprpooo.oo iin refers to the model-generated proposition. Since both the miniF2F dataset and the Lean4 code produced by Goedellautoformalizee-- V2 are structured as theorem statements awaiting proof, we first transformed them into predicate forms using the def keyword. This conversion carried out using the DeepSeck-V22 V3.1 model.
denotes the original proposition from the miniF2F
After constructing the bidirecti conaa.eqqivalenee automated theorem prover. The prover allowed up 10 iterative corrections in case of compilation errors. Only proofs that passed the compiler without errors were considered valid.
theorem, we employed DeepSeek- V3.11
We also report the self-check pass vates-wher "self-check" refers to single ASCC evaluation performed by the current model itself during the iterative process, as opposed to DeepSeek- V3 model usd in ASCC-3 thrruch one, two, and three rounds of iterative refinement the MATH-500
29

---

Published as a conference paper at ICLR 2026
and miniF2F datasets. The results show that the self-check pass rate increases with more iterations for both DeepSeek- V3 and KIMI-K2. In contrast, Qwen3-235B exhibits a significant deviation from standard 3SCC-3-MV metric. We argue this is because smaller-scale models struggle to make judgments on semantic consistency that align with human standards. See Figure G-14 for details.
98
95
MATH
miniF2F
Pass rate
75
75
73
15
Self
35
36
Rectification roundDerepeek V3)
Rectification roundkk
Rectificttion cound(Qwes-
Figure G-14: Self-check pass rate during iteration
APPENDIX H DETAILS ABOUT OUR BASELINES
For both the Formal-Baseling and saaaal-teertiv-Baseliin set and few-shot mechanism as our approach, except that for the baseline method, the formal Lean 4 code is transformed into a theorem with sorry like previous works works(Azerbayee al.) 2023a Li et al., 2024a Wu et al., 2022). For the the same with method, except it adopted basic semantic checker. The SFT-Baselin used the same configuration as the Formal- -anaal-Baseline, with the exception that the base model was replaced by SeepSeek-Prover-V2
adopted exactly the same example
the iteration settings are exactly
APPENDIX PROMPTS
I.1 PROMPT DIFFERENCES ACROSS MODELS
We observed that the Qwen3-2333 235B model tends to generate overly lengthy responses (resembling thinking mode despite being used as an instruct model). To address this, we introduced instructions such Your analysis must be concise but accurate. and Note: Avoid tediously long analysis. to guide the model toward producing more concise outputs. The inclusion of these instructions successfully reduced verbosity in the model's responses.
We further evaluated the effect these instructions on DeepSeek-Vy V3 and KIMI-K2. The results indicated that DeepSeek-V3 generated more concise content when the instructions were applied, which led to a performance drop on the ASCC evaluation using the MATH-150 dataset. In contrast, KIMI-K2 was largely unaffected by the instructions, demonstrating greater robustness to minor prompt variations.
We argue that this discrepancy is reasonable, as differences in training strategies and data can lead to varied output styles across models. Although some minor differences on prompt is acceptable in practice, these findings highlight a limitation of our approach: is susceptibility to specific prompt designs.
I.2 THE PROMPT USED FOR FORMALIZATION
# Please use Lean code to convert the textual description of the problem into formal representation.
## Instruction
The following is a middle school mathematics problem. Please use Lean 4 code to convert the textual description of the problem into a formal representation.
30

---

Published as a conference paper at ICLR 2026
Any mathematical problem specific mathematical system. mathenatical system consists of several mathematical objects, along with a set of constraints that 1imit the propertics or relationships of these objects, thereby defining the mathematical system under investigation. The requizement the mathematical problem is study particular property of this mathematical system. Therefore, a mathematical problem can be formally expressed by declaring a mathematical system composed of several nathematical objects and a series of constraints, and for any concrete instance of the system, the conjunction all these constraints imply statement about solution.
viewed the study the properties of
# Attentions
Note: You
need solve the problem, your task is solely translate the problen's s description into formal Lean 4 code. Note: For the naming of any symbols, if the stem explicitly provides a name, it should be consistent with the stem; otherwise, provide a reasonable name.
Note: The scle purpose of naming cannot be relied upon to convey semantic meaning or mathematical structure all such information must be expressed through the code's s logic.
improve code readability. Names
Note: Please pay attention to distinguishing the syntax differences between Lean and Lean 4.
#V Problem
The problem to be processed is as fcllows: coriginal_problent
## Response Template
Here, you should formalize the above problem in Lean4, strictly following the provided Lean4 template shown below. 'Lean
import Mathlib
-->>declare @eeeclareeevii ree_vii roment open Real innerProdduttteemmerry Matrix Topology Filter KNNRea1 Polynomia Classical Complex
notation "R""n BuclideanSpace R (Fin n)
notation "M [" ", mj => Matrix (Fin m) (Fin n) R
notation "(("
"})" einner R R__xp x
variable (V Type) [NormedAdeCommGroup V] [InnerProductspacee R V]
The foundational environment has been established, and you can not modily it. For the sake of automated control, declaring additional notatiens or opening more namespaces is not allowed.
noncomputable section
Some mathematical objects have complex types and need to be declared using the 'structure" or 'inductive' keywords. At this stage, you can declare the types of certain complex mathematical objects for ease of later use.
->>declare mathematiaa system
31

---

Published as a conference paper at ICLR 2026
In Lean 4, declaring mathematical system involves defining structure (must be named as "MySystem' for automatic code check) composed of mathematical objects that may represent either structural spaces (possible value domains) or concrete instances (specific values). The matheratical system consists of several mathematical objects, along with set of constraints that limit their properties or relationships. Follow the below principles when constructing this system:
1. Complete System Deciaration Principle:
For readability, the mathematical system structure must contain all objects mentioned or implied in the problem statement, which enables immediate visual mapping between problem text and formal structure, and help the zeaders to understand.
2. Type Specification Principle:
Declare only the types of mathematical objects at this stage. Detailed definitions and preperty relationships will be established later through constraiat predicates.
3. Solution Object Principle:
There must. exists a special mathematical object that named with the prefix 'sol_', denotes the target property/solution the problem seeks
Analyze the problem determine:
what constitutes a valid sclution
Whether it represents cencrete value or solution space
The appropriate type representation (set/type for spaces, direct type for unique solutions)
4. Clarify Spine Principle
A mathematical object should be formalized as a concrete instance (e.g., Nat) if and only if it is uniquely determined within the problem's s constraints. Otherwise, it must represented as a set or type (e.g., Set Nat) to preserve its possible value space.
5. Exhaustion Principle of Predicate Satisfaction
If it desired for set predicate P, must be ensured that every element set satisfies predicate P, and that there does not exist an element e such that satisfies predicate but e does not belong to set A.
contain all elements that satisfy
-/
/-
The definitions, properties, relationships of declared objects need be specified later by declaring predicate constraints. However, some predicates may be overly complex, so you can define auxiliary functions or predicates at this stage to simplity the subsequent predicate constraints. Predicates defined here cannot serve as antecedents in problensstatement implications. They require encapsulation as constraint predicates the next step before usage.
For the purpose of automated control, parameters of type KySystem cannot be used in this step.
->>declaro
/-
In this step, you need to express the definitions, properties, relationships of mathematical objects in the system by declaring predi The names of these predicates must end with '_constraint" for better readability.
32

---

Published as a conference paper at ICLR 2026
Al1 constraints from the original problem must be reflected in this step, and all constraint predicates declared here must appear problem statement as antecedents in implication expressions.
While maintaining strict logical rigor, prioritize code readability and semantic clarity by avoiding the conflation of multiple constraints within a single restrictive predicate. For the sake of code readability and semantic clarity, a reasonable amount of code redundancy is acceptable. Avoid sacrificing readability in pursuit excessive brevity.
Additionally, the constraint describing the property of the 'sol_' object should be named 'solutioo_coontraiint which is used to constrain the 'sol_" object that it satisfies the requirements of the original problem and becomes the solution to it.
-->acclarc_thhoprrollomsssaa
/-
this step, you need declare special predicate called mroollemsstatemee
which takes the 'solution' variable as a free This predicate applies all constraint predicates to the mathenatical system, thereby completing the declarative expression of the original problem. The format of the 'problem. statement predicate is strictly defined: for any mathematical system, the following implication holds, where the antecedent is the logical AND of all constraint predicates, and the consequence is 'solution sol_object'.
input
The semantics "problem_statement statement are as follows: the proposition is true if and only if the value of 'solution" is the solution to the original problem.
end
# Examples
1.3
THE PROMPT USED FOR BACK TRANSLATION (PER CONSTRIANTS)
## Requirement Translate Lean4 to natural language
attempting to formalize certain mathematical problen. To achieve this formalization, model the mathematical problem as a several mathematical objects and a
mathematical system consisting series of constraints on the system. The following Leand code representa one of the complete formalized constraints for the mathematical problem. Additionally, MySystem describes the mathematical system, while the rest of the code serves as auxiliary. Please analyze the senantics of this constraint and express it in natural language.Pay attention the use of quantifiers and the domain of variables.
Any mathematical problem can be viewed as the study of the properties of a certain mathematical system. A mathematical system consists of several mathematical objects, along with a series of constraints that limit the properties relationships of these mathematical objects, thereby defining the mathematical system under study. The requirement of & mathenatical problem is to investigate a certain property of this mathenatical system. Therefore, a mathematical problem be forma'l expressed declarime mathematical cal system composed of several nathematical objects and series constraints.
33

---

Published as a conference paper at ICLR 2026
Note:
There is some distinctions between certain Lean4 data structures, for example, between List and set, where a List may contain duplicate elements, while a Set enforces uniqueness, reflect the feature of the data structure used.
Note: Your task is solely describe the semantic meaning the constraint's Leand code, do not make any calculations or derivations. Focus exclusively on providing a precise mathematical characterization of the system formalized in this code. Do not make any assumptions about the zeal-world problem it might represent. must carefully translate the logical structure of Leand code, especially when it involves universal quantifeers or existential quantifiers.
Note:
Note: The naming of objects is merely an identifier and should not be used reference for semantic meaning.
Note: Describing Lean4 code in natural language may introduce ambiquity, so try your best to avold ambiguity.
Noto: If any auxiliary functions are used in the Lean4 code of constraint, describe their semantic meaning integrated naturally with the constraint, rather than referring
them by name.
Note: In your analysis and summary, you must reflect the below two (Clarity principles (Ciaityl Point-Space Principle and Exhaustion Principle of Predicate Satisfaction).
## Formalization Principle
Clarify Point-Space Principle
A mathematical object should be formalized as a concrete instance (e.g., Nat) if and only if it is uniquely determined within the problem's constraints. Otherwise, it must be represented set or type (e.g., Set Nat) to preserve its possible value space.
Exhaustion Principle of Predicate Satisfaction
If it is desired for set to contain all elements that satisfy predicate P, must be ensured that every element set satisfies predicate P, and that there does not exist an element e such that satisfies es predicate P but e does not belong to set A.
@magic__mehoo_oo__nt
## Your response should strictly follow the template below.
### **Analysis of '<constraint name>*** <Your analysis of the constraint, must reflect the above two principles>
#HF Concise Summary of ><constraint name> 'markdown
<Here is clear and natural language summary of the constraint's meaning that incorporates the semantics of any auxiliary functions. Emphasize adherence the above principles, especially in cases where they may have been overlooked,>
# Lean4 code you need to translate
LLean
code>>
111
1.4 THE PROMPT USED FOR CONSISTENCY LEVEL DETERMINATION
Requirement: The Lean4 code is formalization of
problem_originee (intendedly transformed into verification task by introducing "[sol_obj] ; since there is concept such 'solve' in
34

---

Published as a conference paper at ICLR 2026
Lean4), , but it may have some issues in the formalization procedure. have observed some semantic discrepancies between the Lean4 code and the problem_original but I can not be sure wether these discrepencies is severe enough to break the semantic consistency, Please analyse every discrepancy listed and determine the consistency level of the Lean4 code, by the final criterion and definitions consistency level. Your analyse must be concise but accurate.
**Consistency Criteria
The liean 4 code is deemed .onnsis with the original problem if and only if it exdoes not violate** any of the following *vViolation Criteria....
### ** Violation Criteria
(If any of these e*Violation Criterion 1: Object Omissien**
true, the code is wrinconssstentxx]
Not all mathematical objects in 'problem_original" are reflected in the Lean4 code or their types mismatch (except for M(sol_obj)' the type of "(so__obj)'
be different but must be equivalent). As long the objects are correctly reflected, code are acceptable.
redundancy in the Lean4
viVolatioon Criterion 2: Semantic Alteration
The definitions, properties, are not exactly preserved the Lean4 code. * (Note: Some redundancy is permitted as long as the core semantics are constrained correctly.)
relationships of any mathematical object
from 'problem originai 'problem_originaa_'
Violation Criterion Constraint Incompleteness
The constraints expressed problem_ formal fail to comprehensively represent all explicit and implicit constraints present in problen_originel. (Note: Full completeness is essential, both explicitly stated and implicitly inferred constraints must be accurately formalized.)
*VViolttion Criterion 4: per-Simplification
The leea4 code conducts concrete computation derivation that simplifien the original problem, leading to semantic inconsistency.
### Exceptions Criteria**
+ Exception Criterion 1: Formatting Flexibility=
There is need to strictly adhere to the original problem's formatting requirements for the solution, Lean4 does not support extensive formatting options (such as requiring decimal numbers, stc.).
### **Final Criterion
Your determination should fecus the discrepancies listed, other aspects are irrelevant.
The Lean 4 code is **consistent** with the original problen. ++if and only it*+: All the discrepancies listed are acceptable under the above criteria.
long as the core properties and relationships
essential
objects are preserved, some redundancy or unnecessary complexity in the Lean4 code is acceptable.
## Formalization Principle for reference:
Clarify Pcint-Space Principle
A mathematical object should be formalized as a concrete instance (c.g., a: Nat) if and only if it can be uniquely determined within the problen's constraints. otherwise, it must be represented
type (e.g., Set Nat) to preserve its possible value space.
Exhaustion Principle of Predicate Satisfaction
35

---

Published as a conference paper at ICLR 2026
If it is desired for set to contain all elements that satisfy predicate P, must ensured that every element satisfies predicate P, and that there does not exist an element e such that satisfies predicate but e does not bolong to set A.
# Mandatory Leand Template:
'Lean4
=>xclare_envirrmmnt
<ome envircment>
->>>deciare aat_lare_axxiliary__aaa
<some auxiliary types>
--
3>xécclare_mathematica____
st sucture MySysten where
<objects>
furettionoccioosss or prediicatsess
<some auxiliary definitions, without any parameter be of type My5ystem>
-=>ddclarc_constrannee
def <nwme>_ccnssteeeeteeeeeee (sys:MySystem) Prop
<expr_bedy>
def <name> baame>_constrantt (sys:MySystem) Prop :-
cexpr_body>
def
(sys:MySystem) : Prop
<expr boxpr_body>
-->>declare the problem statement
def problem_statemeee (solution : <type>) Prop :
y sys:MySystem, <name>_constraint sys
<name> coonstinnntt sys
solution colution_constraine constraint sys
<expression of solution and scl_object>
end
##
@original_probles
lean4 Code Judge:
1Lenn @Lean4_codk
Fotential Sementic Discrepancies: seteential_semetteeeiieeeeeee
## Consistency level:
There three levels of consistency you can choose.
level_1: Fully consistent py the final criterion.
level_2: Consistent without loss of generality: The Leand code formalizes the problen analyzing representative cases. In each of these cases, the final. criterion are fully satisfied, and the general case follows through straightforward deduction.on the formalization rely on equivalent conversions, such as transforming canonical equations into general form. In such cases, the formulation can be regarded as consistent without loss of generality. level_3: Inconsistent, any critericn breaked
lead to this.
Note: Your reasons and recommendations should avoid including any specific calculations or derivations, as this may lead to inconsistency.
Note: Avoid tediously long analysis.
## Your response should be like:
## Analyse of all the listed discrepancies:
36

---

Published as a conference paper at ICLR 2026
<Analyse the discrepancies by examining the Leand code and original problem determine wether severe engough to impair the semantic consistency, Make sure every discrepancy listed is analysed in detail.>
### Analyse of each consistency level:
<According to the definitions of consistency level and your above analyse about the discrepancies listed, determine which consistency Level is appropriate. Your determination should focus on the discrepancies listed, other aspects are irrelevant.>
#+ Consistency Level Determination 'jjson
"consistency levell "<level_1 level_2 level_3>",
"discrepancies" ["<According te your previous analysis, list all the scmantic discrepancics here. If consistency_lovar is 'levol_1', leave this filed blank.Plcase provide some detailed doscriptions of the discrepancies, ensuring it is concrete rather than high-level. Exclude di discrepancies related unnecessary abstractions, complexity, or redundancy, as that not really matter.>"), recoomendat los" inns"
["<Some specific recommendations to rectify the Lean4 code instead of higa-leved recommendations such rectify whicn declaration into what. Your recomentation Formalization Basement and Mandatory Lean4 Template. The recommendations must directly correspond to the discrepancies. If consistency_level is 'eevel_l', leave this filed blank.>")
align with the
1.5
THE PROMPT USED FOR RECTIRICATION
Requiren rement: There appears to be a discrepancy between your Lean4 formalization and the original problem, due to the following reasons, and
to rectity the Lean4 code provided, Please rectify the Leand code accordingly. Print the rectified Leand code di rectly according to the error information. Do not make further thinking.
recommendation
Note: All suggestions are indicative, not mandatory. Rectify the Lean4
code based on your understanding.
Note: Your rectification must meet all the formalization principles mentioned above.
Noto: Your formalization must adopt this treatment: the solution to the free variable in the proposition such that #sproblen_etatcment and only the *ssolutions* is indeed valid solution to the original problem.
original problem is taken
garrollo__statemente
holds true
The determination consistency follows the criteria below. ## +*Consistency Criteria
The Lean 4 code is deemed *connistent*** with the original problem if and only if it **does not violate** any of the following **Violation Criteria.x
VFF Viclation Criteria
(If any of these are true, the code is *inconsssttent...) AiViolation Criterion 1: Object Onissiona*
Not all mathematical objects in maabblem_original are reflected in the Lean4 code or their types mismatch (except for \(sol_obj) the type ([so__bbj)' can different but must be equivalent). long as the objects are correctly reflected, some redundancy in the Lean4 code are acceptable.
*vViolation Criterion Semantic Alteration**
37

---

Published as a conference paper at ICLR 2026
The definitions, properties, relationships of any mathematical object from "problem_original" are not exactly preserved the Lean4 code. (Note: some redundancy is permitted as long as the core semantics are constrained correctly.)
**Violation Criterion Constraint Incompleteness**
The constraints expressed repzesent all explicit and implicit constraints present in sroblem_original (Note: Full completeness is essential both explicitly stated and implicitly inferred constraints must be accurately formalized.)
problem_formal fail to comprehensively
vVoolation Criterion 4: Over-Simplification
The Lean4 code conducts concrete computation derivation that simplifies the original problem, leading to semantic inconsistency,
#+# Exceptions Criteria=e
EException Criterion 1: Formatting Flexibility*.
There is need to strictly adhere to the original problem's formatting requirements for the solution, Leand does support extensive formatting options (such as requiring decimal numbers, etc.).
### **Final Criterion
Your cetermination should focus the discrepancies listed, other aspects are irrelevant.
The Lean 4 code is +*consistent** with the original problem **ff and only if*:: All the discrepancies listed are acceptable under the above criteria.
As long as the objects are preserved, some redundancy or unnecessary complexity the Leand code is acceptable.
properties and relationships of the essential
Reflect the Clarify Point-Space Principle and the Exhaustion Principle Predicate Satisfaction in your analysis. For some cases, violation of these princip plep may lead to severe semantic inconsistencies
Clarify Peint-Space Principle
A mathematical object should be formalized as a concrete instance (e.g., a Nat) if and only if can be uniquely determined within the problem's s constraints. Otherwise, it must be represented as set type (e.g., Set Nat) preserve its possible value space.
Exhaustion Principle of Predicate satisfaction
If it is desired for set A to contain all elements that satisfy predicate P, it must be ensured that every element in set A satisfies predicate P, and that there does exist an element such that satisfies predicate but e does not belong to set A.
Final criterion:
The lean 4 code is consistens with the original problem if and only if, for any concrete instance of MySystem satisfying the constraints, the three basic criteria are satisfied. As long as the properties or relationships of those essential objects are not compromised, some redundancy unnecessary complexity in the Lean4 code is acceptable long the above three criteria fully satisfied.
# Reasons:
ercasons
Recomendations:
grecommendation
é recommendations
38

---

Published as a conference paper at ICLR 2026
# Your response should strictly follow the following template:
Leean
import Mathlib
-->>declare aatarreeevirmeeeeeeeeeee
open Real InnerProduattGeometryy Matrix Topology Filter ENNReal Polynomial Classical Complex
notation "K""n EaclideanSpace R (Fin n) notation "M [" ", "1 -> Matrix (Fin m) (Pin n)
notation "{(" x ", "))" -> @inner R R x
variable (V. Type] [NormeckddComGGroup V] [Imerrrodductspace R VJ
/-
The foundational environment has been established, and you can not modify it. For the sake of automated control, declaring additional notations opening more namespaces is not allowed.
The purpose of this formalization project is for educational purposes, so we strive to minimize reliance on implementations from the Mathlib library. Apart from 'import Mathlib', no additional imports should be included.
-/
noncomputable section
-->
<some auxiliary types>
-->>declare aaaiecaarr_maahhmatiaaaall mathematical_syeeeeee
structure MySystem where
<objects>
<some auxiliary definitions, without any parameter be of type MySystem>
-=>delarr_ccnstrrantt
def <name>_constraint (sys:MySystem) Prop :-
<expr_bedy>
def <name> conttrsannntttnnttttmm (sys:MySystem) Prop
<expr_body>
def cttautiiinnonssaaintttt.. (sys:MySystem) : Prop :=
boxpr_body>>>
-->>declare_the the wwtplppooosaapeeeeeeeeelleeeeeee statement
def problem_statement (solution <type>) Prop
sys:KySystem, <name>_constranl sys A <name> connsts_nntttinttttt sys A soluticn_constraiee sys <expression of solution and scl_object>
end
I.6 THE PROMPT USED FOR SC- CC-BASELINE
You will receive a natural language math problem statement, along
its formal statement
in LEAN 4 and, in some cases, description of mathematical terms.
Please evaluate whether
the formal LEAN statement appropriately translates the natural language statement based on the following criteria. They are considered different if any of the criteria are not satisfied.
1. Key Elements: The fundamental mathematical components, including variables,
39

---

Published as a conference paper at ICLR 2026
constants, operations, domain, and codomain correctly represented in LEAN code.
2. Mathematical Accuracy; The mathematical relationships and expressions should be
interpreted consistently during translation.
3. Structural Fidelity: The translation aligns closely with the original problem, maintaining
its structure and purpose.
4. Comprehensiveness: All conditicns, constraints, and objectives stated in the natural
language statement are mathematically included in the LEAN translation.
when doing evaluation, break down each problem statement into components, match the components, and evaluate their equivalence.
Think step-by-step and explain all of your reasonings.
Natural language math problem statement: (original_problem/
Formal statement in LEAN (Lean4_code)
Your answer should be like: <some analyase here
Judgement and recomendatton: ''json
{f
"consistent_or_not" <yee no>", "reascns" "<if inconsistent, leave your here>", "recommendations" "<if incensistent, leave your recommendations here>"
1)
1.7 THE PROMPT USED FOR SC-BASELINE-BE -T
You will receive a natural language math problem statement, along with
its formal statement
in LEAN and, in some cases, description of mathematical terms.
Please evaluate whether
the formal LEAN statement appropriately translates the natural language statement based on the following criteria. They are censidered different if any of the criteria are not satisfled.
1. Key Elements:
fundamental mathematical components, including constants, operations, domain, and codomain are correctly represented in LEAN code.
variables,
2. Mathematical Accuracy: The mathematical relationsnips and expressions should be
interpreted consistently during translation.
3. structural Fidelity: The translation aligns closely with the original problem, maintaining
its structure and purpose.
4. Comprehensiveneee in the natural
All conditicns, constraints, and objectives stated
language statement are mathematically included in the LEAN translation. When doing evaluation, break down each problem statement into components, match the components, and evaluate their equivalence. Think step-by-step and explain all of your reasonings. Your answer should be in the following format: rhought: [Your Answer]
40

---

Published as a conference paper at ICLR 2026
Judgement:
(Your Answer, Appropriate, Inappropriate]
Natural language math problem statement: [original_problem]
Formal statement in LEAN (Lean4_code)
Natural Language description of LEAN 4: /
1.8 THE PROMPT USED FOR FORMAL- BASSLIN
Please translate the following mathematical problem into Leand by completing the template provided. not try to solve the problem, your task is formalization. Do not make any derivation or comutation as that would be inconsistent with the original problem. Enclose your Leand code in ""Leand section.
Problem:
(problem)
Lean4 tamplate to complete: 1Lean
import Mathlib
open Real InnerProduuttGeomeety Matrix Topology Filter ENNRes1 Polynomial Classical Complex
notation "R""n => EaclideanSpace R (Fin n)
notation "M [" "," m: => Matrix (Fin m) (Fin n) R
notation "((" y ")}" @inner R R__xp x
variable (V Type] [NormedhddCommGrouy V] [InerProoductppac R V]
noncomputable section theorem <name> <parameters> (sclution:<typ) of solution>) ; <conclusion> :- by sorry
end
Examples:
1.9 THE PROMPT USED FOR FORMAL-ITERATIVE BASELINE(SEMANTI E RECTIHICATION)
Your Lean4 code is not consistent with the original problem for the following reasons, try rectify your Lean4 code according to the reasons and recommendations.
## Reasons: (reasons)
## Recommendations:
(tecommendation]]
lean4 tamplate ate completer
41

---

end Published as a conference paper at ICLR 2026
LLean import Mathlib
open Real InnorProductGcometry Matrix Topology Filter ENNReal Polynomial Classical Complex
notation "R""n "n BaclideanSpace (Fin n) notation "M [" n
notation "((" "," nin => Matrix (Fin m) (Fin n) "))" => @inner R --
noncomputable section theorem <name> <parameters> (sclution:<type of solution>) <conclusion> := by sorry
I,10 THE PROMPT USED FOR SIAMALLTTTRAAIVE-BSELLLNNYYYNN RECTIFICATION)
Requirement:
There appears be some errors in your Leand code.
Please rectify the Lean4 code accordingly.
Note: You only need to correct syntax errors, do not change semantic, otherwise the Lean4 code will inconsistent with the original problem.
declaration's name, parameters, type,
Note:Try to implement the same logic using simpler syntax by yourself, rather than relying on Lean4 or Mathlib's built-in special features, to reduce the possibility of syntax errors compilation errors.
## Errors: @err_msg_str
response follow fel following template ate:
"hean
import Mathlib
open Real InnerProduuttGeemeerry Matrix Topology Filter ENNRea1 Polynomial Classical Complex
notation "R""n EuelideanSpace R (Fin n) notation "M [" ", " => Matrix (Fin m) (Fin ")"" Ginner R R_- x
notation "(("
noncomputable section
theorem <name> <parameters> (sclution:<tys solution>) : <conelusion> :- by sorry
end
42


Reviews:
[{"review_id": "hCHKc73ab9", "reviewer": "Reviewer_8Wwq", "summary": "This paper proposes a pipeline, Loc-Decomp, for autoformalization of math problems. It consists of four components. FormalTrans introduces the use of a structured formalization template, to decompose the statement into parts such as functions, types, constraints, and the problem statement. BackTrans translates the formal statement back into natural language. ASCC-R and CpC-R use a divide-and-conquer “LLM-as-a-judge” approach to verify semantic alignment and syntactic correctness, respectively, and leverage error feedback to iteratively improve accuracy. The method seems to achieve strong results on subsets of MATH-500 and miniF2F, namely MATH-Level5-50 and MATH-ASCC-Eval-150.", "questions": "1. For miniF2F there is ground-truth formalization available. Given a dataset with ground-truth formal statements, BEq can evaluate formal-statement equivalence and reduce the need for manual annotation. Please explain the rationale for preferring LLM-as-a-judge over BEq in this setting.\n\n2. In the example in Figure 2, the auxiliary functions and constraints introduced appear to duplicate existing definitions in the standard math library (mathlib)—for instance, continuity is already defined in mathlib. Could this duplication create unnecessary obstacles for downstream automated theorem proving? Is this duplication an intentional design choice or a potential problem? How does LoC_Decomp avoid or mitigate such issues in practical formalization workflows?\n\n3. Line 203 states that instead of using the traditional automated theorem proving placeholder “sorry” as a solution placeholder, this work uses an input 's', a free variable representing the solution. This is not a standard practice and might harm the usefulness of the resulting autoformalization dataset for automated theorem proving. Can the authors provide further justification for avoiding “sorry” as the placeholder?", "limitations": "", "rating": 2, "confidence": 4, "soundness": 2, "presentation": 1, "contribution": 1, "strengths": "1. The proposed FormalTrans converts autoformalization into a structured template. Using free variables as answer placeholders (instead of the more conventional “sorry” placeholders) is a novel idea.\n\n2. Figure 5 shows that ASCC’s divide-and-conquer plus majority-vote strategy for semantic alignment checking is effective and produces judgments that align better with human evaluation.\n\n3. The paper’s figures present the pipeline clearly.", "weaknesses": "1. Lack of novelty. Much of the paper repeats prior work and reads more like an engineering integration than a substantive methodological advance; the novelty is therefore marginal. In particular, the idea of semantic consistency checking by decomposing the formalization code has been previously explored [1], and iterative feedback-based methods for semantic and syntactic correction have been investigated in prior work [2] and [3]. Using back-translation plus an “LLM-as-a-judge” for semantic checks is also a standard practice in this area [4]. The authors should provide explicit comparisons to demonstrate what is new in this paper.\n\n   \n\n2. Questionable evaluation methodology. The two baselines in Table 1 (SymEQ and Lean-workbook) use different datasets and evaluation criteria; reporting their absolute scores side-by-side with the proposed method is misleading and does not support a fair comparison of method superiority. Besides, miniF2F is primarily used as a benchmark for automated theorem proving rather than autoformalization. Using miniF2F for formalization evaluation is not a common practice and should be justified.\n\n\n\n3. Limited and potentially biased MATH-ASCC-Eval-150. The MATH-ASCC-Eval-150 split is very small, relies heavily on manual annotation, and depends on a single formalization model (DeepSeek V3). As a result, the evaluation of semantic-alignment judgment ability is limited: it is unclear whether the reported ability would generalize to formalizations produced by other models. The authors should provide variants of MATH-ASCC-Eval-150 derived by different formalization models or present an analysis of generalization across models; otherwise the practical value of this dataset is questionable.\n\n  \n\n4. Writing quality and presentation issues. Overall the manuscript would benefit from careful proofreading and stricter editing for consistent terminology and formatting.\n\n  - The manuscript uses many nonstandard abbreviations and inconsistent spellings, which make it difficult to follow and reduce readability.\n\n  - The term “autoformalization” appears with multiple spellings (“automated formalization” on Line 013, “auto formalization” on Line 108, “auto-formalization” on Line 117, “autoformalization” on Line 051). These inconsistencies are embarrassing and should be standardized.\n\n  - The paper mostly uses “Lean4,” but “Lean 4” appears on Line 219; the usage should be consistent.\n\n  - Typographical/spacing issues: missing space after commas on Line 062; missing space after periods on Line 110 and Line 351.\n\n[1] Zhang, J., Zhong, C., Xu, H., Li, Q., & Zhou, Y. (2025). *KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment* (No. arXiv:2507.08665). arXiv. https://doi.org/10.48550/arXiv.2507.08665\n\n[2] Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., Lu, J., Saxcé, H. de, Bailey, B., Song, C., Xiao, C., Zhang, D., Zhang, E., Pu, F., Zhu, H., … Li, J. (2025). *Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning* (No. arXiv:2504.11354). arXiv. https://doi.org/10.48550/arXiv.2504.11354\n\n[3] Liu, C., Shen, J., Xin, H., Liu, Z., Yuan, Y., Wang, H., Ju, W., Zheng, C., Yin, Y., Li, L., Zhang, M., & Liu, Q. (2023). *FIMO: A Challenge Formal Dataset for Automated Theorem Proving* (No. arXiv:2309.04295). arXiv. https://doi.org/10.48550/arXiv.2309.04295\n\n[4] Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., & Chen, K. (2024). *Lean Workbook: A large-scale Lean problem set formalized from natural language math problems* (No. arXiv:2406.03847). arXiv. https://doi.org/10.48550/arXiv.2406.03847", "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": "GHzN41Jw6S", "reviewer": "Reviewer_DZ3h", "summary": "This paper introduces LoC-DeCOMP, a framework for automated formalization of mathematical statements using off-the-shelf LLMs. The approach integrates a structured decomposition template for Lean4 code generation, a semantic self-checking mechanism (ASCC) leveraging divide-conquer-merge back-translation, and an iterative feedback-driven refinement loop employing both semantic and syntactic (compiler) error signals. Experimental evaluation on the MATH-500 and miniF2F datasets demonstrates substantial improvements over baseline and prior state-of-the-art methods. Furthermore, experiments on the human-verified MATH-Level5-50 subset show a notable 30 percentage point improvement over the baseline.", "questions": "1.\tCould you please elaborate on the extent to which the proposed template may limit the expressive capability of Lean4? A theoretical discussion on this trade-off, perhaps analyzing constructs that are difficult or impossible to represent, would greatly strengthen the paper.\n2.\tIf a theoretical analysis (Question 1) is difficult, could you provide some empirical evidence demonstrating the framework's applicability to mathematical domains beyond high school-level problems? \n3.\tWould it be possible to include an experimental comparison with a system specifically designed or fine-tuned for formal theorem proving? This would help benchmark the performance of your training-free workflow against alternative approaches.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1.\tClarity and Presentation: The paper is exceptionally well-written and easy to follow. The proposed method, LoC-DeCOMP, and its evaluation are described with great clarity, which significantly aids in understanding the contribution.\n2.\tAccessibility and Ease of Use: A key strength of this work is that it proposes a training-free workflow. By designing a system that effectively orchestrates off-the-shelf LLMs, the framework is highly accessible and can be readily implemented without the need for costly model fine-tuning.\n3.\tDemonstrated Effectiveness: The method shows significant empirical success. The 30 percentage point improvement over the baseline on the human-verified MATH-Level5-50 dataset is impressive and underscores the practical utility and effectiveness of the proposed workflow.", "weaknesses": "1.\tPotential Loss of Expressive Capabilities: The framework's reliance on a predefined template for formalization, as mentioned in Appendix A.4, is a central concern. This template-based approach may inherently restrict the expressive power of the Lean4 language. The paper currently lacks a thorough analysis of this trade-off. Specifically, there is no justification or evidence to suggest that the template is sufficient for formalizing mathematics beyond the scope of high-school-level problems. If the template's expressiveness is severely limited, it could significantly impact the generalizability and overall contribution of the proposed method.\n2.\tNarrow Scope of Evaluation: The empirical evaluation is confined to the MATH and miniF2F datasets, both of which primarily consist of high-school-level mathematics. The paper would be much stronger with experiments on more advanced or diverse mathematical domains (e.g., undergraduate-level abstract algebra or analysis). This weakness is particularly concerning when considered alongside the potential loss of expressiveness (Weakness 1). Without empirical evidence of its applicability to more complex mathematics, it is difficult to assess the method's general utility.\n3.\tMissing Comparison with Specialized Systems: The paper compares its framework against general-purpose LLMs but does not include comparisons with models or systems specifically designed or fine-tuned for formalization tasks. While the primary contribution is the workflow itself, which is well-demonstrated by comparing it against base LLMs, including a baseline from a specialized formalizer would provide a more complete picture of its performance.", "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": "SgXD3tSfYT", "reviewer": "Reviewer_2crV", "summary": "This paper introduces **Loc-Decomp**, a framework that improves automated formalization—the process of converting natural language math statements into formal, machine-verifiable code. It combines a **structured Lean4 template**, a **semantic consistency checker**, and an **iterative feedback loop** that jointly refine both meaning and syntax. Unlike previous methods, Loc-Decomp detects subtle semantic mismatches and uses compiler errors to iteratively correct them. Experiments on MATH and miniF2F datasets show major improvements, achieving up to **90% formalization accuracy**, far surpassing previous state-of-the-art methods.", "questions": "Please Refer to Weaknesses", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- A **divide–conquer–merge–based semantic self-checking mechanism** is proposed to detect subtle inconsistencies between the formalization and the original statement, which aligns well with the motivation behind **Retrieval-Augmented Generation**.  \n- For the first time, it combines semantic inconsistency feedback with compiler error information to perform iterative refinement.  \n- The method is **simple and easy to understand**.", "weaknesses": "- The experiments are too limited; please provide **comparative experiments on the ProofNet and Putnam datasets**.  \n- Please provide a **detailed ablation study** of **Logical Concept Decomposition** and **Iterative Feedback Correction**, explicitly isolating and analyzing their individual effects.", "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)