ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
Authors: Guoxin Chen
Wu Jing
Xinjie Chen
Xin Zhao
Ruihua Song
Chengxi Li
Kai Fan
Dayiheng Liu
Minpeng Liao
Venue: ICLR 2026 Poster (2026)
Keywords: Autoformalization
Automated Theorem Proving
Primary area: unsupervised, self-supervised, semi-supervised, and supervised representation learning

Abstract: Autoformalization, which translates natural language mathematics into machine-verifiable formal statements, is critical for using formal mathematical reasoning to solve math problems stated in natural language. While Large Language Models can generate syntactically correct formal statements, they often fail to preserve the original problem's semantic intent. This limitation arises from the LLM approaches' treating autoformalization as a simplistic translation task which lacks mechanisms for self-reflection and iterative refinement that human experts naturally employ. To address these issues, we propose ReForm, a Reflective Autoformalization method that tightly integrates semantic consistency evaluation into the autoformalization process. This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors through progressive refinement. To effectively train this reflective model, we introduce Prospective Bounded Sequence Optimization (PBSO), which employs different rewards at different sequence positions to ensure that the model develops both accurate autoformalization and correct semantic validations, preventing superficial critiques that would undermine the purpose of reflection. Extensive experiments across four autoformalization benchmarks demonstrate that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines. To further ensure evaluation reliability, we introduce ConsistencyCheck, a benchmark of 859 expert-annotated items that not only validates LLMs as judges but also reveals that autoformalization is inherently difficult: even human experts produce semantic errors in up to 38.5\% of cases.

Published as a conference paper at ICLR 2026
REFORM: REFLECTIVE AUTOFORMALIZATION WITH PROSPECTIVE BOUNDED SEQUENCE OPTIMIZATION
Guoxin Chen Jing Wu? Xinjie Chen Wayne Xin Zhao 1441, Ruihua Song Chengxi Li', Kai Fan", Dayiheng Liu?, Minpeng Li
"Gaoling School of Artificial Intelligence, Renmin University of China
Tongyi Lab, Alibaba Group, 3Zeejiang University
Beijing Key Laboratory of Research on Large Models and Intelligent Governance {gx. chen. batmanflyJ@gmaii com, songru wwwuuuhhabbba caoaaaallloououu look. com
cherxinjie, exj, minpeng. hatp::almm@aaaaaaaii saaallbbbaiinne ceaaainnc.ae com
Model
Benchmark
O Code
ABSTRACT
Autoformalization, which translates natural language mathematics into machine- verifiable formal statements, is critical for using formal mathematical reasoning to solve math problems stated in natural language. While Large Language Models generate syntactically correct formal statements, they often fail preserve the original problem's 's semantic intent. This limitation arises from the LLM ap- proaches' treating autoformalization mechanisms for self-reflection and iterative refinement that human experts natu- rally employ. To address these issues, propose ReForm, Reflective Autofor- malization method that tightly integrates semantic consistency evaluation into the autoformalization process. This enables the model iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors through progressive refinement. To effectively train this reflective model, we introduce Prospective Bounded Sequence Optimization (PBSO), which employs different rewards at different sequence positions to ensure that the model develops both ac- curate autoformalization and correct semantic validations, preventing superficial critiques that would undermine the purpose of reflection. Extensive experiments across four autoformalization benchmarks demonstrate that ReForm achieves average improvement 22.6 percentage points over the strongest baselines. To further ensure evaluation reliability, introduce ConsistencyCheck, a bench- mark of 859 expert-annotated items that not only validates LLMs as judges but also reveals that autoformalization is inherently difficult: even human experts pro- duce semantic errors in to 38.5% of cases.
simplistic translation task which lacks
ReForm-328
Geodei-V2322
GPT-5
07.7
ReForm-8B
Geodei-V2-8B
Kimina-78
81.1
70.4
65.6
66.7
Performance (%)
60
44.6
45.8
46.7
42.9
23.6
25.1
26.726.7
20
16.7
13.3
Putnam Figure Autoformaliiation performance of REFORM against state-of-the-ee models.
miniF2F
ProofNet
AIME2025
Equal Contribution. 1 Corresponding Authors.

---

Published as a conference paper at ICLR 2026
INTRODUCTION
Recent advances in Formal Mathematical Reasoning have demonstrated remarkable capabilities across a variety of challenging scenarios (Polu & Sutskever 2020; Yang ct al. 2023 Xin ct al.
2024a b InternLM Team 2023 Wu et al. 2024 et al.] 2024 Wu et al. 2025 Ren et al. 2025
2025a] Weng et al., 2025). However, these advances are unevenly distributed across two symbiotic tasks: Automated T Theorem Proving (ATP), the process of finding a proof for given for- mal statement, and Autoformalization, the translation of natural language mathematical problems into formal, vachine-verifiable statements such as those in Lean (De Moura et al.) 2013). This dis- parity establishes autoformalization that poses a great challenge even for human experts (Chen et al. 2025b).
Lin et al.
critical bottleneck: it remains labor-intensive endeavor
While Large Language Models (LLMs) (Hurst et al. 2024; Anthropic 2025 Yang al., 2025 Google 2025) have shown proficiency in generating syntactically well-formed statements that pass Lean compiler verification (syntactic correctness), they often struggle to faithfully capture the mantic intent of the original problem (semantic consistency). Recent studies (Peng et al., 2025) have highlighted the pervasive issue of poor semantic fidelity in the current autoformalization sys- tems. Several concurrent works (Wang et al. 2025a Lin et al.) 20256) have attempted to address this challenge by curating high-quality datasets specifically designed to improve semantic consis- tency while still treating autoformalization as a direct translation task in which models generate for- mal statements in a single forward pass, an approach we term the one-pass generation paradigm. While these data-centric efforts yield notable improvements, we find that models trained under this paradigm still frequently fail on subtle semantic details, such as misinterpreting quantifier scopes, overlooking implicit constraints, incorrectly formalizing edge cases, etc., that fundamentally com- promise the original problem's ' intended meaning. In this work, we argue that the root of this persis- tent limitation lies not only in the data quality, but more fundamentally in the one-pass generation paradigm itself: without any mechanism for self-reflection and correction, models cannot progres- sively identify and resolve their own semantic errors during generation. This stands in stark contrast to how human experts tackle autoformalization. They employ an iterative process of review and re- finement, continuously validating and adjusting their formal statements to ensure semantic fidelity.
Inspired by this, we propose REFORM, a novel Reflective Autoformalization paradigm that em- ulates the human process of iterative review and refinement to enhance semantic consistency. In- stead of treating autoformalization as single-pas pass translation task, REFORM reconceptualizes it as a reflective, iterative process that interweaves autoformalization with semantic self- elf-vvaiiattin. Specifically, REFORM operates through self-correction loop: (1) it first generates a candidate for- mal statement, (2) then critically evaluates whether this formalization faithfully captures the original problem's ' semantics, and (3) iteratively refines the statement based on the identified semantic dis- crepancies. Unlike traditional one-pass approaches that commit to a single translation, this reflective paradigm enables the model to detect and correct its own semantic errors during the generation pro- cess, significantly reducing the risk of meaning distortions.
To prevent superficial or hallucinated critiques in the semantic self-validation. design hetero- geneous reward mechanism that targets two synergistic objectives: achieving correct final formal statements as the primary task (Fusk rewarded at the sequence end) and producing accurate semantic validation critiques as the auxiliary task (Faux rewarded at intermediate steps). However, optimizing such heterogeneous rewards poses a significant challenge for existing reinforcement learning (RL) methods, which typically handle only single terminal reward. We therefore introduce Prospective Bounded Sequence Optimization (PBSO), a novel RL algorithm that enables optimizing multiple reward signals at different sequence positions. The key innovation of PBSO lies in its prospective bounded return, which smoothly integrates these heterogeneous signals by computing a discounted sum of future rewards for each step, while crucially bounding these returns within the reward func- tion's 's range to prevent unbounded accumulation and ensure training stability. This enables effective credit assignment across steps with different reward objectives. That is the validation steps learn to produce accurate critiques that facilitate later corrections, while generation steps benefit from the improved validation signals. By optimizing these complementary objectives within each sequence, the model both develops stronger self-validation capabilities and achieves better nutoformalization performance, with each capability reinforcing the other throughout the training process.
Extensive experiments across four challenging autoformalization benchmarks validate the effective- ness of our REFORM. We achieve an average improvement of 22.6 percentage points over the
2

---

Published as a conference paper at ICLR 2026
strongest baselines. In the choice of evaluation metrics, while recent works predominantly rely LLMs as judges for semantic consistency evaluation in autoformalization (Wang et al. 2025a Lin
et al. 2025b), the reliability of these LLM-basee judges is not sufficiently studied. To rigorously investigate the reliability of frontier L.MMs as evaluation metrics, we construct ConsistencyChedee a benchmark of 859 expert-annotated items test how accurately model determines whether a given formal statement correctly captures the problem's 's intent. Our analysis on ConsistencyCheck reveals three insights: (1) Human Expert Fallibility: 16.4% of miniF2F and 38.5% of ProofNet's human- written formal statements contain semantic errors, demonstrating that autoformalization challenges even human experts. (2) Evaluation Reliability Despite Imperfection: Frontier LLMs make cor- rect determination 85.8% of the time, indicating sufficient reliability as evaluation metric. Cru- cially, REFORM'S 's substantial improvements far exceed the potential evaluation noise, confirming the robustness of our findings. (3) Paasification-Genrratii
Gap: This binary classification task is conceptually simpler than autoformalization task. However, its maximum performance is 85,8%, which helps explain why generating semantically faithful formalizations remains stubbornly diffi- cult. These results confirm the effectiveness of our reflective method in producing more reliable and semantically faithful autoformalization.
In summary, our contributions are as follows:
We propose REFORM, a reflective autoformalization paradigm that reconceptualizes autoformal- ization from one-pass translation to an iterative process interweaving generation with semantic self-validation, enabling progressive error identification and correction.
We introduce Prospective Bounded Sequence Optimization (PBSO) handle different reward signals at different sequence positions through prospective bounded returns that improve both autoformalization and semantic validation.
We construct ConsistencyChecl benchmark rigorously evaluate the reliability of LLM-bassed metrics and the quantify the challenges autoformalization poses.
We demonstrate REFORM's effectiveness across four challenging benchmarks. The model achieves an average improvement of 22.6% while maintaining computational efficiency.
2 RELATED WORKS
Autoformalization. Autoformalization the translation of natural language problems into machine- verifiable formal languages- plays a pivotal role in formal mathematical reasoning (Wu et al. 2023
Jiang et al. 2023 Ying et al. 2024 Xie et al. 2025 He et al., 2025 Zhang et al. 2025 Jiayi et al,,
2025 Yu et al.] 2025b). While early approaches achieved syntactic correctness through increasing
training data (Han et al. 2024| Xin et al. 2024b), recent studies (Peng et al. (025) reveal that these models suffer from pervasive semantic infidelity. Recent concurrent works (Wang et al. 2025a]
Lin et al. 2025b) focus on semantically-enhanee datasets to address this issue, yet they remain constrained by the one-pass generation paradigm without correction mechanisms. In contrast, REFORM interweaves autoformalization with semantic self-validation, allowing the model to pro- gressively identify and correct its own semantic errors during generation.
Reinforcement Learning for LLM Reasoning. Reinforcement Learning (RL) has emerged as a powerful paradigm for enhancing L.M reasoning capabilities (Schulman al. 2017 Shao al.) 2024 Chen et al. [2024a b) Wang et al. 2025b) Yu et al. 2025a Qiao et al. 2025 Chen et al. 2025a).
However, existing methods predominantly rely on terminal-onie rewards. While effective for single- objective tasks, this reward paradigm fails to monitor intermediate validation steps in multi-objective tasks, leading to superficial or hallucinated critiques that undermine the self-correction process. In contrast, our PBSO introduces a prospective bounded return integrate heterogeneous rewards across sequence positions. This enables position-spest specific optimization for both reflective autofor- malization and general sequential decision decision-making tasks with multi-objective requirements.
3 METHODOLOGY
As illustrated in Figure we present REFORM, our reflective autoformalization framework that departs from the prevailing one-pass generation paradigm by introducing an iterative self-correction process for enhanced semantic consistency. In this section, we describe the Reflective Autoformal- ization Paradigm ($3.1) followed by the Prospective Bounded Sequence Optimization (3.2).
3

---

Published as a conference paper at ICLR 2026
One-pass Generation Paradigm:
Reflective Autoformalization Paradigm (Ours):
Question
Autoformation
Semantic Self-validation
Final Statement
Question
Final Statement
X
Self-correction Loop
Prospective bounded return:
Gr
GT++
G clip(ri+1 + Gi-1, Tiin Timsx)
T Bux
T aux
T BIX
T aux
T Task
Statement
Critique
Question
S
C1
S
2
5
C3
ST
C7'
Ans
Ans
Final Statement
G
G2
G2
G
Gr-1
Figure 2: Overview of REFORM. (Top) Unlike traditional one-pass generation, our REFORM recon- ceptualizes it as iterative process that interweaves autoformalization with semantic self-validation. (Bottom) We assign heterogeneous rewards across iterations: auxiliary rewards T'u for critique quality and task reward Tusk for final correctness. Prospective bounded returns G2 computed through clipped backward accumulation enable fine-grained credit assignment for each iteration, preventing the degeneration of self-validation while improving autoformalization performance.
3.1 REFLECTIVE AUTOFORMALIZATION PARADIGM
The core innovation of REFORM lies in reconceptualizing autoformalization as an iterative refine- ment process that interweaves formal statement generation with semantic self-validation. Unlike traditional one-pass approaches, our reflective paradigm establishes self-correction loop where the model progressively refines its output based on its own semantic critiques.
Given a natural language mathematical question Q, REFORM operates through sequence of re- finement iterations. At iteration f, the model maintains the complete history of previous attempts: C,-1)), where S, and C, denote the j-th formal statement and its cor- responding semantic critique. This history enables the model to learn from its previous attempts, avoiding repeated errors and progressively converging toward a semantically faithful formalization. interconnected stages:
H, = { C.),..,, (S,-1,
Each iteration comprises
1. Autoformalization: The model generates new formal statement S, conditioned on the ques- tion Q and history He. For the initial iteration (t = 1), the model performs standard autoformal- ization: S π (Q). For subsequent iterations (1 > 1), the generation leverages insights from previous critiques to address identified semantic issues: S. = (QQ, Hc).
2. Semantic Self- Vali-alliatiin: Given the newly generated statement St, the model produces cri- tique C. (Q, (Q,H4, H4, S.) that assesses the semantic consistency between S, and Q. The critique Ct provides detailed diagnostic feedback, identifying specific semantic discrepancies, enabling targeted improvements in subsequent iterations.
This "Autoformalization Self-validation" loop continues until the critique indicates satisfactory semantic fidelity after which the model produces the final statement.
Unified Generation. While conceptually iterative, our paradigm implemented single contin- uous autoregressive generation. Both autofommalization and self eellvvalittion naturally unfold within the same generation sequence: the model generates S,, which becomes part of the context for gen- erating C,, which in turn informs Se+1- This design ensures that the entire reflective process occurs within a single forward pass, maintaining computational efficiency comparable to the one-pass meth- ods while achieving superior semantic consistency. The model learns to autonomously identify and correct semantic errors during generation, effectively internalizing what would traditionally require multiple model calls and human oversight.
Mutual Reinforcement with Dual Capabilities. The interweaving of autoformalization and self- validation creates virtuous cycle: the autoformalization capability progressively develops semantic awareness by learning from validdatt,,,,nn, while the vali-vatiat capability becomes increasingly adept at identifying subtle errors by observing refinement patterns. This mutual reinforcement stands
4

---

Published as a conference paper at ICLR 2026
in contrast traditional one-pass approaches and is instrumental in enabling REFORM achieve formal statements that are both syntactically valid and semantically faithful.
3.2 PROSPECTIVE BOUNDED SEQUENCE OPTIMIZATION
While the reflective autoformalization paradigm establishes the structural framework for iterative refinement, training models to effectively execute this process presents a unique challenge: how to jointly optimize for both correct final autoformalizations and accurate intermediate selfvvalidations within a single sequence?
The core difficulty lies in the heterogeneous nature of these objectives. High-quality self-validation critiques are essential for guiding refiement, yet they serve as diagnostic tools rather than direct solutions. A model might generate insightful critiques identifying all semantic issues but fail to translate these insights into correct refinements, spite superficial self-validations. This creates an important credit assignment problem: optimizing solely for final task success provides no explicit signal for the critique quality, potentially causing the self validation mechanism to degenerate into trivial or hallucinated assessments.
conversely, produce correct formalizations de-
3.2.1 HETEROGENEOUS REWARD MECHANISM
To address this challenge, we introduce a heterogeneous reward structure that supervises both the primary autoformalization task and the auxiliary self-validation task:
Task Reward for Autoformalization. We assign a positive reward the final formal statement (termed 'Ans' below) only when it achieves both syntactic and semantic correctness:
(Q, Ans) = {
if PassesLeanAAns)) A IsConsistent(Q.
(1)
otherwise
where PassesLean verifies syntactic validity through the Lean compiler, and IsConsisters assesses semantic consistency between "Ans" and the original question Q using an LLM-based judge[] This reward drives the primary learning objective, encouraging the model to produce correct final formalizations.
To prevent degeneration of self-validation, we introduce auxiliary rewards that directly supervise each critique C.:
Auxiliary Rewards for Self- Validation Quality.
f1 {
if Ii Ct)
Tuxx (Q, S₁ S,, C,)
otherwise
where IsFaithfulcritiqus evaluates whether C, accurately diagnoses the semantic relation- ship between the current statement S, and question Q, penalizing false positives, false negatives, and premature termination (incorrectly claiming semantic fidelity when discrepancies remain).
Together, these heterogeneous rewards provide complementary supervision signals. The task reward ensures correct final outputs while auxiliary rewards maintain the integrity of the self-validation mechanism, jointly enabling effective reflective autoformalization.
3.2.2 PROSPECTIVE BOUNDED RETURN
Existing RL methods typically assign rewards only at sequence termination, optimizing solely for task success. In our reflective paradigm, this method would provide little supervision for the quality of intermediate self-validations. Without explicit rewards for self-validation, the model is at risk of learning to generate superficial or hallucinated critiques that appear justify refinements but provide no genuine diagnostic value, thereby undermining the entire reflective mechanism.
To address this problem, we introduce prospective bounded return that maximizes expected cumu- lative reward while ensuring quality at each step. Our approach integrates both task and auxiliary rewards distributed across the trajectory, where each position's 's return G, captures the cumulative value of the remaining sequence from that point forward. This prospective view enables the model
consi stent and LaFai WWrichfulCro i que evaluated by Criti cl.ean-1 48 (Peng et al. 2025 and Qwen3 - A228 Yang 2025) respectively. We provide detailed reliability evaluations in
5

---

Published as a conference paper at ICLR 2026
to learn how current decisions contribute to eventual task success. For trajectory with T itera- tions producing rewards !'m.....,, Faaxx l'usk]: we compute returns for each step through backward accumulation with bounded discounting:
G2 = =clpp (rip + G1+1, Tmin: mmax)
(3)
where 7 E (0, 1] is the discount factor, GT+1 O, and the clipping operation bounds returns within the reward function's 's range [Tmin r'max] to prevent gradient instability from unbounded accumula- tion. Each G, serves as the composite reward signal for the entire (-th ceraation-ecompaasse both the statement generation St and its critique C capttrnnn how this complete reflective step contributes to the trajectory's 's overall success.
3.2.3 SEQUENCE OPTIMIZATION WITH POSITION-SPECIFIC ADVANTAGES
Building on the prospective bounded returns, we now present our complete Prospective Bounded Sequence Optimization (PBSO) algorithm. Unlike existing RL. methods that compute advantages using only terminal task rewards without supervising intermediate steps, PBSO leverages the full se- quence of heterogeneous returns to compute position-specific advantages. This enables fine-grained credit assignment where each iteration receives distinct supervision based on its actual contribution to the trajectory's 's success.
For each question Q, sample N complete trajectories, where trajectory j undergoes T3 itera- tions. The bounded return computation (Eq. 3 yields a sequence of returns {G², GG..... G
capturing the prospective value each iteration. enable policy optimization, we transform these returns into advantages through joint normalization across all sampled trajectories:
G mC) st)
A
where
G UlG! : :t= I,.. T3 +1 j=1
(4)
This produces rrsition-specifie advantage sequences À = [A]. Ag. A.. A/, for each trajectory,
where all tokens within iteration receive advantage A/. These advantages vary across iterations within the same trajectory-cait iterations that successfully identify critical errors may receive higher advantages than later iterations that make minor refinements. We then update the policy using these pesition-specifie advantages with standard GRPO (Shao al. 2024), jointly optimizing both autoformalization accuracy and self-validation quality.
EXPERIMENT
4.1 EXPERIMENTAL SETUP
Datasets. To rigorously assess the effectiveness of REFORM, evaluate four challenging benchmarks: (1) miniF2F (Zheng et al. (021): 244 test problems from high-school mathematics
competitions. (2) ProofNet (Azerbayev et al.] 2023 186 undergraduate-leve theorems from text- books spanning real analysis, abstract algebra, and topology. (3) PutnamBench (Tsoukalas et al.)
:024 644 college-level competition problems from the Putnam Mathematical Competition (1962-
2023). (4) AIME2025 (OpenCompass 2025): 30 problems from the 2025 American Invitational Mathematics Examination, testing autotormalization on contemporary competition problems.
Baselines. We compare our REFORM against the sate-oofthe--re methods including: (1) Propri- etary and Open-source Models: We evaluate frontier LLMs including GPT-5 (OpenAl 2025).
Claude-3.77 3.7--nnetnttt (Anthropic 2025). Gemini-2.55Pro (Google) 2025). DeepSeek-R 1-0528 (Guo
al. 2025), QwQ-32B (Qwen) 2024). and Qwen3 series (Yang et al. 2025). (2) Autoformalization
Models: We compare with state-of-the-an autoformalization models, including Prever
V1.5-RL (Xin et al. 2024b), Goedel-Vi V1 (Lin al. 2025a), Simina-Autoformaliia (aariierrrBBBangggggggg et al.
2025a). and Goedel Formalizer22 (8B and 32B) (Lin al. 2025b).
Evaluation Metrics. We consider two key metrics: (1) Syntactic Correctness (syn): whether the
formal statement passes Lean compiler verification; (2) Semantic Consistency (sem): whether the statement is both syntactically correct and semantically faithful. This is our primary metric. We adopt Qwen3 3-2e33-235.. - our default evaluation model unless explicitly stated otherwise.

---

Published as a conference paper at ICLR 2026
Table 1: Main results. We report both syntactic correctness (syn) and semantic consistency (sem), with sem being our primary metric. 'Improvements are relative to the best baseline with comparable model size. The best results are in bold, and the second best are underlined among baselines.
mi
ProofNet
Putnam
AIME2025
AVG
Model
syn
syn
syn
syn
syn
Proprietary and Open-source Models
5
70.9
66.0
49.5
44.6
61.6
45.8
13.3
13.3
48.8
42.4
Claude-3.7-somne
40.2
34.0
28.5
22.0
20.2
22.2
Gemini-2.5-pra
28.7
25.8
23.1
15.7
6.5
13.3
0.0
20.2
DeepSeek-RI
38.5
35.2
11.3
9.7
19.7
11.3
16.7
3.3
21.6
14.9
Qwen3-235B-A223
35.7
43.9
16.7
12.9
33.1
19.9
20.0
13.3
31,4
22.5
Qwen3-32B
57.4
53.3
10.8
8.1
8.2
6.2
10.0
10.0
21.6
19.4
Qwen3-8B
37.7
31.6
7.5
5.9
4.5
3.1
3.3
0.0
16.6
10.1
Autoformalization Models
DeepSeek-Praver Prover-Vi....
51.5-R
86.1
43.0
36.6
16.1
11.3
8.6
0.0
0.0
30.8
14.8
Goedel-V
95.1
47.1
48.4
18.3
62.1
9.3
70.0
3.3
68.9
19.5
Voccel-V--32B----
93.4
69.3
47.8
26.3
73.1
17.2
80.0
13.3
73.6
31.5
Kimina-Autofore Autoformamlzzz---
92.6
67.6
53.2
23.6
69.7
25.1
80.0
16.7
73.9
33.3
V2-8B
97.5
81.1
70.4
47.3
74.5
42.9
66.7
26.7
77.3
49.5
Goedel- Formalizer V2-32B
97.1
82.0
71.5
50.5
74.2
41.4
66.7
26.7
77.3
50.1
Ours
REFORM-8B
98.4
87.7
78.5
65.6
81.9
57.3
83.3
46.7
85.5
64.3
Improvement
0.9
1 8.1
1 18.3
t 7.4
3.3
1 20.0
f 8.2
1 14.8
REFORM-322B
97.1
91.4
82.3
70.4
83.1
62.3
86.7
66.7
87.3
Improvement
0.0
9.4
1 10.8
1 19.9
1 8.9
20.9
1 6.7
1 40.0
1 10.0
1 22.6
Implementation Details. We implement REFORM based on Qwen3 (8B and 32B) YYang et al., 2025). We curate training data from diverse open sources including Omni-MATH (Gao al. 2024). IneqMath (Jiayi et al., 2025), the Lean Workbook (Ying et al. 2024), DeepTheorem (Zhang et al. 2025), Natural Proofs (Razborov & Rudich, 1994). and Big-Math (Albalak et al. (025), with rig-
orous deduplication against all test sets to ensure fair evaluation. For details, we refer readers to Appendix A.I for dataset statistics, SFT and RL training procedures.
4.2 MAIN RESULTS
Table [ comprehensive evaluation results across four challenging autoformalization bench- marks. Additionally, we provide CriticLean based evaluation results to further validate the robustness of our findings (Appendix 4.6). We have two key findings that validate the effectiveness of the reflective paradigm.
presents
First, our REFORM achieves sate-of-the-d performance with substantial improvements across all benchmarks. REFORM-SB surpasses the strongest baseline of + +1..8pp in semantic consistency while improving syntactic correctness (+8.2pp)). Remarkably, our 8B model even outperforms the 4x larger tic consistency, demonstrating that the reflective paradigm's architectural innovation goes byond mere parameter scaling. The improvements are particularly pronounced on the more challenging benchmarks: +18.3pp on ProofNet and + 14.4pp on PutnamBench compared to Goedel-V2-SB, with the most dramatic gain of +20.0pp AIME2025. These consistent improvements across diverse benchmarks confirm that iterative self-validation fundamentally enhances semantic understanding.
by an average
Maaeell-oolllizee---ee by + +14.2pp seman-
Second, the reflective paradigm specifically addresses the critical semantic issue that plagues exist- ing autoformalization systems. All baseline methods exhibit severe syntactic-semantic perfor- mance gap. revealing that models readily generate Lean-compilable code but systematically fail at semantic fidelity. This gap is most extreme the more difficult datasets (e.g. Putname). In con- trast, REFORM'S improvements are more concentrated semantic consistency than syntactic refinement. This asymmetric improvement pattern amplifies on harder benchmarks, with semantic gains consistently exceeding syntactic improvements by 2-3x, demonstrating that by making seman- tie validation an integral part of generation, REFORM transforms autoformalization from superficial pattern matching genuine mathematical understanding.

---

Published as a conference paper at ICLR 2026
4.3 ABLATION STUDIES
We conduct comprehensive ablation stud- ies to analyze the contribution of each component in our framework, as shown in Table 2 The experiments are divided into two parts: (1) Training Compo- nents. Removing the bounded clipping in Eq. [ causes severe degradation par- ticularly on the harder benchmarks, con- firming that bounding returns is crucial for stable optimization with heterogeneous re- wards. The auxiliary reward Taux exhibits increasing importance as problem com- plexity increases, indicating that explicit supervision for self-validation quality be- comes more critical for harder problems. The RL training phase provides consistent improvements across all datasets, with gains increasing on harder problems, demonstrating that PBSO effectively learns complex reasoning strategies beyond SFT. (2) Paradigm Comparison. The most striking re- sult emerges from comparing our reflective paradigm against one-pass generation: when trained on identical data, the one-pass baseline shows dramatic performance gaps that widen with problem dif- ficulty. This widening gap validates our core hypothesis: mathematical complexity increases, the need for iterative seff-correction becomes paramount. Single-pass generation fundamentally lacks the mechanism to identify and rectify its semantic errors, while reflective paradigm enables progressive refinement through self-validation.
Table 2: Ablation studies training methodology and paradigm with semantic consistency score. All variants use identical training data ensure fair comparison.
Method
miniF2F
ProofNet
Putnam
AIME25
Ablation on training Methodology
REFORM w/o clip
87.7
65.6
$7.3
46.7
84.0
59.6
48.9
26.7
w/o T'ux
87.7
65.6
52.1
40.0
w/o RL
85.2
62.3
49.4
30.0
Ablation Paradigm
Onc-pass 82.7
59.1
40.8
16.7
4.4
TRAINING DYNAMICS OF PBSO
Rewards
Response Length Curve
Accuracy on Putnam
60
Response Length
5k
EMA Smoothed Length
Original Length
Accuracy (sem %))
0.5
Roward
55
4kc
0.4
3k
Original Reward
Avgg3
0.2
2k
45
100
200
300
100
300
100
200
300
400
Step
Stop
Step
Figure 3: Training dynamics of our RL process.
To understand how Prospective Bounded Sequence Optimization enables effective learning of the reflective paradigm, analyze the training dynamics in REFORM-8B across three key dimensions. Figure 3 reveals three critical insights into how PBSO shapes model behavior:
(1) Stable from 0.30 to 0.47 over 400 steps, with progressively narrowing confidence bands indicating stable convergence. This smooth progression demonstrates that PBSO successfully balances heteroge- neous rewards at different sequence positions, optimizing both task success and critique quality. (2) Emergent Reflective Behavior: Response length (middle) exhibits remarkable organic growth from 2,300 to 4,800 tokens during training-a 2. 1 expansion solely from heterogeneous reward signals, without any explicit length bonuses or penalties. This phenomenon reveals crucial insight: when properly incentivized through auxiliary rewards for critique quality, models autonomously develop more thorough self-examination behaviors. (3) Robust Generalization. Performance on held-out PutnamBench (right) improves from 47% to 57% in semantic consistency, closely tracking train- ing rewards. This tight correlation between training and test performance, maintained throughout optimization rather than diverging due to overfitting, demonstrates that PBSO enables learning of transferable reflective capabilities. Together, these dynamics reveal how PBSO orchestrates the RL process: heterogeneous rewards drive the emergence of reflective behavior, which in turn generates richer training signals, further improving both autoformalization and self- validatiin capabilities in a virtuous cycle.
cacoogeennou--bbecctii Optimization. The training reward (left) steadily improves
8

---

Published as a conference paper at ICLR 2026
4.5 RELIABILITY OF SEMANTIC CONSISTENCY EVALUATION
Since our evaluation relies on LLM-based judges to assess semantic consistency, establishing their reliability is crucial for validating our experimental conclusions. We construct ConsistencyCheck, benchmark of 859 expert-annotated items where models perform binary classification: determining whether formal statement correctly preserves the mathematical semantics of the original question.
Human expert fallibility in existing benchmarks. During the annotation process, we uncovered that 16.4% of miniF2F and 38.5% of Proo/Net's numan-writter formal statements contain semantic errors. This high error rate in expert-cras crafted formalizations underscores that autoformalization chal- lenges even human specialists, further motivating the need for automated approaches like REFORM.
Table 3: LLM performance on ConsistencyCheck benchmark for semantic consistency evaluation. Full model names: Claude-3.7-Sonnet, Qwen3-235B A--B--AA2----iiiii
CriticLeann- 14B.
Metries
GPT-5
Gemini-2.5-pro
Claude-3.77
DeepSeck-RI Qwen3-235B'
QwQ
CriticLean
Accuracy
82,5
85,8
77.2
78.1
82.9
77.9
79.1
Precision
88.9
84.4
75.7
84.7
85.3
75.5
80.7
Recall
82.9
96.9
93.3
79.0
87.7
95.4
87.3
F1
85.8
90.2
83.6
81.8
86.5
84.3
83.9
LLM evaluation reliability analysis. 3 that while Gemini-2.5-PP achieves the high- est accuracy (85.8%), open-source Qwen3-235B-A22B provides comparable performance (82.9%) with balanced precision-recall trade-offs. These results reveal two critical insights for the auto- formalization community: (1) Munsification-Generatii Gap validates autoformalization's 's dif- ficulty. On this classification task, which inherently simpler than generation, frontier models plateau at 86% accuracy. This 14% eгrоr rate in merely recognizing semantic consistency helps explain why generating faithful formalizations remains fundamentally challenging. as generation requires not just recognition but creative synthesis under semantic constraints. (2) Current evalua- tion sufficiently reliable for our experiments. Despite imperfections, with an accuracy at 85. 85.8%, current LLMs provide adequate signals for drawing research conclusions. Crucially, REFORM's 's im- provements far exceed potential evaluation noise: our + +14.4pp gain on PutnamBench represents 2.5 2.5-standard-deviiation effect size given the judge's on AIME2025 corresponds to 3.5 standard deviations - both statistically robust. Based on these analyses, we adopt (iwen--2352 A22B as our primary semantic judge (balancing quality with producibility) and CriticIean 14BB for RL training (for efficiency). Finally, ConsistencyCheck released to facilitate future research on autoformalization evaluation reliability.
rate, while +20.0pp improvement
Human Evaluation on REFORM While LLMM-bssed evaluation provides scalable assessment, we further conduct human evaluation to directly validate REFORM'S outputs. We evaluate the final formal statements generated by REFORM-8B on miniF2F and ProofNet test sets. Each statement was classified as "Correct" only it was both syntactically valid and semantically faithful to the original problem; otherwise, it deemed "Incorrect". The human evaluation revealed high fidelity, with 86.1% %% of miniF2F and 69.4% of ProofNet formalizations verified as correct, closely aligning with LLM--baeed semantic consistency scores (87.7% and 65.6% respectively) and validating the reliability of automated evaluation.
4.6 ROBUSTNESS ANALYSIS ON MAIN RESULT EVALUATED BY CRITICLEAN-14B
To validate that our improvements are not artifacts of a specific evaluation metric, Table presents results evaluated by CriticLeen--Me 14B (Peng et al. 2025). an independent semantic consistency judge trained specifically for autoformalization assessment.
(1) Consistent Improvements Across Evaluators. REFORM maintains substantial advantages un- der CriticLean evaluation, with ReForm-8B achieving an average improvement of +18.0pp over Goedel-V22 -2-8B- (compared to + 14.8pp under Qwen3-235B evaluation). This consistency across fun- damentally different evaluators a general-purpose LLM (Qwen3) versus specialized critic model (CriticLLen)-stiee stronglyy validates the robustness of our approach.
(2) Amplified Gains on Challenging Benchmarks. The improvements are even more pronounced under Criticleean evaluation for difficult datasets: +33.3pp AIME2025 (vs +20.0pp with Qwen3)

---

Published as a conference paper at ICLR 2026
Table 4: Main results. We report semantic consistency (sem) based on
14B (Peng
et al. 2025) with sem being our primary metric. $ *Improvements are relative to the best baseline with comparable model size. The best results are in bold, and the second best are underlined.
Model
miniF2F
ProofNet
Putnam
AIME2025
AVG
Proprietary and Open-source Models
GPT-5
66.8
41.5
44.1
13.3
41.7
Claude-3.7 Baude-3.7-Sonnet
34.8
22.6
10.9
0.0
17.1
Gemini-2.5-Pro
28.3
7.0
4.5
0,0
10.0
DeepSeek-RI R105228
33.2
10.2
11.2
3.3
14.5
Qwen3-235B 2-2B-223BBA22BB
44.7
12.4
18.8
23.3
24.8
Qwen3-32B
54.1
7.5
6.7
6.7
18.8
Qwen3-8B
32.0
7.0
3.1
0.0
10.5
Autoformalization Models
DeepSeek-Prover V1.5-RL
44.3
0.0
0.5
0.0
11.2
Boodee-VV-32B-Workkee
48.8
18.3
9.6
3.3
20.0
Goedel-V1-92B-Somee
66.0
23.1
17.4
10.0
29.1
Kinina-Autoformaizzz--11
66.8
22.0
26.2
13.3
32.1
Fordel--ormalizer- V2-8B
86.9
54.8
40.8
26.7
52.3
Goedel-Fone Goedel-Formalizer-rr V2-32B
89.3
59.1
44.3
33.3
56.5
Ours
REFORM-8B
92.2
69.4
59.6
60.0
70.3
Improvement
5.3
1 14.6
18.8
33.3
1 18.0
REFORM-32B
91.4
73.7
64.6
63.3
73.2
Improvement
2.1
14.6
20.3
1 30.0
1 16.7
and +p8.8pp on PutnamBench (vs +14.4pp). This suggests that CriticLean may be more sensitive to semantic nuances in complex problems, where our reflective paradigm provides the greatest benefits.
(3) Different Absolute Scores but Consistent Rankings. While Criticleea generally assigns higher semantic consistency scores than Qwen3 (possibly due different training objectives or calibration), the relative rankings remain largely consistent. Notably, REFORM achieves the highest scores under both evaluators, with ReForm-8B reaching 70.3% average semantic consistency under CriticLean-a remarkable achievement given the inherent difficulty of autoformalization.
These results from Table I and Table 4 confirm that the reflective paradigm's effectiveness tran- scends specific evaluation methodologies, providing robust improvements in semantic consistency regardless of how it is measured.
CONCLUSION
We introduce REFORM, reflective autoformalization paradigm that fundamentally shifts from pass generation to an iterative process interweaving generation with semantic self-validation. To effectively train the reflective paradigm, we propose Prospective Bounded Sequence Optimization, which realizes heterogeneous rewards via prospective bounded returns. This enable models to jointly optimize for both correct final formalizations and accurate intermediate critiques, preventing degen- erate or hallucinated self-validation Extensive experiments demonstrate the effectiveness of our REFORM with an average improvement of 22.6% across four benchmarks. Our Consistency benchmark further reveals that autoformalization challenges even human experts while confirming the reliability of L.--- evaluation metries.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGMENTS
This work was supported by Alibaba Research Intern Program. This paper was partially supported by the National Natural Science Foundation of China No. 92470205 and Beijing Major Science and Technology Project under Contract No. Z251 100008425002.
ETHICS STATEMENT
Our work focuses advancing automated mathematical formalization through novel reflective paradigm and reinforcement learning algorithm. We have carefully considered the ethical implica- tions of our research and taken appropriate measures ensure responsible development.
The construction of our ConsistencyChede benchmark involved human experts mathematics and Lean4. All annotators were fairly compensated for their exper- tise and time according to prevailing standards for skilled technical work. The annotation process was designed to be intellectually engaging rather than repetitive, leveraging the annotators' mathe- matical expertise. We ensured reasonable working conditions with no excessive time pressures, and annotators retained the right to decline or withdraw from tasks at any point.
Human Annotation and Labor.
Intellectual Property and Attribution. Our benchmark builds upon existing mathematical datasets (miniF2F and ProofNet), which we use in accordance with their licenses and with proper attribution. We acknowledge the substantial human effort that went into creating these original resources and ensure all sources are appropriately cited.
Potential Impacts. While our work aims to democratize access to formal mathematical reasoning tools, we acknowledge potential concerns. The automation of mathematical formalization could reduce demand for certain types of mathematical verification work. However, we believe our tech- nology will primarily augment rather than replace human mathematicians, enabling them to focus higher-level creative and conceptual work. Furthermore, by making formal verification more accessible, our work could enhance mathematical education and research, particularly in resource- constrained settings.
REFERENCES
Alon Albalak, Duy Phung. Nathan Lile, Rafael Rafailov, Kanishk Gandhi, Louis Castricato, Anikait Singh, Chase Blagden, Violet Xiang, Dakota Mahan, et al. Big-math: A large-scale, high-quality math dataset for reinforcement learning language models. arXiv preprint arXiv:2502.17335 2025.
Anthropic. Claude 3.7 sonnet and claude code. 3laude-3-7-sonne February 2025.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathemat- ics. arXiv preprint arXiv:2302.12433, 2023. 2023.
Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Alphamath almost zero: Process supervision without process. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024a. URL SttL:ttts////eeeeieieee net wwteee/oorumiiiaaaaaaa33222
Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Step-level value preference optimization for mathematical reasoning. arXiv preprint arXiv:2406. 10858, 2024b.
Guoxin Chen, Zile Qiao, Xuanzhong Chen, Donglei Yu, Haotian Xu, Wayne Xin Zhao, Ruihua Song, Wenbiao Yin, Huifeng Yin, Liwen Zhang, et al. Iterresearch: Rethinking long-horizon agents via markovian state reconstruction. arXiv preprint arXiv:2511.07327 2025a.
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint 2rXiv:2507.237720 2025b.

---

Published as a conference paper at ICLR 2026
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doom, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pp. 378-388. Springer, 2015.
Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, et al. Omni-math: A universal olympiad level mathematic benchmark for large language models. arXiv preprint arXiv:2410007963, 2024.
Google. Gemini 2.5 pro. http://///eeeeeee....oo//o////ea April 2025.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability in llms via reinforcement learning. 2025.
Chuanyang Han, Pu Huang, Yixuan Wang, Yutao Chen, Sheng Zhang, and Li Song. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprini arXiv:2404.1488 14813,,,..1 2024.
Zhiwei He, Tian Liang, Jiahao Xu, Qiuzhi Liu, Xingyu Chen, Yue Wang, Linfeng Song, Dian Yu, Zhenwen Liang, Wenxuan Wang, et al. Deepmath-103k: A large-scale, challenging, de- contaminated, and verifiable mathematical dataset for advancing reasoning. arXiv preprint 1rXiv:2544.11556. 2025.
Aaron Hurst, Adam Lerer, Adam Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Os- trow, Akila Welihinda, Alan Hayes, Alec Radford, Aleksander Madry, Alex Baker- Whitcomb, Alex Beutel, Alex Borzunov, Alex Carney, Alex Chow, Alex Kirillov, Alex Nichol, Alex Paino, Alex Renzin, Alex Tachard Passos, Alexander Kirillov, Alexi Christakis, Alexis Conneau, Ali Ka- mali, Allan Jabri, Allison Moyer, Allison Tam, Amadou Crookes, Amin Tootoonchian, Ananya Kumar, Andrea Vallone, Andrej Karpathy, Andrew Braunstein, Andrew Cann, Andrew Codis- poti, Andrew Galu, Andrew Kondrich, Andrew Tulloch, Andrey Mishchenko, Angela Back, An- gela Jiang, Antoine Pelisse, Antonia Woodford, Anuj Gosalia, Arka Dhar, Ashley Pantuliano, Avi Nayak, Avital Oliver, Barret Zoph, Behrooz Ghorbani, Ben Leimberger, Ben Rossen, Ben Sokolowsky, Ben Wang. Benjamin Zweig, Beth Hoover, Blake Samic, Bob McGrew, Bobby Spero, Bogo Giertler, Bowen Cheng, Brad Lightcap, Brandon Walkin, Brendan Quinn, Brian Guarraci, Brian Hsu, Bright Kellogg, Brydon Eastman, Camillo Lugaresi, Carroll L. Wainwright, Cary Bassin, Cary Hudson, Casey Chu. Chad Nelson, Chak Li, Chan Jun Shern, Chamning Con- ger, Charlotte Barette, Chelsea Voss, Chen Ding. Cheng Lu, Chong Zhang. Chris Beaumont, Chris Hallacy, Chris Koch, Christian Gibson, Christina Kim, Christine Choi, Christine McL eevve, Christopher Hesse, Claudia Fischer, Clemens Winter, Coley Czamecki, Colin Jarvis, Colin Wei, Constantin Koumouzelis, and Dane Sherburn. Gpt-4o system card. CoRR, abs/2410.211776 2024. doi: 104455W/ARXX2224122277.. URL https:://oiii http://................././..../
21276
InternLM Team. Internlm: A multilingual language model with progressively enhanced capabilities. arXiv preprint arXiv:2307.16135, 2023.
Albert Qiaochu Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755 2023.
Sheng Jiayi, Lyu Luna, Jin Jikai, Xia Tony, Gu Alex, Zou James, and Lu Pan. Solving inequality proofs with large language models. arXiv preprint arXiv:2506.07927, 2025.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey deep learning for theorem proving. arXiv preprint 2xxvv2240.00999, 2024.
Yong Lin. Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint 2rXiv:2502.07644 2025a.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel prover-:r: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508. (00::250..0663... 2025b.
12

---

Published as a conference paper at ICLR 2026
OpenAl. Gpt-5 is here. https::/openai.com/
August 2025. 2025.
OpenCompass. AIME 2025 Benchmark.
httes///ogggligffc...//ottttttt
opencompass AAIIMMMMMEE222 2025.
Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang. Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, et al. Criticlean: Critic-guided reinforcement learning for mathematical formalization. arXiv preprint arXiv:2507.0618), 2025.
Stanislas Polu and Πla Sutskever. Generative language modeling for automated theorem proving. In International Conference on Machine Learning, pp. 7872-7882. PMLR, 2020.
Zile Qiao, Guoxin Chen, Xuanzhong Chen, Donglei Yu, Wenbiao Yin, Xinyu Wang, Zhen Zhang, Baixuan Li, Huifeng Yin, Kuan Li, et al. Webresearcher: Unleashing unbounded reasoning capa- bility long-horizon agents. arXiv preprint arXiv:2509.13309 2025.
Qwen. QwQ: Reflect deeply on the boundaries of the unknown. Hugging Face, 2024.
Alexander A Razborov and Steven Rudich. Natural proofs. In Proceedings of the twenty-sixth anmual ACM symposium on Theory of computing, pp. 204-213, 1994.
ZZ Ren. Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang. al. Deepseek-prover-ye Advancing formal mathematical rea- soning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford. and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06344 2017.
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song. Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. 2024.
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37: 11545-1 1569, 2024.
Haiming Wang. Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504. 11354, 2025a.
Weixun Wang, Shaopan Xiong, Gengru Chen, Wei Gao, Sheng Guo, Yancheng He, Ju Huang, Jiaheng Liu, Zhendong Li, Xiaoyang Li, et al. Reinforcement learning optimization for large- scale learning: An efficient and user-friendly scaling library. 2025b.
Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang Aut- oformalization in the era of large language models: A survey. arXiv preprint arXiv:2505.2344 2025.
Yilun Wu, Albert Jiang, Wenda Li, Mateja Jamnik, Guillaume Lample, and M Rabe. Autoformal- ization with large language models. Transactions on Machine Learning Research, 2023.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang. Dahua Lin, and Kai Chen. Intern1m2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:24100 10.55000 2024.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, and Kai Chen. Intern1m2. 5-stepprover: Advancing automated theorem proving via critic-guided search. In 2nd for Math Workshop@ ICML 2025, 2025.
Jiaxuan Xic, Chengwu Liu, Ye Yuan, Sigi Li, Zhiping Xiao, and Ming Zhang. Fme: Formalization of natural language mathematical competition problems, arXiv preprint arXiv:2507.1 1275, 2025.
13

---

Published as a conference paper at ICLR 2026
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-provee Advancing theorem proving llms through large-seale synthetic data. arXiv preprint 2rXx::24055.4333,, 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-vl.. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08115 2024b.
Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388 2025.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. Advances in Neural Information Processing Systems, 36:21573- 21612, 2023.
Huaiyuan Ying. Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in Neural Information Processing Systems, 37:105848-105861 2024.
Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Tiantian Fan, Gaohong Liu, Lingjun Liu, Xin Liu, al. Dapo: An open-source IIm reinforcement learning system at scale. 2025a.
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathemati- cal reasoning of large language models. arXiv preprint arXi::2505.022 02255,, 2025b.
Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song. Zhenwen Liang Zhuosheng Zhang, Rui Wang, et al. Deeptheorem: Advancing Ilm reasoning for theorem proving through natural language and reinforcement learning. arXiv preprint arX1v:2505.23754, 2025.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematies. arXiv preprint arXiv:2109.00110, 2021.
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. minif2f: cross-system benchmark for formal olympiad-level mathematics. In International Conference Learning Representations, 2022. URL htnttts::/ooeerevieeee net. mttt:/orrmmm
14

---

Published as a conference paper at ICLR 2026
A MORE IMPLEMENTATION DETAILS
In this section, we provide a comprehensive implementation details of our proposed method. For additional insights and more intricate details, we refer the reader our supplementary materials.
A.1
IMPLEMENTATION DETAILS
Table 5: Key hyperparameters in the SFT phase.
Table 6: Key hyperparameters in the RL phase.
Hyperparameter
Value
Hyperparameter
Value
Learning Rate
le-5
Learning Rate
le-6
Batch size
512
Batch size
32
#Epochs
3
Group size per Question (G)
16
Chat template
Qwen
Temperature
1.0
Max Context Length
40960
Top-p
0.95
Warmup ratio
0.03
KI coefficient (A)
0.0
LR scheduler type
Cosine
Entropy coefficient
0.0
Supervised Fine-turning Phase. We utilize s Slime as our training framework for the initial su- pervised fine-tuning phase. The detailed syper-parameters for this phase are presented in Table 5 Since current LLMs lack inherent capabilities for our iterative autoformalization paradigm, we first construct high-quality training data that demonstrates both autoformalization and semantic self- validation behaviors. We employ a multi-agent system based on to generate training trajectories that embody our reflective paradigm. For each mathematical prob- lem in our source datasets (Section 4.1. we execute the following iterative process:
(-35--222B-TT- Think nnking ing
(Step 1) Initial Autoformalization: Generate an initial Lean4 formalization using standard
one-pass prompt (Appendix [.IIp
(Step Syntactic Validation: Verify the generated statement compiles successfully in Lean4. Non-compiling statements trigger subsequent refinement.
(Step 3) Semantic Consistency Evaluation: For syntactically valid statements, apply a consis- tency checking prompt (Appendix[D.2 to assess semantic alignment with the original problem. (Step 4) Reflective Refinement: When inconsistencies are detected, combine the failed statement with evaluation feedback to generate corrections using reflective prompts (Appendix) D.I D.2). (Step 5) Iteration:
Repeat steps 2-4 until either (a) semantic consistency is achieved, (b) maxi- mum iterations (3 rounds) reached, (c) further improvements generated.
This pipeline produces training trajectories that naturally interweave autoformalization attempts with oof--valiatiin and correction, providing rich supervision for learning our reflective paradigm. The resulting dataset contains 447,508 trajectories with iteration distributions detailed in Table / where 83.1% of problems achieve resolution within a single iteration while the remaining require multiple rounds of refinement.
Table Data Statistics for SFT and RL Phase.
Iteration Distribution
Stage
Data Type
Total
Iteration
Iteration 2
Iteration 3
SFT
Trajectories
371,679
65,734
10,095
447,508
RL
Question only
2,048
Reinforcement Learning Phase. For training data in RL phase, we start with a diverse batch of mathematical problems spanning various difficulties, grade levels, and domains. For each problem, we generate 8 candidate formalizations by sampling from our SFT model. These candidates were then evaluated against two successive criteria: compiler verification and semantic consistency
15

---

Published as a conference paper at ICLR 2026
check. From this pool, curate final dataset with 2048 items for RL. The selection was deliber- ately stratified to include problems with varying pass rates (i.e., the proportion of the eight samples that passed the checks), thereby ensuring the dataset represented a wide spectrum of formalization difficulty. Moreover, Table 6 summarizes the key hyperparameters used during the reinforcement learning phase. We also use 51 iime our RL frameowrk due its efficient and easy to
Inference Phase. During inference, we employ deterministic sampling with temperature 0.6 and top-p 0.95 to balance between generation quality and diversity. The maximum generation length is set to 40,960 tokens. We utilize vLLM as our inference engine.
A.2 IMPACT OF RL TRAINING ON ITERATIVE REFINEMENT BEHAVIOR
Reform SPT Reform NL
(S5.15)
80
Number of Samples
PELOG)
40-
02.0%
10
Figure 4: Iteration Distribution of our REFORM-SFT and RL.
We further analyze the distribution of iteration rounds for ReForm-80 8B across four benchmarks, comparing models after SFT and RL training stages. As shown in Figure the results reveal striking behavioral changes that validate our reflective paradigm's 's effectiveness.
REFORM-SFT exhibits a heavily skewed distribution, with 86.3% of samples terminating after a sin- gle iteration and the remaining samples distributed across 2-3 iterations pattern directly reflecting our SFT training data, which was capped at three iterations. In MnntrastREFFRRM-RR demonstrates markedly different behavioral pattern. Most notably, it explores iteration depths never seen during SFT training, with 0.7% and 0.3% of samples extending to 4 and 5 iterations respectively. More im- portantly, the overall distribution shifts toward deeper refinement: the percentage of single-iteration completions drops to 70.6%, while 2-iteration cases nearly double from 12.0% to 25.7%. This redistribution indicates that PBSO training successfully teaches the model to recognize when additional refinement is beneficial, rather than prematurely terminating the reflective pro- entirely absent from the SFT training
cess. The emergence of 4-5 itcration trajectorics-patte data-demonntrrates that PBSO enables genuine exploration beyond the supervised distribution, dis- covering more effective refinement strategies through trial and error. This finding is further cor- roborated by the consistent increase in average response length during RL training (Section 4.4), confirming that the model learns to invest more computational effort in challenging problems that benefit from extended reflection.
The results provide strong empirical evidence that our heterogeneous reward mechanism success- fully prevents the degeneration of self-validation capabilities while encouraging productive iteration when needed, ultimately validating the core premise of our reflective autoformalization paradigm: that iterative self-correction, when properly incentivized, leads to superior semantic consistency.
B THE CONSISTENCYCHECE BENCHMARK
Our annotation team for both the ConsistencyCheck benchmark and the aut- oformalization results in Section 4.5 comprised 6 members. All are senior PhD. candidates with strong background in mathematical competitions and prior experience in formalization-related annotation tasks.
Annotation Team.
httpp::/ thub. com/ http//vllmmppprrr 1m-project/v11
16

---

Published as a conference paper at ICLR 2026
Expertise & Training. To ensure high-quality and consistent annotations, rigorous training pro- tocol was implemented. This included dedicated sessions on interpreting the annotation guidelines, mastering the criteria for semantic consistency, and standardizing the handling of ambiguous or edge cases. Furthermore, all annotators are active researchers in Lean and formalization-relatte fields, possessing practical experience in formal proof development autoformalization.
Annotation Protocol. Our annotation protocol employed three-annotator design per statement to ensure robustness. Initially, two annotatios worked independently. Subsequently, a third senior annotator reviewed their annotations and accompanying textual comments (examples of which are provided in Appendix C) to perform cross-validation, resolve any discrepancies, and render the final judgment.
Annotation process. To construct high-quality benchmark for evaluating semantic consistency, we commission a team of experts with deep proficiency in both mathematics and Lean4. The anno- tators were tasked with assessing the semantic fidelity of formal statements from dataset composed of items from miniF2F (Zheng et al. 2022) and ProofNet (Azerbayev et al. (023), which were pre- sented to them an anonymized format. For each item, two experts independently compared the machine-verifan verifialee formal statement against the original natural language problem. If the formaliza- tion faithfully captured the problem's 's semantic intent, it was labeled as "Correct". any semantic discrepancy found, it labeled "Incorrect", and the annotators were required to provide a detailed written justification. In cases disagreement, a third senior expert was brought to adjudicate and determine the final label, ensuring the reliability of our benchmark.
Example of ConsistencyCheck Benchmark. A representative example of a semantic discovered in a ProofNet entry illustrated in Example B In this instance, the human-authored formalization contained two critical flaws: (1) a "constant term mismatch", where vII from the natural language incorrectly transeribed as 11; and (2) "degree bound inconsistency", where the constraint "degree < 80" was altered to "degree < 80". Notably, the annotation team also identi- fied another significant class of error in minil2F entries: cases where the formal statement included an explicit answer, while the original natural language problem did not. These instances were also systematically classified as "Incorrect." Such discrepancies underscore the profound difficulty of achieving true semantic fidelity, even in expert-curated datasets.
Based on this benchmark, we investigate the performance of each LLMs semantic consistency evaluation. These models are tasked with assessing the semantic consistency following the prompt specified in Appendix D.2 as discussed Section 4.5
Examples in ConsistencyCheck Benchmark
Example 1
set: ProofNet
name: exereise.5.4.33
split: test
question: If is such that p(a) 0, where p(x) - 1 + 220 2 + v50²+ vix+ VII,
show that a is algebraic over Q of degree at most 80.
header:
import Mathlib open Fintype Set Real Ideal Polynomial open scoped BigOperators
formal statement:
theorem exercise\_51_41
(a R] (p R+R) \n (hp À x, x\5 real. sgrt 2 x\* real.sqrt
x)2
+ \n real. 7 1n) (ha P = 0) \n 3 polynomial IR, p.degree support, 3 b Σ, p.coeff
2EE p.rooss A \n Wnip
//b b
17

---

Published as a conference paper at ICLR 2026
Human check
Incorreco
Human comment
2. Degree bound Consisteeng degree < 80 in natural language vs < 80 (i.e. S 79) in
1. Polynomial constant term mismatch: vII in natural language vs 11 in formalization.
inthematically inequivalent to the original -
drmmiiidieee These discrepancies make the Aomalizzation mathematically statement
mathertnn
Example 2
set: miniF2r name:
queess
split: test
question: Suppose is a real number for which
19
20
91
+
+
+
+
+
= 546.
100
100
100
100
Find [100r]] (For real x, [a] is the greatest integer less than or equal to x.) Show Show that it is 743.
header:
import Mathlib Animppos Aesop desoplainset, wnweetnstttoooo optionn andtearbbeat O'n\ ! nopen BigOperators Real Nat Topology ogy Rat An'n
formal statement:
theorem aime 1991_9911 p6 (r R) (ho : [ k in Finset. Icc (19
N) 91, int.flooz (r + 100)) 546)
Int. floor (100 r) = 743 = by
Human check Correct
C
CASE STUDY OF OUR REFORM
We present a detailed case study demonstrating our model's reflective inmoforrmann capabilities in practice. The skample below illustrates how REFORM reccessting identifies and corrects its own prmantte errors throught iterative self validatii...
Round I: Initial Attempt and Error Detection. The model generates its first autoformalization ins.maaiizzainnn attempt, then performs semantic self- validation by systematically five critical dimensiiinn (1) variable definitions and types, (2) aithematiee constraints and condi- tions. (3) logical aattoonsinnn between statements, (4) completeness of the cormalizannn and (5) aiismmen with the problem's ss intent. Through this structured analysis, the model autonomousy dientifiie semantic inconsistencies in its initial output (highlighted in red). red).
(2temaatiid)) analyzing the formalization across
Round 2: Self-Correction and Validation. Leveraging its self- geff-generated critique as feedback, the model produces& refined @ifooormaiiztionn that directly addresses the identified issues. The cor- rected
statement undergoes another round of semantic validation, this time passing all consistency checks. This successful self-correction comonstrates the model's ability to not only detect its own enror but also synthesize this understanding into improved sondelitiizzznnn
This example showcases the core strength of our reflective paradigm: the model's capacity for gen- uine self- seff-improvement without external intervention, achieving semantic Corectmes through itera- tive refinement guided by its own critical analysis.
18

---

Published as a conference paper at ICLR 2026
Example of Our REFORM
Question: What value of x will give the minimum value of x² 14x + 3? Show that it is 7.
The response of our REFORM:
<think>
Round (Autoformalization)
<round>>
The problem is asking for the value of æ that minimizes the expression x²² 14x - 3, and states that this value is 7.
To formalize this in Lean 4, need to express that: 1. The function f(x) = x²² 14r + has minimum Let me think about how to express this properly in Lean 4:
7 2. This means that for all real numbers x, have ((7) f(x)
'Lean
theorem test probler V x R, (7 R) 2 14 7 - 3 = by sorry
x
Wait, let me think about this more carefully. The problem is asking "what value will give the minimum value". This suggests we want to find the argmin of the function. Actually, let me be more precise. The statement should be that 7 is the point where the function achieves its minimum. So we want:
lean4 theorem gest_problen : V x I, (7 22 14 A 14 x
5 x
by sorry
...
But this is a bit awkward with the explicit casting. Let me try:
... lean4
theorem test_probles : V x R, 7-2 14 * 7
x
* x 3 = by sorry
...
Actually, in Lean 4, when we write
*7"2* where '7 R
should automatically be interpreted as real number. But to be safe, let be explicit:
lean4 theorem test test_problem : A R, (7 R) 14 * (7 R) I x 14
3 by sorry
I'll verify the calculation to ensure accuracy. The key is to confirm that 7 truly minimizes the quadratic expression by checking the algebraic properties of the function.
Expanding the squared term reveals the minimum occurs precisely at 7, with a value of -46. The algebraic manipulation shows x: 14x 3 reaches its lowest point when 7, supporting the original claim about the minimum value.
The Lean theorem captures this relationship, demonstrating that for all real numbers, the function's value at 7 less than or equal the function's value at any other point. Looking at this problem. I need to formalize the statement that x = 7 gives the minimum value for the expression x² 14x
19

---

Published as a conference paper at ICLR 2026
... lean4
import Mathlib
import Aesop
set Loption maxHeartbeats
open BigOperators Real Nat Topology Rat
theorem test peot_prrbeem : A x R, (7 2 14 * 7 + S x by sorry
Round (Semantic Self-validation)
It's time to assess the Formal Statement correctly captures the essence of the given math problem.
1. Math Assertion Analysis: The problem asks for the value of that minimizes the quadratic function x² 14r + and requires proving that this value is 7. The key components are: (a) the function f(x) x² 14x + 3, (b) the variable RR (c) the claim that x = 7 is the minimizer, and (d) the requirement to prove this claim.
2. Lean Statement Analysis: The theorem asserts Vz R, (72 - 14- 7 3) < x²² 14x + 3. This captures the inequality that the function's 's value at value at any other R. However, it does not explicitly state that x 7 is the minimizer (i.e., the argument where the minimum occurs). The theorem only asserts the inequality, not the existence of the minimizer or its uniqueness.
is less than or equal to its
3. Comparative Verification: The Lean statement correctly captures the inequality part of the problem (that f(7) is the minimum value). However, it does not explicitly state that x=7 is the value that achieves this minimum. The problem requires both identifying the minimizer (x=7) and proving the inequality. The Lean theorem omits the explicit identification of x=7 the minimizer, focusing only the inequality.
4. Conclusion:
The Lean statement is incomplete formalization of the problem. While it correctly captures the inequality that f(7) is the minimum value, it does not explicitly state that x=7 is the value that achieves this minimum. The problem requires both the identification of the minimizer and the proof of the inequality, but the theorem only addresses the latter.
Accuracy Confirmation: The Lean statement is incorrect. fails to explicitly state that x=7 is the minimizer, which is a critical part of the problem. The theorem only asserts the inequality, not the identification the minimizer.
Therefore, the outcome of the consistency verification is: Incorrect
</round>
Round (Autoformalization)
Time to reformulate the Lean Formal Statement based on verification analysis.
<round
## Thought Process
20

---

Published as a conference paper at ICLR 2026
Looking the informal statement and the critic, 1 see the issue with the previous formaliza- tion:
1. The problem asks for two things: -hhat value of x minimizes x² 14x + 3 Show that this value
The previous formalization only captured the second part (that gives the minimum value) but didn't explicitly state that 7 is the value that minimizes the expression.
3. To properly formalize this, I need to: Define the function f(x) x² 14x + 3 State that
7 is the unique minimizer this function
4. In Lean, a proper formalization would need to express both that 7 is minimizer and that it's the unique minimizer.
Given New Formal Statement:
... lean4
import Mathlib. luu
Calculus Der.seeeevvvvvv.e.eee..e. import Mathlib. Real. Basic
theorem test test_problem 1et f R +
X => x 14*x 3; f
(A x R, E7 E x)
A AA X R, x = 7) = by
sorry
Round 2 (Semantic Self-validation)
Now I'll check if the Formal Statement completely and correctly formalizes the mathemati- cal question.
1. Math Assertion Analysis: The problem asks for the value of æ that minimizes the quadratic function f=)) x² 14r and requires proving that this value 7. The mathematical structure involves: (a) defining the function f R IR, (b) asserting that = 7 is the global minimum (i.e., Vx, f(7) S fxx),, and (c) ensuring uniqueness (i.e.,
f(x) = f(7), then 7). The problem implicitly relies the function'' convexity (since the coefficient of is positive), guaranteeing a unique minimum.
2. Lean Statement Analysis: The theorem defines f R as x²
14r + 3. The conclusion asserts two claims: (a) Vz, f(7) f(x) (global minimum), and (b) (xx) = f(7) ~ x = 7 (uniqueness). The function definition, domain (R), and logical structure match the problem's requirements.
Comparative Verification: The Lean statement correctly captures both the existence and uniqueness of the minimum at = 7. The function definition matches the mathematical text. The universal quantifiers (Vx) and implications
(-) align with the problem's 's logical structure. The use of IR ensures the domain is preserved. No extraneous conditions or missing components are present.
Conclusion: The Lean statement accurately formalizes the problem's requirements.
The Lean statement correctly formalizes the problem. The function definition, domain, and logical claims (global minimum and uniqueness) align perfectly with the mathematical text.
5. Accuracy Confirmation:
Consequently, the outcome of the consistency check is:
21

---

Published as a conference paper at ICLR 2026
Correct
</round>
</think>
Final Statement
With successful verification, here's s the final Lean 4 Formal Statement:
lean4
import Wathlib.Analyan Calculus Cawculls..errv.................. Deriv. Basic import Mathlib. Real Basic
theorem test_problem :
let f R + = X => x 14xx 3; (4 x R, 7 x) (A R, X E 7) == by
sorry
111
D PROMPT
D.I INSTRUCTION FOR COLLECTING SET TRAJECTORIES
The autoformalization prompt firstly initializes the reflective data construction process by converting a natural language mathematical problem into a Lean formal statement.
When an initial formalization fails the semantic consistency check, this prompt takes input: (I) the original mathematical problem, (2) the failed formal statement, and (3) the detailed feedback from the consistency evaluation explaining the semantic discrepancies. By explicitly conditioning both the failure case and its diagnosis, the prompt guides the model to generate targeted corrections that directly address the identified issues rather than producing entirely new attempts that might introduce different errors.
This prompt operationalizes core insight that models can learn from their mistakes through structured self-reflection.
Reflective Autoformalization for Collecting SFT trajectories
You expert mathematician and Lean 4 programmer. Your task is to translate the given mathematical problem in natural language into formal statement Lean4 syntax, strictly following the guidelines below.
Guidelines
If the previous iteration of autoformation and consistency check results are provided, analysis and revise the autoformation according it.
If the math problem is algebra question, the answer will be provided well.
For non non-standard mathematical problems, first reformulate them into standard mathemati- cal format.
For complex problems containing multiple independent parts, break them down into separate theorems.
Must strictly follow Lean 4 syntax and utilize standard Lean mathematical library Mathlib4 components when possible.
1. Use correct type declarations and notation conventions
2. Include necessary imports
3. Leverage existing mathlib4 definitions and theorems
Follow proper naming conventions
22

---

Published as a conference paper at ICLR 2026
Pay attention the consistency between the Natural Language Statement and the Formal Statement in Lean4:
Variable domains (c.g.. N. 2, R. R++)
2. Boundary conditions (especially for special values like 0,1)
Quantifier scopes (V. 3)
4. Prerequisites and assumptions
Logical implications (-) 6-, A, V)
6. Function types and properties Set-theoretic notations
Only generate the translation. Do not try to solve prove the problem. Include clear documentation comments for theorems.
Input Format
Informal Statement: [Natural language description of math problem] History of Formal Statement and consistency Comments: [The existing Lean 4 formaliza- tion and its critique, or an empty string none exists.]
Thought Process
Formatted Mathematical Problem
1. List all known conditions
2. Define variables and their domains
3. State assumption
For multiple sub-problems:
Sub-problem [Description]
Sub-problem 2: [Description]
For revised autofomalization
1. Analyze ambiguities with natural language and potential mismatches
Evaluate consistency comments' validity
3. Identify missing assumptions or incorrect type signatures
Determine required mathlib imports Lean
5. Preserve original theorem name unless invalid
Output Format
Given New Formal Statement should always use end it:
'lean4 to start the code block and
'laan4
[Corrected Lean4 code]
Now! It's your turn to generate the Formal Statement. Informal Statement: [INFORMAL STATEMENT (QUESTION) HERE.) History Formal Statement and crities: (HISTORY HERE.) Thought:
The model's output here.
D.2 INSTRUCTION FOR SEMANTIC CONSISTENCY CHECK
This section presents the semantic consistency evaluation prompt that serves as the foundation for both our training and evaluation procedures. Specifically, this prompt template:
Powers the IsConsistent reward function during RL training, providing binary semantic correctness signals
Drives the consistency evaluation in our ConsistencyCheck benchmark, ensuring uniform assess- ment criteria
crucial component of SFT Trajectories by validating the outputs from both the initial and reflective autoformalization attempts.
23

---

Published as a conference paper at ICLR 2026
Instruction for Consistency Check
Your role is a Lean4 expert, please help me check consistency between natural language expression and its Lean4 formal statement.
Guidelines for Consistency Check
1. Core Checking Requirements:
When critique from previous autoformalization and consistency check result is provided, you must first analyze its findings and then assess their problems.
Must carefully compare the Natural Language Statement and the Formal Statement in Lean4 through a rigorous and explicit process.
Determine if the Lean thcorem statement an exact and faithful formalization of the mathematical problem
any result is Incorrect of consistency, briefly list all inconsistencies and reasons leading to the Incorrect determination in comments
Evaluation Stages
Math Assertion Analysis
Identify all structurally and semantically relevant components of the mathematical problem, including variables, types, quantifiers, constraints, logic structure, conclusion, and so on. The analysis should be based the actual content of the text.
Lean Statement Analysis
Extract all structurally and semantically relevant components from the Lean statement,
including
Variable domains (e.g., real numbers vs positive real numbers)
Boundary conditions (especially for 0,1)
Quantifier scopes
Prerequisites and assumptions
Logical implications
3. Comparative Verification
Check for exact correspondence between the math and Lean statements; you may refer to aspects like:
Semantic alignment, logic structure, and quantifier correctness.
Preservation of constraints and boundary assumptions.
Accurate typing and use of variables.
Syntactic validity and proper Lean usage (free from errors).
Use of symbols and constructs without semantic drift.
No missing elements, no unjustified additions, and no automatic corrections or comple- tions.
4. Final Judgement
Based solely on the above analysis, judge whether the Lean statement is a correct and exact formalization of the mathematical problem.
When a critique from a previous consistency check is provided, you must first analyze its findings and then assess their correctness. Result must be strictly "Correct" or "Incorrect" Use "Correct" ONLY when 100% mathematical equivalence is confirmed
5. Accuracy Confirmation
correct: clearly confirm why all elements match. If incorrect: list all mismatches and explain how each one affects correctness.
Intput Format
The Natural Language Statement:
[A math problem in Natural language]
The Formal Statement in Lean4:
lean4
24

---

Published as a conference paper at ICLR 2026
[A Lean 4 theorem statement formalizing the problem]
Previous round of autoformalization and sematic validation if provided: [The existing critique, or an empty string if none exists.]
Output Format
Return exactly one XML object
<comments>>>
Your brief analysis:
1. Math Assertion Analysis: [...]
Lean Statement Analysis (Proof Ignored): [...]
3. Comparative Verification: [...]
4. Conclusion: [...]
5. Accuracy Confirmation: [...match confirmation list of discrepancies...] </comments>
<consistency> Corrc//lnnorrees///ossssseyy
Now! It's your turn to compare the natural language statement with the formal state- ment in Lean4:
The Natural Language Statement (INFORMAL STATEMENT (QUESTION) HERE.
The Formal Statement in Lean4:
"lean4
(FORMAL STATEMENT HERE.
Previous autoformalization and consistency Comments:
(HISTORY CRITIC HERE}
Think about the consistent result:
The model's output here.
D.3 INSTRUCTION FOR ISFAITHFULCRITIQUE IN RL
Instruction for IsFaithuulCritqque
Your role a Lean4 expert, helping me review the previous consistency checking results.
Guidelines for IsFaithfulCrittque Check
Thoroughly examine the previous consistency result (Correct/Incorreet) and comments. Carefully evaluate whether the comparison results between informal statement and formal statement in previous consistency comments are correct, and the reasoning sufficient. Try to identify any errors in previous consistency comments. Trry to compare the mathemat- ical problem and the Lean4 formal statement to see if you would reach the same consistency conclusion. If you agree with the previous consistency result, provide your consistency result as "Correct": if you disagree, provide "Incorrect" and explain your reasons for dis- agreement in the comments. Intput Format
The Natural Language Statement:
[A math problem Natural language]
Previous Validation result:
[Previous Lean4 formal statement and semantic validation result]
Output Format
Return exactly xml object
25

---

Published as a conference paper at ICLR 2026
<comments>
Brief analysis of my semantic validation result, with improvements if needed. If previous result is not faithfull, explain why.
</comments>
Now review my consistency checking result:
The Natural Language Statement:
(INFORMAL STATEMENT (QUESTION) HERE.)
History formal statement and consistency check result: [PREVIOUS CONSISTENCY CHECKING COMMENTS HERE} (The model's output here.}
D.4 INSTRUCTION OUR REFORM
After collecting multi-turn autoformalization trajectories through our multi-agent system (Ap- pendix [.I]), we restructure these trajectories into unified format for SFT. The key insight to present the entire reflective process-including initial attempts, validation results, and iterative re- finements-ae as a single model response. This allows us to train models to internalize the complete reflective paradigm within their generation process.
Instruction for our Reform
Think step by step to translate the mathematical problem in natural language to Lean 4, and verify the consistency. (informal statement
The model's output here.
26


Reviews:
[{"review_id": "cfOS9yUCTN", "reviewer": "Reviewer_4Tg9", "summary": "This paper introduces **ReForm**, a reflective autoformalization paradigm that shifts from one-pass translation to an iterative process combining formal statement generation with semantic self-validation. To train this model effectively, the authors propose **Prospective Bounded Sequence Optimization (PBSO)**, a novel RL algorithm that uses heterogeneous rewards at different sequence positions to ensure both accurate autoformalization and faithful self-critiques. Extensive experiments on four benchmarks show ReForm achieves an average improvement of **17.2 percentage points** in semantic consistency over state-of-the-art baselines. The authors also introduce **ConsistencyCheck**, a benchmark of 859 expert-annotated items, which reveals that autoformalization is inherently difficult, even human experts make semantic errors in up to 38.5% of cases.", "questions": "See the above weaknesses.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "1.  **Novel Reflective Paradigm:** The core innovation is shifting autoformalization from a one-pass translation task to an iterative, self-correcting process. By mimicking the human expert's cycle of generation, validation, and refinement, ReForm directly addresses the critical challenge of semantic fidelity, moving beyond mere syntactic correctness.\n\n2.  **Effective Training with PBSO:** The proposed Prospective Bounded Sequence Optimization (PBSO) algorithm is a clever solution to the multi-objective credit assignment problem. It effectively trains the model to produce high-quality final formalizations *and* accurate intermediate critiques, preventing the self-validation mechanism from degenerating into superficial or hallucinated feedback.\n\n3.  **Rigorous and Comprehensive Evaluation:** The paper provides extensive empirical validation across four challenging benchmarks, demonstrating substantial and robust improvements. The creation of the expert-annotated **ConsistencyCheck** benchmark adds significant rigor, not only validating the use of LLMs as judges but also quantifying the inherent difficulty of the task itself.", "weaknesses": "1. **Heacy Dependence on LLM-based Evaluation**: The entire training and evaluation framework relies heavily on LLM judges (like Qwen3-235B and CriticLean-14B) to assess semantic consistency. While the authors rigorously validate these judges with their ConsistencyCheck benchmark, they still have a non-trivial error rate (about 17%). \n2. **Insufficient Ablation on Key Algorithmic Components**: While the paper demonstrates the overall effectiveness of PBSO, it lacks ablation studies on several critical design choices. The contribution of position-specific advantages is not isolated from the core bounded return mechanism, making it unclear if this complexity is necessary. Furthermore, the individual and interactive effects of the Task Reward &   Auxiliary Rewards are not thoroughly dissected.\n3. **Lack of Details of Human Evaluation**: Number of the annotators in total? Number of the annotators per statement? Background of the annotators?  and so on...\n4. The performance of 32B and 8B is very close, yet the author has not provided a reasonable explanation for this.", "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": "W0RY9EFwOa", "reviewer": "Reviewer_d2BC", "summary": "The paper presents ReForm, a novel reflective autoformalization framework that aims to improve the semantic fidelity of translating natural language mathematics into formal statements. Unlike traditional “one-pass” autoformalization models that generate a single formal output, ReForm introduces an iterative self-correction loop where the model alternates between formal statement generation and semantic self-validation. To train this reflective process effectively, the authors propose a new reinforcement learning algorithm, Prospective Bounded Sequence Optimization (PBSO), which integrates heterogeneous rewards for both the main task (final correctness) and auxiliary critiques (intermediate semantic validation). Extensive experiments across four challenging benchmarks (miniF2F, ProofNet, PutnamBench, AIME2025) demonstrate an average +17.2 percentage point improvement in semantic consistency over the strongest baselines.", "questions": "1. The paper both trains and evaluates with LLM-based judges (CriticLean for RL and Qwen3 for evaluation).  Could the authors verify cross-judge robustness, e.g., whether ReForm still shows similar gains when evaluated with a different LLM judge, such as Gemini or GPT-5?\n2. In Sec. 4.4, the authors show that responses get longer during RL, but longer ≠ is better. Can we disentangle “more tokens” from “better critiques”? For example, is there an automatic or human rating showing that later reflections actually introduce new semantic constraints (quantifier scopes, hidden assumptions, edge cases), rather than just paraphrasing previous critiques? A precision/recall–style analysis on detected error types would clarify this.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The target problem is well-motivated and addresses a clear bottleneck in formal reasoning: the semantic fidelity in autoformalization.\n- The integration of reflective reasoning and reinforcement learning is novel and effective; the experiments demonstrate consistent and interpretable improvements across multiple benchmarks.\n- The newly established ConsistencyCheck benchmark provides a valuable resource for quantitatively assessing the reliability of LLM-based metrics and for understanding the intrinsic challenges of mathematical autoformalization.", "weaknesses": "- The paper relies heavily on LLM-based semantic evaluation metrics, which, despite the ConsistencyCheck benchmark, may still introduce bias or circularity in measuring semantic consistency.\n\n- The computational cost and efficiency trade-offs of the reflective multi-iteration process are not fully analyzed — it remains unclear how scalable the approach is for large-scale or more complex formal systems.\n\n- Several important related works are missing; please refer to the recent surveys [1, 2] for a broader overview.\n\n- (Minor) There are too many autoformalization papers recently, which may cause aesthetic fatigue in the community.\n\n[1] A Survey on Deep Learning for Theorem Proving, COLM 2024. \n\n\n[2] Autoformalization in the Era of Large Language Models: A Survey, arXiv 2025.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "JsUinJU3NB", "reviewer": "Reviewer_63fq", "summary": "The paper introduces ReForm, a novel Reflective Autoformalization framework designed to convert natural language mathematics into machine-verifiable formal statements more accurately. Unlike previous one-pass translation approaches that often lose semantic fidelity, ReForm integrates semantic self-validation directly into the autoformalization process.", "questions": "Please check the **Weaknesses** section.", "limitations": "", "rating": 4, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper provides a **ConsistencyCheck benchmark** that rigorously evaluates the reliability of **LLM-based judges** and quantifies the challenges of **autoformalization**.  \n- Introduces **iterative reflection techniques from reasoning models** into the process of **autoformalization**.  \n- The paper is **well-written**.", "weaknesses": "- LLM is not a perfect supervisory signal, and I would like to know to what extent the capability of the judge model affects the stability of training.  \n- How did you handle **semantic alignment** in your method — was it **integrated into the reward design**?  \n- Please provide an **ablation study comparing process-level supervision and outcome-level supervision**.", "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)