Mathesis: Towards Formal Theorem Proving from Natural Languages
Authors: Yu Xuejun
Jianyuan Zhong
Zijin Feng
Pengyi Zhai
Roozbeh Yousefzadeh
Wei Chong Ng
Haoxiong Liu
Ziyi Shou
Jing Xiong
Yudong Zhou
Claudia Beth Ong
Austen Jeremy Sugiarto
Yaoxi Zhang
Wai Ming Tai
Huan Cao
Dongcai Lu
Jiacheng Sun
Qiang Xu
SHEN XIN
Zhenguo Li
Venue: ICLR 2026 Poster (2026)
Keywords: autoformalization
AI for math
AI for science
Lean 4
formal reasoning
parallel corpus
large language model
LLM
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Recent advances in large language models (LLMs) show strong promise for formal reasoning. However, most LLM-based theorem provers remain constrained by the need for expert-written formal statements as inputs, limiting their applicability to real-world problems expressed in natural language. We address this gap by focusing on autoformalization, the task of translating informal problems into formal statements. We propose Mathesis, the first pipeline for the systematic study of formal theorem proving from natural language. It contributes the first autoformalizer trained with reinforcement learning, which integrates syntactic, semantic, and prover feedback as reward signals to yield accurate and verifiable formalizations. This is further supported by our novel LeanScorer framework for evaluating semantic correctness. To assess real-world applicability, we introduce Gaokao-Formal, a benchmark of 495 complex proof problems from the college entrance exams. Experiments demonstrate that our autoformalizer improves pass rates by 45% on Gaokao-Formal and 6% on MiniF2F compared to state-of-the-art baselines. Paired with provers, our autoformalizer consistently enhances proving accuracy, including a 42% gain for DeepSeek-Prover-V2 on Gaokao-Formal. Our code is available at https://github.com/Huawei-AI4Math/Mathesis.

Published as a conference paper at ICLR 2026
MATHESIS: TOWARDS FORMAL THEOREM PROVING FROM NATURAL LANGUAGES
Xuejun Yu Jianyuan Zhong?:3. 2.3. Zijin Feng?* Pengyi Zhai' Roozbeh Mohit
Wei Chong Ng', Haoxiong Liu?, Ziyi Shou' Jing Xiong" Yudong Zhou' Claudia Beth Ong'
Austen Jeremy Sugiarto Yaoxi Zhang' Wai Ming Tai Huan Cao Dongcai Lu'
Jiacheng Sun Qiang Xu Shen Xin Zhenguo Li
'Huawci Celia Team
Huawei Foundation Model Department
The Chinese University of Hong Kong [Li Zhenguo, shenxinl (wwpxiinn9gghaaaeee wew@@hhawwwcomm
ABSTRACT
Recent advances in large language models (LLMs) show strong promise for for- mal reasoning. However, most LLM-based theorem provers remain constrained by the need for expert-written formal statements as inputs, limiting their applica- bility to real-world problems expressed in natural language. We address this gap by focusing on autoformalization. the task of translating informal problems into formal statements. We propose Mathesis, the first pipeline for the systematic study of formal theorem proving from natural language. It contributes the first autofor- malizer trained with reinforcement learning, which integrates syntactic, semantic, and prover feedback reward signals to yield accurate and verifiable formaliza- tions. This further supported by our novel LeanScorer framework for evaluating semantic correctness. To assess real-world applicability, introduce Gaokao- Formal, a benchmark of 495 complex proof problems from the college entrance exams. Experiments demonstrate that autoformalizer improves pass rates by 45% on Gaokao-Formal and 6% on MiniF2F compared to state-of-the-art base- lines. Paired with provers, our autoformalizer consistently enhances proving accu- racy, including 42% gain for SeepSeck-Proverrs V2 on Baokao-Formal. Our code is available hhttps:: /attps://github.. gightbt..h.....gggg www. Huawei
INTRODUCTION
The emergence of reasoning abilities in large language models (LLMs) has opened new frontiers in automated mathematics (Yang et al. 2025a). Recent automatic theorem provers (ATPs) leverage formal verification systems, such as Lean (mathlib Community 2020 Moura & Ullrich 2021 Isabelle (Paulson 1994), and Coq (Huet et 1997), to enable formal reasoning. Formal reasoning starts with clear formal problem statement, followed by the generation of mechanically verifiable proofs in formal languages. This approach ensures greater reliability and verifiability. Notable models in this field, including Deepseek-Prone Prove----ve-- V2 (Ren et al. 2025), Kimina-Prover (Wang et al.) 2025), and Goedel-Prover (Lin et al. 2025), are currently ofate-of-the-art on benchmarks such as Mini (Zheng et al.] 2021). proofNet (Azerbayev et al.) 2023). and PutnamBench (Tsoukalas) ct al. 2024), where the input problem statements have been formalized by human experts.
However, real-world mathematical problems are typically written in natural language, which pro- hibits the direct use by ATPs. Traditionally, manual formalization ensures faithful translation of problems but requires significant effort and expertise before ATPs can solve them. In this paper, study automatic formal theorem proving from natural language. The task begins with a given natural language (NL) problem statement and translates it into formal language (FL), followed by the generation of a formal proof. A critical step in this task is autoformalization the process of automatically translating informal mathematics into formal language (Gao et al. 2024)-whin can
Equal Contribution, Corresponding authors.

---

Published as a conference paper at ICLR 2026
Informal Statement: St, that {an arithmetic sequence.
sequence Oxe- 28n n 20, I. prove
Two Formal Statement Cases: theorem case_one (a N
RJ
(ha 3 d,
ta
Ezroneously includes the desired goal in
adsumptions
C Pinset. range :n sozzy
3 d, V 4
theorem case_two (a - B) N:N thi (n N), a 2 1, s
Σ
Finset.range Dr k) +
Σ Pinset. Icc n,
th : in Ni, a 2,1 2. 2.82l
(a
Ri
in
R) by sorry
3 ld B), V in N),
Figure 1: Illustrative examples of incorrect formalization. Case mistakenly includes the goal as an assumption, resulting in a circular yet technically provable formalization that mathematically invalid. Case 2 mistranslates the summation range, leading an incorrect formal statement that is both unprovable and misaligned with the informal input.
significantly impact the success of proving due errors introduced during formalization. Figure illustrates two common examples, highlighting how improper formalization can yield misleading proof successes or render problems unprovable.
Despite its importance, the task remains understudied, particularly in terms of semantic evaluation and the availability of powerful autoformalizer. On the evaluation side, existing methods rely on
Lean syntactic compilation checks and basic binary LLM judgments (Lin et al. 20255 Gao et al. 2024 Ying et al., (024)), which fail to capture nuanced semantic errors, resulting in the absence of fine-graieed evaluation and limiting the performance of formal theorem proving from natural language. Moreover, most existing formal benchmarks are not designed to assess the quality of autoformalization. These benchmarks might allow easy passage of basic checks but fail reveal semantic errors, necessitating harder-to-formaliz benchmarks for rigorous evaluation. Specifically, some benchmarks simplify the original problems in ways that alter their intent, exclude problem types that are challenging to formalize, such as those involving geometry, combinatorics (Zheng al. 202T), and word problems (Azerbayev et al., 2023). On the autoformalizer side, recent meth- ods (Jiag et al. 2023 Gao et al. [224] et al. 2025b Lin et al. 2025) fine-tune LLMs on paired informal and formal statements (a.k.a parallel statements (Jiang et al. [2023] Liu al.) (005b)) for higher quality, with Kinina-Autoformalle
(Wang et al. (0255) achieving state-of-the-an perfor-
mance via expert iteration. However, these training approaches lack dynamic learning from direct
feedback on both syntactic and semantic correctness.
In this paper, we present Mathesis (Multi-domain Autoformalization Through Heuristic-guided Syntactic and Semantic Learning), an autofornalization-tive that solving natural language problems. To our knowledge, we are the first to systematically study the entire workflow from natural language input to formal proof generation critical yet previously overlooked aspect in the community. At the core Mathesis is autoformalization framework trained via online reinforcement learning (RL) enhanced by novel Hierarchical Preference Optimization (HPO) mechanism. By incorporating Lean compilation and semantic verification into the RL reward function while learning prover preferences through HPO, Mathesis significantly enhances formalization quality and achieves state-of-the-ar performance. To enable rigorous and nuanced evaluation of formalization quality, we propose LeanScorer, novel semantic evaluation framework designed to capture subtle errors beyond binary correctness checks. We further introduce Saokao-Forraal a challenging benchmark of 495 proof problems, spanning a wide range of mathematical domains. Our key contributions are as follows.
formal theorem proving pipeline
the first
the first autoformalizer trained via online rein- forcement learning with rewards signals for syntactic validity, semantic correctness, and prover feedback. It improves pass rates by 22 percentage points (45% relative gain) on Forkao-Formal and points (6% gain) on MiniF2F over the state-of-the-ard baseline.
We introduce MaathsiisAAtoformmalii
2

---

Published as a conference paper at ICLR 2026
We propose LeanScorer, novel semantic evaluation framework that combines LLM- based analysis with the Sugeno Fuzzy Integral for nuanced assessment of formalizations. LeanScorer achieves 0.92 F1 score, outperforming prior approaches LLM-as-a-Judge by 7 percentage points and Re-informalization by 27 points on human-annotated data.
. We provide the first systematic study of formal theorem proving from natural language. Extensive experiments show that our autoformalizer consistently improves prover accuracy, with gains up 122% Gaokao-Formal and 98% MiniF2F.
2 RELATED WORK
Formal Reasoning Recent advancements have produced powerful LLM- based automated theo-
rem provers for proof assistants like Lean 4, including DeepSeek- Proveer-22 (Ren et al. 2025).
Kimina-Prover (Wang et al., 2025), and Goedel-Prover (Lin et al. 2025). alongside many advacc algorithms for proof search (Liang et al. 2025 Xin et al. 2025 Li et al. 2024, Liu et al. 2025a
Yang et al.] 2025b). These systems demonstrate strong formal-to formalll (F2F) reasoning capabili- ties, where both input statements and output proofs are expressed in formal language. Correspond- ingly, benchmarks such MiniF2F (Zheng et al.] (021]. PutnamBench (Touualas et 22024). and FIMO (Liu et al.) 2023) are designed to evaluate such F2F reasoning ability using well-formalized problem statements. However, it leaves critical gap in the study of formal theorem proving from natural language, which requires first formalizing the input informal mathematical statements and then proving them. Our work addresses this gap by introducing a complete pipeline for formal theo- rem proving from natural language, grounded in autoformalization. While some other works (Zhao al. 2023 Wang et al., 2023, Diang et al., 2022, Cabral et al., 2025), such as Lego-Prover (Wang et al. 2023), also target informal-to-fe formaal reasoning, they require an additional informal proof sketch as input. In contrast, our approach performs fully automatic, autoformalliaaioo-diiii
for- mal theorem proving, starting solely from informal statements to whole-proof generation (Xin et al. 2024). making direct comparisons inappropriate.
Autoformalization, the process of formalizing informal mathematics into for- mal language , is essential for bridging the NL-FL gap. Prior work includes prompting pre-trained
Autoformalization
LLMs (Wu et al. 2022, Azerbayev et al. 2023 Poiroux et al. 2024] Patel et al. 2023) and fine-
tuning models
static NL-FL pairs (Cunningham et al.) 2023 Jiang et al. 2023 Lu et al. 2024b
Gao et al. 2024 Liu et al. 2025b), with systems like Aimina-Autoformaiize (Wang et al. 2025
achieving notable success. However, these approaches often lack dynamic learning from direct feedback on syntactic and semantic correctness, and their evaluation has typically relied on binary
compilation checks basic LLM judgments (Peng et al.) 2025 Lin et al. 2025 Liu et al. 2025b
which may not capture nuanced misalignments.
Semantic evaluation itself remains key bottleneck. Training-free methods such LLM-as-a-Judge (Lin et al. 20225 Gao et al.) 2024) and Re-informalization (Ying et al., (024) are most widely used, but they offer only indirect signals of semantic correctness and can be inconsistent. In contrast, For- malAlign (Lu et al. 2224a) offers training-based alternative by fine-tuning an alignment model to compute likelihood- and representation based scores, though such trained evaluators may generalize less effectively to out-of -utto--distribution mathematical problem types.
To address these limitations, we introduce Mathesis Autiiesssss,uutooomaliieee, which, to our knowledge, is the first autoformalizer to leverage online reinforcement learning and the feedback from the prover for improved accuracy and robustness. Concurrently, our LeanScorer framework provides a more fine-grained evaluation of autoformalization quality, moving beyond simple binary pass/fail metrics.
Reinforcement Learning Fine-Tunine (RLFT) Reinforcement learning has proven highly ef- fective for enhancing I.LM capabilities in complex reasoning (Anthropic) 2024 DeepSeek-Al & Anonymous Contributors] 2025). The autoformalization task is well-suited for RI, as syntac- tic validity (from a Lean verifier) and semantic correctness (e.g., assessed by an LLM judge or LeanScorer) can serve as direct reward signals. Despite this clear potential, the application of outcome-basee RL techniques to specifically optimize these syntactic and semantic proper- ties in autoformalization models has been largely underexplored in the literature. Our Mathesis- Autoformalizer pioneers this direction by employing Group Relative Policy Optimization (Shao) et al. 2024) with carefully designed composite reward function (in Section 3.1). This approach
3

---

Published as a conference paper at ICLR 2026
Syntax-Valid Statements
Syntax- & Semantio-Valid Statement
Valld Proof
Statemand
Autoformalizor
Leen check
Statement
Prover
Proof
check
Statement 2
Statement 2
Proof 2
Figure 2: Overview of our autoformalizaaion--ivve formal theorem proving pipeline.
allows the model to iteratively refine its ability generate syntactically correct and semantically faithful formalizations, addressing key gap in existing autoformalization methodologies.
3 MATHESIS: AUTOFORRMALIEATIIN-DDRRI
FORMAL PROVING
The core objective of this paper is to tackle the task of formal theorem proving from natural lan- guage (defined Section I by enabling automated formal reasoning directly from informal natural language inputs. To this end, illustrated in Figure 2 we propose structured, multi-stage pipeline built upon an autoformalizatiio-drrvvee approach. It consists of three major stages: autoformaliza- tion, validation, and proving. The pipeline begins with given NL problem statement, which is first processed by an autoformalizer to generate candidate formal statements in Lean This stage is powered by our MathesissAAutooormallii formalization (see Section 3.1). These candidates are then evaluated the validation stage, which includes syntactic verification via the Lean compiler and semantic evaluation. For this purpose, we introduce novel evaluation framework, LeanScorer, and a new benchmark Gaokao- Forioal (see Section 3.2) The formal statement that passes the Lean compiler and semantic assessment is then passed to the final proving stage to generate complete, machine-verifiabl Lean proof.
model that achieves state-of-the-ar performance in
Our approach is, principle, transferable other proof assistants such as Isabelle. We focus on Lean 4 due to its broad adoption in recent literature and its well-supported evaluation stack.
3.1 Mathesii-AAutoormmlizerr ADVANCING AUTOFORMALIZATION WITH REINFORCEMENT LEARNING
The cornerstone our pipeline is Mathesss-AAuooorrmalizzz a novel model designed to translate in- formal mathematical problem statements from NL into formal Lean 4 (mathlib Community 2020) code. Unlike prior approaches that predominantly rely on supervised fine-tuning (SFT) on static datasets, our work presents the first autoformalization model trained with online reinforcement learning via Group Relative Policy Optimization (GRPO) (Shao et al., (224),, using reward signals for syntactic validity and semantic correctness, and incorporating prover-derived feedback. Training proceeds in two stages: GRPO aligns the model to syntactic compilability and semantic faithfulness, after which Direct Preference Optimization (DPO) further aligns to downstream proof success by preferring formalizations that lead to Lean-verified proofs. We refer to this two-stage procedure as Hicrarchical Preference Optimization (HPO).
Composite Rewards for Autoformalization Let me represents the translator LLM policy param- eterized by 0, and Fref be a fixed reference policy (typically the SFT model). In our experiment, the policy Te initialized from Kimina-Autoformalic the-art 7B autoformalizer trained via supervised fine-tuning with expert iteration to translate natural language problems into Lean code. This initialization provides strong structural prior, equipping the model with canonical Lean formatting patterns and facilitating subsequent reinforcement learn- ing. For given natural language input æ E X. the policy TH (-122) generates a group G candidate formal Lean 4 statements outputs {oI,... ..., og). The optimization objective is to adjust 0 to max- imize the likelihood of generating higher- group, while regularizing against large deviations from the reference policy. We define composite reward with two binary components. For an given input x and a corresponding candidate formaliza- tion og define the Semantic Correctness Reward R (xr, oz) to indicate whether o, preserves
(Wang al.) 20255.. the previous state-of-
outputs relative to lower-reward ones within the
4

---

Published as a conference paper at ICLR 2026
the semantic meaning of æ, judged by auxiliary LLM evaluator Jsem:
1 if Jsem (z, 0;) judges "Appropriate"
Remm (I. 01)
otherwise
We also define the Syntatic Verification Reward (o)) indicate whether or is syntactically correct and type-valid under the Lean 4 verifier (Viean), checked up to :- by sorry:
Reer (o:) = {()
Viean (0:) succeeds
otherwise
The final overall reward ri for an output og is computed as a combination of the two components: r, R(x, Og. Ores) = Raem + Rver- We then leverage the GRPO objective to update To (-(2)z)) We find that this simple yet effective summation strategy indeed leads to statc-of-the-ar performance. The rationale for this composite reward is to capture two orthogonal constraints: syntactic validity is necessary condition- -osioon-ooo-vveeee non-verifying candidates are unusable by the prover-while semantic correctness ensures that the formalized statement corresponds to the intended problem be solved. Although both terms are binary, GRPO optimizes within-group preferences rather than absolute magnitudes; we normalize rewards within each group before forming pairwise comparisons, which makes the objective insensitive to uniform rescaling simple weighting. We adopt the unweighted sum for simplicity, noting that weighting schemes are a reasonable direction for future work.
Training Data Curation To effectively identify samples for training, our data curation process employs topic modeling with BERTopic (Grootendorsi, 2022) to the natural language informal state- ments of problems from pset (Lin et al.] 2025) and our in-house Gaokao dataset. BERTopic was selected for its ability to generate coherent topics by leveraging contextual embeddings and cluster- ing, allowing for effective categorization of problems based on their semantic content; this approach is also significantly faster and more cost-effective than using large language models for the same categorization task. We generated embeddings for each statement, performed dimensionality reduc- tion and clustering, and then mapped the resulting topics to predefined mathematical categories in Section 3.33 The categorized data from two sources were then merged. To optimize Reinforcement Learning training efficiency with GRPO, employed our base model (pre-RL) perform rollouts (k=14) on each problem, filtering out those yielding rewards with zero standard deviation across the rollouts. The remaining problems demonstrating reward variance were combined with 8,000 prob- lems randomly sampled from the Lean Workbook (Ying et al. 2024), resulting in a final training dataset of approximately 32k problems.
Hierarchical Preference Optimization for Theorem Proving GRPO provides reward- maximizing initialization, aligning the autoformalizer with local objectives of syntactic correctness and semantic validity. In the context of formal theorem proving from natural language, the auto- formalizer formalizes natural language into formal statements aimed at facilitating successful proof generation by the prover. To enhance this, we further fine-tune the autoformalizer using Direct Pref- erence Optimization (DPO) (Rafailov et al. (2023), where preferences are derived from the global success of the downstream proof generation.
DPO Training Data Generation During the data generation phase, for each natural language statement æ, group of candidate formal statements o, are sampled from the autoformalizer n (- where i indexes the candidates. Each o; undergo syntactic and semantic validation, and those that pass are forwarded to the prover, which attempts to generate proofs z'_ Preferences are assigned based on the successful completion of the proof verified by Lean, yielding data tuple {x, of" 24") for successful cases, and {I. of. 2!) for failed attempts.
DPO Training The training configuration employs single epoch with a learning rate of 1 x 10-5 The KI. regularization coefficient ,3 set to 0. penalizing deviations from the reference model. Optimization is applied to full parameters, with warmup ratio of 0.05. To manage memory usage efficiently, training is conducted using DeepSpeed zero3 offload.
DPO fine-tuning enhances alignment with task-grounded outputs, thereby mitigating mismatches between reward function and actual task objectives. Compared to GRPO, DPO is a more sample- efficient and stable alternative that performs offline preference learning and eliminates the need for a separate reward model (Rafailov et al., 2023] Ouyang et al.] (022). However, its effectiveness heavily relies strong base model to generate meaningful candidate outputs and better exploit
5

---

Published as a conference paper at ICLR 2026
Natural Burament and oa o
Subtaskc
Semunti Consiitercy Labels
Scaring
Decompoation
Forelm 2
Autsbmallstttn
Leas 31 Aei.nkkk -e 3 Tak-ll
Subtask Exslvaation
FNLL
Langag Statement pevergustion in 1i th th V 1C (o:3/2-00 mity iirrostrangg (TrE+
Male 3 1//g < 5/2
Suqees teiegral bcare bastack))
Dera rageeiaooo The Lean venson
Maac glrer wwc.iniionn
Check for mioding conditass linplich cindilioe:
Figure 3: Overview of LeanScorer semantic evaluation framework.
preference signals (Tu et al. 2025 Wang et al. 2024; Pan et al. 2025). To this end, we first apply GRPO to establish a strong initialization before proceeding with DPO fine-tuning.
3.2 LeanScorer: FINE-GRAINED SEMANTIC EVALUATION FOR AUTOFORMALIIATTION
The evaluation of autoformalized problem statements typically follows a two-step process: a syn- tactic check conducted by the Lean compiler, followed by a semantic check, which verifies that the formal statement preserves the intended meaning of the original natural language input. Existing approaches to semantic correctness (Lin et al. 2025) Gao et al.) 2024 Ying et al.. 2024) rely on LLMs and are limited to binary judgments (i.e., correct or incorrect). this section, we propose LeanScorer, novel framework that produces a continuous correctness score, enabling fine-grained and adapttte assessment. Figure provides an overview.
Subtask Decomposition and Evaluation Given a natural language (NL.) statement and its corre- sponding formal (FL) statement, LeanScorer first decomposes the NL statement into subtasks such as premises and conclusions. Each subtask is then aligned with its counterpart in the FL statement and assigned one of three labels: Match (M1), Minor Inconsistency (Ml/2), or Major Inconsistency (MO). Specifically, clear mathematical inequivalence Inconsistency": semantically equivalent but divergent expressions are labeled as "Minor Inconsis- tency": and exact alignment in both content and structure is labeled as "Match". This three-level labeling scheme enables nuanced semantic evaluation while accommodating the inherent variability in LLM outputs. Any extra assumptions or conditions in the formal statement that do not cor- respond to natural-lange languae- subtask are marked as misaligned; likewise, any natural-language subtask missing from the formalization is also treated as a misalignment. This enables LeanScorer to detect both additions and omissions. Prompts are provided in Appendix E
omitted conditions are labeled as "Major
Aggregation via Sugeno Fuzzy Integral subtask-level labels using the Sugeno Fuzzy Integral (Sugeno 1974). a well-established method in multi-criteria decision-making (MCDM) [Wieezynski et al. 2024). We design a customized fuzzy measure that tolerates minor inaccuracies in the LLM judgments while enforcing strict criteria: it strictly penalizes any formalization with a subtask labeled as a Major Inconsistency, grants a full score when all subtasks are labeled as Match, and multiple Minor Inconsistencies incur propor- tional deductions. This method enables robust label aggregation under LLM outputs variability and upholds rigorous evaluation criteria.
To compute an overall correctness score, we aggregate
Let N = {1, ....I,, denote the of subtasks, and let L = (l,,..., ( the corresponding label set, where each 4 E (MI, MY/2, M0} denotes the semantic consistency label of the i-th subtask. We define an evaluation mapping function f L >> [0, 1], where we set f(M1) = 1.0, f(M!/2 = 0.5, and f f(M)) O. To aggregate the semantic quality over a subset C L, we introduce the fuzzy measure (s)) defined as:
E E MO,
m(s)
max
The - moms)) -1mm)) oo
otherwise
(1)
m
where ny and RaDs denote the number of elements in s and elements labeled and M1/2 in s. respec- tively. The coefficient 8 is set to 0.1 when 7aa 1, and 0.2 otherwise. We conducted sensitivity analysis by varying the value of f (M1/2 from 0.1 to 0.9 in increments of 0.1 (see Appendix D), and observed that the performance remains robust: the F1 score remains stable 0.92 for values between

---

Published as a conference paper at ICLR 2026
0.1 and 0.5, and drops slightly to 0.88 for values between 0.6 and 0.9. Thus, set f f(122 0.5 in all experiments. To further validate our design choices, we also conduct an ablation study comparing Sugeno Fuzzy Integral- based aggregation against alternative aggregation methods in Appendix
Next, let the labels be sorted in ascending order as f(+(1)) S f((x(2) I ... S f((+(m)) with (I(,,, (2), (2))
क (n)) representing the corresponding indices. For each i [I,...,,), we define the suffix set ( (n(n)) which represents the subset consisting of (m(s) and all labels ranked after it. The overall LeanScore is then computed as:
S(L. f.P) max min (f(l(()), p(s:))
Ssinn
A decision threshold [0, may optionally be applied map the LeanScore to binary decision.
3.3 THE GAOKAO-FORMAN BENCHMARK
To advance automatic formal theorem proving from nat- ural language, introduce the Gaokao-Forme bench- mark. Unlike existing benchmarks that focus primarily on formal-to-formal proving sometimes exclude those problems that are hard to formalize, Gaokaa-Formal specifically targets the difficulties of auto-formalizing di- verse and complex natural language mathematical state- ments, aiming to motivate real-world applications of for- mal reasoning.
Table I: Summary of Gaokao-Formal Benchmark Categories.
Category
Count
Functions
168
Sequences & Series
148
Analytic Geometry Comprehensive Questions
76
49
Inequality
28
This benchmark consists 495 proof problems from China's National Higher Education Entrance Examina- tion (Gaokao, 2008-2025), often include sub-questions. Each instance contains the original Chinese problem statement, an English translation, and a human-expert formalized Lean formal statement. A sum- mary of question categories is provided in Table I with example problems available in Appendix C
Trigonometry Probability Combinatories
22
Remark. The Gaokao dataset utilized in this study consists of publicly available official statistics,
administered by government authorities. is classified as envermment-manaeee public information and does not involve privately copyrighted material.
4 EXPERIMENTS
We evaluate our proposed approach along three axes. First, we assess the semantic consistency evaluation framework LeanScorer. Second, we compare the Mathesis-Autoformalizee with state- of-the-art autoformalization baselines. Finally, we measure how improved autoformalization affects formal theorem proving from natural language. Experiments conducted on newly introduced Gaokao-Forna benchmark and the widely adopted MiniF2F-test set. We compare our Mathesis- Autoformalizer with strong API-based and open-source baselines, including the prior state of the art Autiiinaiutof (Wang et al. 2025) and Beeradd-Autfformalii [ao et al. (2025). For pipeline evaluation, we pair each autoformalizer with the current best-in-class 7B provers- Kimina- Prover (Wang et al., 2025), 2025) with COT mode tasking the prover to generate proofs from the formal statements produced by the respective autoformalizer and reporting proof success rate.
(Lin et al. 2025), and DeepSeek-Provert V2 (Ren et al.,
Autoformalization quality is measured by two standard metrics: Lean Check success rate at k can- didates (LC@k) for solely syntactic validity, and Lean Check combined with LeanScorer semantic checking (LC+LSC@K k) for overall correctness, jointly assessing syntactic and semantic correctness. We reported results for k 1 and A = 6. Mathesis pipeline performance is measured as the proof success rate, given a fixed search budget 32 attempts per problem, by convention. Additional im- plementation details, including training configurations and prompts, are provided in the Appendix.
4.1 SEMANTIC CONSISTENCY EVALUATION FRAMEWORK
We first validate our LeanScorer against two widely used but indirect, ground-truth fruth-ffree baselines:
I. LLMa-a-a-Judge (Lin al. 2025 Gao al. 2024 and Re-informalization (Ying al. 2024). The
7

---

Published as a conference paper at ICLR 2026
subset of Stokao-Formal containing both correct and incorrect autoformalizations. Annotation details are in Appendix G Unless otherwise noted, the decision threshold is set to 0.6. statement matches a natural-language statement and outputs a single semantic-correctnen judgment. Re-informalization evaluates semantic consistency by first back-translating the formal statement into natural language and then comparing it with the original input, involving two LLM calls per round. Both baselines incorporate test-time scaling and accept formalization only when all four outputs agree. In contrast, LeanScorer performs LLM-an --sistedd subtask decomposition and consistency anno- tation in single pass using two LLM calls, one for decomposition and one for annotation, followed by computationally efficient aggregation step to produce a semantic-consistency score.
evaluation uses
directly prompts LLM to decide whether formal
Table@ that LeanScorer achieves an F1 score of 92%, significantly outperform- ing both the L.L.Mas-a-Judee and Re-informalization (65% F1). While LLM-as-a-Judge has 100% recall, its 73% precision is low, yielding many false pos- itives. Re-informalization is the oppo- site, with 93% precision but 50% recall. LeanScorer delivers both high precision (94%) and high recall (89%), indicating balanced and reliable semantic consistency checker for formalization evaluation. This balance is important for downstream performance: high precision ensures that only semantically correct formalizations reach the prover, while high recall increases coverage but also admits more misaligned statements. Since we require Lean-verifee proof for the original natural- latural-languag problem, maintaining both high precision and high recall is essential for reliable overall performance.
Table 2:
Semantic evaluation framework performance measured by agreement with human annotations.
(85% FI)
Method
Precision
Recall
F1
LLM-as-a-Judge Re-informalization
73
100
0.85
93
50
0.65
LeanScorer (Ours)
94
89
0.92
4.2 AUTOFORMALIZATION FROM NATURAL LANGUAGE
The core contribution of our work is the Mathesis-Autoformalize designed to translate natural language problems into syntactically valid and semantically faithful Lean4 statements. In this section, we evaluate two variants: Mathesis-Autofrrmall Luthesis-Auttfoommlizeeer
obtained after the GRPO stage, and obtained after the full two-stage Hierarchical Preference Optimiza- tion training (GRPO followed by DPO). These models are compared against state-of-the-art API- based and open-source baselines, including Kimina-Autoformalize which serves as our base model and was the strongest publicly available 7B autoformalizer before our work. Evaluations are con- ducted on the MiniF2F-test, Putnam, and Gaokao-Forte -Frmmal benchmarks. Performance is measured using Lean Check (LC@k) for syntactic validity and Lean Check plus LeanScorer Semantic Check (LC+LSC@K) for overall correctness. For fair comparison, our models are compared directly against open-source 7B baselines, with top scores underlined highlight improvements at equal model size. API models, which are much larger in size, are compared within the group, with the top scores shown in bold. All models are evaluated with 600-second timeout per prompt.
Table presents the results. Both Mathesis variants outperform all baselines across datasets and budgets, with the largest gains on the more challenging BaokaooFoormal benchmark. Specifically, achieves an LC+LSC@* @6 score of 71% on Gaokao-Formal, surpass- ing the previous best of 49% by Kimina-Autoformalizer with an absolute improvement of 22 per- centage points and a 45% relative gain. On another challenging dataset Putnam, Mathesis-HPO achieves 30% LC+LSC@6 score, compared with 10% from
and 9% from Herald-Autoformaaiia corresponding to 200% and 233% relative gains, respectively. On MiniF2F- test, it reaches new record LC+LSSC score of 96%. Mathesis-HPO reaches 96% LC+LSC@6, establishing new state of the art for overall pass rate on this dataset. Mathesis- constantly out- performs all much larger API-based models across datasets in both LC@6 and LC+LSC@6, with an average of 31 % and 86%, resp., except for DeepSeek-RI R1 on challenging Putnam in LSC. In terms of LC, our method improves over Gaokao Forkaa,Formal, demonstrating superior syntactic reliability grounded in Lean's 's compiler feedback.
by 4 points on MiniF2F and points on
These improvements support the effectiveness of our training methodology. By employing re- inforcement learning with composite reward that combines Lean-based syntactic signals and
8

---

Published as a conference paper at ICLR 2026
Table 3: Quality assessment of formalized statements. LC denotes Lean Check; LSC denotes
LeanScorer Semantic Check. Top scores for API and open-source models are bold and underlined.
Model
MiniF2F-Test
Putnam
Gaokao-Formal
LC LC+LSC
LC
LC+LSC
LC
LC+LSC
API Models
03-mini
58
45
38
25
6
87
77
13
70
54
GPT-4o
1
50
36
20
13
80
65
48
28
Doubao-1.5
1
48
40
19
15
77
70
10
32
Gemini-2.0
1
56
41
20
10
36
22
80
71
47
Deepseek-V3
1
76
61
10
54
36
6
91
84
22
10
69
56
Deepseek-RI
1
54
44
29
14
45
30
6
86
76
37
57
Open-Source Models Herald-Autoffrmalizer
80
41
35
56
14
6
95
69
64
78
27
Kinina-Autoformalizer
83
61
50
21
6
100
91
30
10
91
49
Nathesis-AAttffrmmalieer
1
92
69
31
9
88
45
100
95
65
25
98
67
Mathesis-Autoformaliee--PP
1 99
79
38
10
93
50
100
71
LeanScorer-basee semantic signals, the model learns to produce formalizations that are both syntac- tically sound and semantically faithful-an essential capability for reliable automated reasoning.
4.3 AUTOFORMALIZATION-
THEOREM PROVING
The ultimate measure of our approach's ss effectiveness is its performance on formal theorem proving from natural language. We posit that the quality the autoformalization critically influences the final proving accuracy. Accordingly, evaluate the proof accuracy on MiniF2F-Test and SaookaoForraa The results are shown in Figure
pair each autoformalizer with downstream provers and
Autoformalization quality correlates with proving accuracy. There is a strong positive corre- lation between autoformalization quality and proving accuracy, where proving accuracy denotes the rate at which the prover produces complete and correct formal proofs. Across all provers and both datasets, accuracy improves consistently the autoformalizer improves. For any fixed prover, placing Herald or Kimina with our Mathesis-HPO yields substantial gains. On Gaokao-Formal, replacing Herald with Mathesis-HPP improves the accuracy of Goedel-prover, Kimina- Kimina-prover, and Deeepseek-Provee Prover- V2 by 86%. 116%, and 122%, respectively. relative to Kimina, the gains are 49%, 33%, and 42%. On MiniF2F-Test, the same replacement improves the three provers by 98%, 77%, and 51 over Herald, and by 6%, 9%, and 5% over Kimina.
These improvements arise because a stronger autoformalizer supplies the prover with a larger num- ber of compiler-valic and semantically faithful Lean statements, providing well-structured and solv- able goals. Mathesis- Autoformalizer-HHee the DPO stage incorporates prover-derived preferences, favoring formalizations that not only com- pile and align semantically but also lead to successful proof completion. Additional evaluations on autoformalizer output before and after DPO provided in Appendix H
further outperforms Mathesis-Aurr Autoformalizer because
Autoformalizer improvements dominate prover upgrades. For problems that are intrinsically harder to formalize, the performance gains from a stronger autoformalizer often exceed those from stronger prover. On Gaokao-Formal, holding the prover fixed and replacing Herald with Mithesis-HPO increases accuracy by 86% for Goedel-Prover, 116% for Limina-Proved and 122% for
By contrast, with the autoformalizer fixed, upgrading the prover from

---

Published as a conference paper at ICLR 2026
Herald
Kimina
Mathesis
Mathesis-HPO
Gaokao-Formal
MinF2FFTest
30
50
60.369.4
25.1
60
57.8
Accuracy (%)
17.7
50-
Accuracy
13.0
11.3
9.1
8.0
20
Kimina-Prover-78 Deop5eck-Prover-2-788
Goedel-Prover-78
Kimina Prover-78 P2-
Figure 4: Performance of formal theorem proving from natural language. In each subfigure, bars are grouped by prover the x-axis, and the y-axis reports pass @ass@32 proving accuracy. Bar col- ors encode the autoformalizers Herald-Autoformaalze (Herald), Lamina-Autoformalizee (Kimina), Mathesis-Autoformalizee (Mathesis), and Bathesis-Auuffommliee--tttt
(Mathesis-HPO))
Geodel-Prover to Deepseekp-Proover- V2 increases accuracy by 55% under Herald and 95% under Kimina. This disparity underscores fundamental challenge in real-world mathematical reasoning: before a proof can be constructed, natural language problems must first be accurately converted into formal statements that theorem provers can process. Suboptimal formalizations, such as encoding problems using difficult-to- unfold built-in functions or embedding questions within overly complex mathematical definitions, create significant obstacles for downstream proof search (this phenomenon is also observed by Lin et al. )) Our results indicate that formalization quality constitutes critical bottleneck, as provers are hindered by suboptimal formalizations that obscure the problem's 's structure or introduce unnecessary complexity. Hence, achieving high accuracy requires both strong autoformalizer and a strong prover, attesting to the critical role of formalization.
Ablations on pipeline design. As shown in Table and Figure 4 adding HPO on top of GRPO improves pass rate from 67% to 71% on Gaokao Formal and from 95% to 96% on MiniF2F. In downstream proving, Mathesis-HH HPO consistently outperforms Mathesis cross provers by an average of 13% on Gaokao-Formal and 2% on MiniF2F. These results show that HPO's prover-derived feedback as reward yields measurable end-task gains and better aligns the autoformalizer with proof success beyond gains attributable to syntax and semantic checks alone.
LIMITATION
While approach demonstrates significant improvements, formal theorem proving from natural language remains far from full automation and real-world deployment. During the development of Aathesis-Autoformaaliae
and LeanScorer, is often difficult to define directly and must be determined based on whether it affects the proof process (e.g., whether functions need explicit domain declarations). This ambiguity in formalization correctness presents ongoing challenges for both training and semantic evaluation.
discovered that the correctness of formalization
6 CONCLUSION
Motivated by the goal of bringing formal reasoning to real-world proof questions, we introduce the task of formal theorem proving from natural language and present Mathesis as a comprehensive so- lution. Our erarchical Preference Optimization, and LeanScorer for robust semantic evaluation both achieve sig- nificant improvements over existing methods. This work lays solid foundation for future advances toward fully integrated and scalable formal reasoning systems, bringing formal theorem proving to real-world mathematical problem solving.
trained through online reinforcement learning with novel Hi-
10

---

Published as a conference paper at ICLR 2026
ETHICS STATEMENT
The research work presented in this paper adheres strictly to the ICLR Code of Ethics. This study does involve human subjects, and there no potential conflicts of interest or fairness concerns related to the work.
The Gaokao-Formal Benchmark introduced in this paper is derived from publicly available official statistics administered by government authorities. As pnvermment-manngee public information, the dataset free from private copyright restrictions. The models, code, and data released in this work are intended solely for academic and research purposes. They do not pose privacy or security risks and comply with legal and ethical standards.
We confirm that we have read and complied with the ICLR Code of Ethics.
REPRODUCIBILITY STATEMENT
To ensure the reproducibility of our research, we provide detailed information about our method- ology, datasets, and experimental setup. The source code for our project, including the implemen- tation of the MathesissAutoffrrmaiizer and the LeanScorer evaluation framework, is available at https:://s com/ -AT4Math S.MatthMatthes
The newly introduced Gaokao-Formal benchmark is described in Section 3.3 with further details and examples provided in Appendix C All experiments were conducted on this benchmark and the publicly available MiniF2F-test set. Our experimental setup. including the baselines used for comparison, evaluation metrics, and results, is detailed in Section 4
The training configurations and hyperparameters for the Mathesis-Autoffrmallis Appendix [A] This includes details on the Group Relative Policy Optimization (GRPO) and Hier- archical Preference Optimization (HPO) stages. The prompts used for all language models in experiments, including the autoformalization prompts and the prompts for the M--as-a-Judge and LeanScorer frameworks, are available in Appendix E
provided in

---

Published as a conference paper at ICLR 2026
REFERENCES
Anthropic. The
Claude
model
family:
Opus,
Sonnet,
Haiku.
Model
Card, March 2024.
URL
com/
de wbt.c9aaccbbbbc3333ca3 3 3b80b 052.://00000088887777777766800
Claude_33 p.f
Zhangir Azerbayev. Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and
Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate--evel mathemat- ics. arXiv preprint urXiv:2302. 12433, 2023.
Lukas Biewald. Experiment tracking with weights and biases. https://wannd: ai 2020. URL
https: //www. wandb. com/ Software available from wandb.com.
Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, and Xin Shen. Proofflow: A dependency graph approach to faithful proof autoformalization. arXiv preprint arXiv:2510.159: 2025.
Garett Cunningham, Razvan C Bunescu, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with clementary proofs. arXiv preprint arXiv:2301.02//5, 2023.
DeepSeek-AI and Anonymous Contributors. DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning, 2025. URL httth:t//axxiii hwtp:////ppp./.......222.2 httppp///aaaa.....rar//////22..
Guoxiong Gao, Yutong Wang. Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald:
A natural language annotated lean 4 dataset. arXiv preprint arXiv:2410. 2024.
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Confer- ence on Learning Representations, 2025. URL https:://///// oppnrevveee / net. fest/forumme forum? d=
Se6MMCtRhz
Maarten Grootendorst. Bertopic: Neural topic modeling with class-based tf-idf procedure. arXiv preprint arXiv:2203.05794, 2022.
Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. LoRA: Low-rank adaptation of large language models. In International net.
Conference on Learning Representations (ICLR), 2022. URL Forum? Barrum?d=nZZeeire d=eeekeeeeeee
Gérard Huet, Gilles Kahn, and Christine Paulin- Meulin-Mohring. The coq proof assistant tutorial. Rapport Technique, 178: 13, 1997.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. 12283, 2022.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.0377 2023.
Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuan- prover: A scalable data synthesis framework and guided tree search for automated theorem prov- ing, arXiv preprint arXiv:2412.2073: 2024.
Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. Mps- prover: Advancing stepwise theorem proving by multi multi-perspective search and data curation. arXiv preprint arXiv:2505. 10962, 2025.
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 25020:2500.076400 2025.
Chengwu Liu, Jianhao Shen, Huajian Xin. Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint 24994555 2023.
12

---

Published as a conference paper at ICLR 2026
Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and Andrew C Yao. Efficient neural theorem proving via fine-grained proof structure analysis. arXiv preprint arXiv:2501.18310, 2025a.
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. arXiv preprint urXiv:2502.0556; 2025b.
Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In International Con- ference on Learning Representations (ICLR), 2019. URL lntts:///penreview..co
Forum?id-Bkg6Rin
Jianqiao Lu, Yingja Wan, Yinya Huang. Jing Xiong, Zhengying Liu, and Zhijiang Guo. Formalalign: Automated alignment evaluation for autoformalization. arXiv preprint arXiv:2410.001 2024a.
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. Process-driven autoformalization lean arXiv preprint arXiv:2406.0109 2024b.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL '20 ACM, January 2020. doi: htRphtt:: dxx doi. org/10 /0. 141444533222 337222888333333888 3373824
00.1144//372885.3333888
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language.
In Automated Reduction-CADI 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. Training language models to fol- low instructions with human feedback. Advances in neural information processing systems, 35:
27744, 2022.
Junshu Pan, Wei Shen, Shulin Huang, Qiji Zhou, and Yue Zhang. Pre-dpo: Improving data utilization in direct preference optimization using a guiding reference model. arXiv preprint arXiv:2504.15843, 2025.
Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization. arXiv preprint S1I::2310000957, 2023.
Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994.
Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, al. Criticlean: Critic-guided reinforcement learning for mathematical formalization. arXiv preprint arXiv:2507.0618), 2025.
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222. 2024.
Rafacl Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly a reward model. Advances in Neural Information Processing Systems, 36:53728-53742 2023.
ZZ Ren. Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, al. soning via reinforcement learning for subgoal decomposition. arXiv preprint 1rXiv:2504.21801, 2025.
Advancing formal mathematical rea-
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y.K. Li, Y. Wu, and Daya Guo. Deepscekmath: Pushing the limits of mathe- matical reasoning in open language models, 2024. URLhttps:
org/ abs hbbs/2402
03300v3
Michio Sugeno. Theory of fuzzy integrals and its applications. Doctoral Thesis, Tokyo Institute of Technology, 1974.
13

---

Published as a conference paper at ICLR 2026
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. arXiv preprint arXiv:2407.11214 2024.
Songjun Tu, Jiahao Lin, Xiangyu Tian, Qichao Zhang, Linjing Li, Yuqian Fu, Nan Xu, Wei He, Xi- angyuan Lan, Dongmei Jiang, et al. Enhancing IIm reasoning with iterative dpo: A comprehensive empirical investigation. arXiv preprint arXiv: 2503. 220055122000 12854, 2025.
Leandro von Werra, Lewis Schmid, Thomas Wolf, and Lewis Tunstall. Trl: Transformer reinforce- ment learning. https:: /ttp:s:///gie /ttgtttttt//t////t www wwwp.//wwwwwggg....oo/oo.ooo/e/e 2t0-0e/200020222022442220 2020-2024.
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint vrXiv:2310.000 0.00056, 2023.
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.11344 2025.
Tianduo Wang, Shichen Li, and Wei Lu. Self-training with direct preference optimization improves chain-of-thought reasoning. arXiv preprint urXiv:2407. 18248, 2024.
Jonata Wieczynski, Giancarlo Lucca, Eduardo Borges, Asier Urio-Larrea, Carlos López Molina, Humberto Bustince, and Graçaliz Dimuro. Application of the sugeno integral in fuzzy rule-based classification. Applied Soft Computing, 167:112265, 2024.
Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Remi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gug- ger, Mariama Drame, Quentin Lhoest, and Alexander M. Rush. Transformers: State-of-the-Art natural language processing. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pp. 38-45, Online, October 2020. As- sociation for Computational Linguistics. URL https: http:://wwwwww /www.www.mmmmmmm/...oo./.. aclweb. wwtggnthogoggy////ooooooooooo/tt
2020. emn -emmnn.pppss......mmmmmmmmmmm..m
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Informa- tion Processing Systems, 35:32353-32368 2022.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-provent for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024.
5: Harnessing proof assistant feedback
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for Ilm-based automatic theorem proving. arXiv preprint arXiv:2502.0324 033488,,, 2025.
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AT. In Proceedings of the International Conference on Machine Learning, 2025a.
Xiao-Wer Yang, Zhi Zhou, Haiming Wang, Aoxue Li, Wen-Da Wei, Hui Jin, Zhenguo Li, and Yu- Feng Li. Carts: Advancing neural theorem proving with diversified tactic calibration and bias- resistant tree search. The Thirteenth International Conference on Learning Representations, 2025b.
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, arXiv preprint arXiv:2406.03847, 2024.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demon- stration learning for formal theorem proving. arXiv preprini arXiv:2305. N.Xiv:335./66366 2023.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematies. arXiv preprint arXiv:2109.000 10, 2021.
14

---

Published as a conference paper at ICLR 2026
APPENDIX
A TRAINING DETAILS FOR Mathesis-Autfoormaliie
The training of our Mathesis-Auutofrrmaiizze model, which employs Group Relative Policy Op- timization (GRPO), involves several key hyperparameters and implementation choices as briefly mentioned in Section 3.1 The policy Ta initialized from Kimina-Autoformalinn
(Wang al. TaneiTuning (PEFT) via Low-Rank Adaptation (LoRA) (Hu
2025). We employ Parameter-Efficienn al. 2022), configured with a rank 16 and a 32. LoRA is applied the attention projection lavers of the base model. The optimization is performed using the Adam W optimizer (Loshchilov & Hutter 2019) with a learning rate of 10 and gradient checkpointing manage memory
usage.
For the GRPO algorithm itself, we sample language problem x. The Kullback- (KL) divergence coefficient B, which regularizes the policy updates against the reference SFT policy, is set 0.04. The policy model Ta updated once sampling/exploration phase (i.e., = 1, meaning updates occur after each group of G genera- tions for a given input æ processed and rewarded). To enhance efficiency, reward computations (syntactic verification via Lean and semantic assessment) parallelized using Python's 's asyncio library. The overall training pipeline is managed using the Hugging Face trans formers (Wolf) al. 2020) and trl (von Werra et al. 2020-2024) libraries. Experiment progress and results logged using Weights & Biases (Biewald 2020).
14 candidate formal statements per input natural
B DATA DEDUPLICATION AND CONTAMINATION ANALYSIS
To ensure that the performance gains reported this paper reflect genuine reasoning capabilitiess rather than memorization, we conducted rigorous data contamination analysis. This section details our methodology and presents the overlap statistics our main evaluation benchmark, GAOKAO- FORMAL, as well as standard benchmarks MiniF2F and PutnamBench against our three primary training data sources: the In-house Gaokao Corpus (Combined), Goedel P-Set, and Lean Workbook.
B. METHODOLOGY
We implemented strict lexical overlap detection pipeline to audit potential data leakage. The process consists of the following steps:
1. Normalization: All text data from both training and evaluation sets was normalized using NFKC normalization, converted to lowercase, and had whitespace collapsed.
2. N-gram Extraction: We extracted all 50-character substrings (windows) starting at word boundaries from the evaluation benchmarks.
3. Matching: An Aho-Corasick automaton was constructed to stream the training corpora and detect matches efficiently.
For each problem statement in the evaluation set, we calculated an overlap ratio n) defined as:
matched windows
V/
(3)
total windows
Based on this ratio, problems were categorized into three levels of contamination:
Clean: γ) < 0.2 (Less than 20% overlap)
Suspicious: 0.2 S 7/- < 0.8 (Between 20% and 80% overlap)
Dirty: n 2 0.8 (Greater than 80% overlap, indicating nepr-dupli
B.2 RESULTS
We performed the analysis for GAOKAO-FORMAL, MiniF2F-test, and PutnamBench against three distinct training subsets.
15

---

Published as a conference paper at ICLR 2026
Analysis 1: Overlap against In-house Gaokao Corpus. Table 4 shows the contamination rates against our primary In-house Gaokao training corpus (Combined English Informal). GAOKAO- FORMAL shows negligible overlap (1.2% suspicious, 0% dirty). Similarly, MiniF2F and Putnam- Bench are entirely clean relative to this training source.
Table 4: Contamination Analysis against In-house Gaokao Corpus (Combined)
Evaluation Set
Total Entries
Clean (< 0.2)
Suspicious (00.2.08))
Dirty (2 0.8)
Gaokao-Formal
495
489 (98.8%)
6 (1.2%)
0 (0.0 %
MiniF2F
488
488 (100%)
(0.0%)
0 (0.0%
PutnamBench
661
661 (100%)
(0.0%)
0 (0.0 %
Analysis 2: Overlap against Goedel P-Set. Table 5 presents the results against the Goedel P-
Set. While GAOKAO-FORMAL remains robust with zero dirty matches, existing benchmarks show significant contamination. Specifically, MiniF22 contains 31 dirty proof' (6.4%) and PutnamBench contains 41 dirty proofs (6.2%), suggesting that models trained on the P-Set may memorize solutions for these standard benchmarks.
Table 5: Contamination Analysis against Goedel P-Set
Evaluation Set
Total Entries
Clean (< 0.2)
Suspicious (0.22,08))
Dirty (2 0.8)
Gaokao-Formal
495
479 (96.8%)
16 (3.2%)
0 (0.0%)
MiniF2F
488
372 (76.2%)
85 (17,4%)
31 (6.4%)
PutnamBench
661
433 (65.5%)
187 (28.3%)
41 (6.2%)
Analysis 3: Overlap against Lean Workbook. Table 6 displays the overlap against the Lean Workbook dataset. All three evaluation benchmarks are virtually free of contamination from this source, with GAOKAO-FORMAL showing 100% clean entries.
Table 6: Contamination Analysis against Lean Workbook
Evaluation
Total Entries
Clean (< 0.2)
Suspicious ((..2,08))
Dirty (2 0.8)
Gaokao-Formal 495
495 (100%)
0 (0.0%)
0 (0.0 %
MiniF2F
488
486 (99.6%)
(0.4%)
0 (0.0 %
PutnamBench 661
660 (99.8%)
1 (0.25)
0 (0.0 %
In conclusion, our analysis confirms that GAOKAO-FORMIA is not contaminated by any of the training datasets used this work. Furthermore, the detection of "Dirty" samples in MiniF2F and PutnamBench against the Goedel P-Set highlights the importance of using fresh, uncontaminated benchmarks like GAOKAO-FORMAL to accurately assess generalization in formal theorem proving.
B.3 CONTAMINATION ANALYSIS AGAINST PRETRAINING CORPORA
To further ensure that the performance Gaokao-Formal reflects genuine reasoning capabilities rather than memorization of pretraining data, we conducted an extensive contamination analysis against major open-source pretraining corpora. Specifically, we checked for N-gram overlap against The Pile (Pilc-train), DCLM- -CLM-baseline, and five snapshots of CommonCrawi (CC-2025-05 through CC-2025-21).
(CC-22200055
As shown in Table 7 Gaokao-Formal exhibits 0.0% "Dirty" matches (defined as 2 80% 50-char N- gram overlap) across all evaluated pretraining datasets. This confirms that the benchmark problems were not seen during the pretraining phase of standard base models.
C DETAILS OF GAOKAO-FORMAL BENCHMARK
Problem-Type Diversity Unlike benchmarks that may filter out problem types with less devel- oped theorem libraries (e.g., geometry, c.mbinatorics), Gaokao-Formal includes all such problems
16

---

Published as a conference paper at ICLR 2026
Benchmark
Pile-train Dirty (%)
DCLM-base
CC-25-05
CC-25-08
CC-25-13
CC-25-18
CC-25-21
Diny (%)
Diryy (%)
Dirty (%)
Dirty (%)
Dinyy (%)
Dirty (%)
Gaokao-Formal
0.0
0,0
0.0
0.0
0.0
0.0
0.0
Reference Benchmarks:
ATME 2025 AMC 2023
0.0
0.0
0.0
0.0
0.0
N/A
N/A
0.0
0.0
0.0
0.0
0.0
0.0 N/A
0.0
TruthfulQA
0.1
0.1
1.0
N/A
N/A
N/A
Table 7: Contamination analysis of Gaokao-Formal against massive pretraining corpora. "Dirty" indicates the percentage of samples with 80% overlap. Dash (-) indicates no data available for that snapshot. Gaokao-Formal remains entirely clean across all sources.
MiniF2F
NL: If and are positive integers for which 2"3" = 1296, prove that r + y 8. y 1296): y= by sorry
FL: theorem. amc12b. 2004 p3 yx:: N) (hu
Gaokao-Formal
NL: Let m a positive integer, and let (1, 02 ... 04m+2 be an arithmetic sequence with a non- zero common difference. If two terms and (i < j) are removed from the sequence such that the remaining 4m terms be evenly divided into groups, and each group of 4 numbers forms arithmetic sequence, then the sequence di "2.".. ..4m+2 is called an seppaable sequence. For m 2 3. prove that the sequence 41, #2,... 44m-2 (2, 13) separable sequence. (m: (hm S m) (a: N - R) (ha: 3 (d:R), d # ( (sep: (N N) + Prop) (h.sep: A (ijN), (i> I M). (h:N), (h A 4 4 h h
FL: thecrem, gaokaoformal
(n:N), (n> A < 4* + (m+])=
iij A m + sep (f: (h:
(fh 2 1
S m)) A (V (g:),, let
fh= g);
gg 2 1 A á m) > (Nat.crr S =4 A (p - SV SY
2
A A
k & + pk pl) (3 R)) & (kN), (K2 TAA 5 (k+))))))==a=))aa))))))))>)))))= (')))) m 2
sep (2.13) by somr
Figure Comparison of the complexity of the problems in MiniF2F v.s. Gaokao-Formal
as they appear in the Gaokao exams. This encourages broader model capabilities and contributes to expansion Lean Mathlib (mathlib Community 2020
Autoformalization Complexity Many existing benchmarks simplify exclude problems where the primary challenge lies in the formalization. Gaokao-Forni retains these, especially in its "com- prehensive questions" category, which features problems with multi-domain concepts, novel defini- tions within question, or complex linguistic structures, thereby rigorously testing LLM abstraction capabilities. We provide an example of this kind of question, comparing with one MiniF2F ques- tion in Figure
Remark on Copyright Status: The Gaokao dataset utilized in this study consists of publicly available official statistics, administered by government authorities. It is classified as government- managed public information and does not involve privately copyrighted material.
D AGGREGATION DESIGN AND SENSITIVITY ANALYSIS OF THE LEANSCORER
D.1 EVALUATION AND ABLATION OF AGGREGATION METHODS FOR LEANSCORER
To demonstrate the superiority of our Sugeno integral- based scoring framework, we conduct com- prehensive ablation studies comparing our design against four alternative aggregation strategies:
Binary Aggregation: A strict one-vote-veto scheme, where the presence of any minor or major inconsistency results in a score of 0, and only all-M1 evaluations receive score of 1.0:
S(L) = 0
31, E (M'5, MO}
otherwise
17

---

Published as a conference paper at ICLR 2026
Precsson Compaation
Recel Compurtsnn
Store Corpaation
Accoricy Compariane
Figure 6: Performance comparison of aggregation methods Sugeno, Binary, Uniform, Geometric, and OWA across thresholds ranging from 0.1 to 1.0.
Table Comparison of aggregation methods, reporting best threshold, Precision, Recall, F1, Accu- racy, and Average Accuracy (# standard deviation)
Methods
Best Threshold
Precision
Recall
Fl
Accuracy
Average Acc
Sugeno (ours)
0.6
0.94
0.89
0.92
0.91
0,85(+10.046
Binary
N/A
0.97
0.6
0.74
0.77
0.77 0.0)
Uniform
0.8
0.94
0.89
0.92
0.91
0.72(# 0.117)
Geometric
0.6
0.89
0.89
0.89
0.87
0.82 (# 0.069)
OWA
0.9
0.91
0.89
0.90
0.89
0.66 (# 0.105)
Uniform Averaging:
A straightforward arithmetic mean that assigns equal weight to all subtask
evaluations:
S( _
Σ f(4)
with the mapping function f(MI) 1.0, (M 0.5, and f(M0)
Geometric Mean: An aggregation method more sensitive to low scores, computing the geometric mean of all evaluation scores. To avoid zero product, MO is mapped to 0.01.
1/n
Y2
S(L.f)
II
f())
with the mapping function f(MI) 1.0, f(M/) = 0.5, and f(M0) 0.01.
Ordered Weighted Averaging (OWA): A position-weighted approach that emphasizes higher- ranked evaluations, with weights decreasing linearly. Here, we adopt a descending order (((x1)) Z
(((()))) 2 ... 2 f(la(n)):
S(L f)
Σ wi f(1(())
where w; = n-i+l Σ5-13" D w; = 1, and the mapping function is f(M1) 1.0, f(M/2) 0.5. and
(M0) = 0.
Figure 6 presents the performance curves of all scoring methods across thresholds ranging from 0.1 to 1.0, while Table & summarizes each method's optimal performance and stability, reporting both mean and standard deviation of accuracy across thresholds. Our Sugeno integral achieves the best overall performance, with an Fl score of 0.92 and accuracy of 0.91 11 at the threshold of 0.6. also exhibits the highest mean accuracy and the lowest standard deviation, highlighting both its effectiveness and robustness.
Among the methods, the Binary method achieves the highest precision of 0.97 but suffers from very low recall of 0.6, which reduces its Fl score to 0.74. The Uniform averaging method attains a competitive the threshold, reflected by mean accuracy of 0.72 and standard deviation of 0.117, which, in contrast to the more stable performance the Sugeno method (accuracy mean = 0.85, std 0.046). The Geometric mean demonstrates moderate stability but does not surpass the Sugeno integral in
score of 0.92 and accuracy of 0.91, but its performance varies substantially with
18

---

Published as a conference paper at ICLR 2026
the best Fl accuracy, whereas OWA achieves strong Fl and accuracy the optimal threshold but exhibits the poorest stability, with mean accuracy of 0.66 and a standard deviation of 0. 00105.
Our gigeno-based aggregation method offers two key advantages: First, it provides strong balance by maintaining consistently high precision 0.94 and recall of 0.89. It avoids the over-rejection characteristic of Binary aggregation and achieves the best F1 and accuracy among all methods, reaching 0.92 and 0.91, respectively. Second, it demonstrates robustness and operational flexibility. The method attains the highest mean accuracy of 0.85 and the lowest standard deviation of 0.046, highlighting its superior stability relative to all baselines. Moreover, as illustrated in Figure 6, remains effective across wide threshold range from 0.1 0.7, enabling flexible threshold selection and reducing the need for extensive tuning during deployment.
D.2 SENSITIVITY ANALYSIS OF LEANSCORER
We conduct sensitivity analysis assess the impact of the evaluation mapping value for partially correct subtasks, f(M1/), on semantic correctness checking performance. As shown in Table 9
{0.1, 0.2, ..., 0.9). while keeping f(M1) observe that the F1 score remains stable at 0.92 for f (M1/2 values in the range [0.1. 0.5], indicating
we vary (M1/2
1.0 and f(M0) 0 fixed. We
robustness to the exact scaling of partial credit. As the value increases beyond 0.5, the score
shows a slight degradation, dropping to 0.88 when f(M1/) E [0.6, 0.9). These results suggest that
our metric is relatively robust to the choice partial reward, we set (MM/2 = 0.5 in all experiments.
Table 9: Sensitivity of F1 Score to the Value of (MV/)
((M2)
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
0.9
Fl Score
0.92
0.92
0.92
0.92
0.92
0.88
0.88
0.88
0.88
The robustness of LeanScore to the value of ((MV/) arises from two factors. First, its max-min ag- gregation over sorted prefix subsets means small changes to f(M//) rarely affect which subset yields the maximum, unless the changes significantly alter the ordering. Second, the fuzzy measure uss) assigns zero to any set containing an MO label, making LeanScore more sensitive to fully incorrect outputs than partial ones. Nevertheless, the partial credit remains critical by distinguishing M1/2 from MO, LeanScore captures finer-grae meer-grained differences in output quality, especially in borderline cases, which would otherwise be treated the same if both were mapped to O.
We also conduct sensitivity analysis on the parameter 5 used fuzzy measure jus), and observe that the F1 score is not sensitive to the choice of 8.
E PROMPT TEMPLATES
Prompt for Autoformalization (used by all baseline models except Herald)
You ure an expert in formal mathermaticx. Your task is to translate the given natural language mathematical stalement into a formal Leun thentem.
[Natural language statement]:
[statement]
Please convert this statement into precise firrnal Lean 4 theorem, Follow these guidelines:
1. Start with cheorem followed by unique
the provided ID available
2. Define the types of all variables (e.g.. : IR for real numbers)
3. Use uppropriate mathematical symbols and notation
4. End with == by sorry to indicate the proof will he completed later
Your formalization must exactly capture mathematical meaning the statement
Formal Lean theorem:
19

---

Published as a conference paper at ICLR 2026
Prompt for LLM--as-a-Judee Semantic Check
You will receive natural language math problem statement, along with its formal statement in LEAN 4 and, in some cases, a description mathematical teross Please evaluate whether formal LEAN statement appropriately translates natural language stateneeut based the following criteria. They considered diflerent any the criteria not satislied.
Key Elements: The fundamental mathematical components, including variables, correctly represented in LEAN code.
operations, domain, codomain
2. Mathematical Accuracy: The mathomatical relationships and expreasions should be interpreted consistently during translation.
3. Structural Fidelity: The translation aligns closely with the original problem, maintaining its sinacture and purpose.
conditions, constraints, and objectives stared in the natural language statement are mathemarically cluded in the LEAN translation.
Comprehensivenes:
When doing evaluation, break down each problem Think stop-by-stpp and explain all of your reasonings. Your answer should be in the following formar: Thought:
into components, match components, and evaluate their equivalence.
[Your Anawer]
Judgement:
[Your Answer,
of (Appropriate, Inappropriate))
Prompt for Subtask Decomposition in LeanScorer
Help me conditions conclusions problem (using specific mathemarical formulas), without solving
Here is example:
[Problem]: The sequence (a, satislies 41 1, ag 2, Gn42 20 an + 2. Let b.. aut1 au. Prove that (bn, } arithmetic sequence.
[Conditions and Conclusions]:
Conditions:
1.
=
3. Vn 2 1,,, 2a,+1
on +
4. vn 2 1,b, Op+1
Conclusion:
{b..} } is an arithmetic sequence, i.c., E R, Vn 1, 1,b bn
Now. please help extract conditions without solving it:
problem in way (using specific mathenatical formulas),
[Problem]:
{informal statement)
[Conditions and Conclusions):
Prompt for LLM- based Evaluation in LeanScorer
Here math question and Ican statement. Compare the conditions and conclusions in this code with mathematical ones. matching them one by one to see if the formal statement is un appropriate trunslation of the mathematical condition by assigning one three tags (Match: Minor inconsistency: Major inconsisteacy). Then, audit missing/implicit conditions. Judge with extremely strict standards any minor inconsistency will considered mismatch. Special attention triangle angle-side comespondence. If the question explicilly mentions apposite angles/ /////dds.. this comespondence must be clearly siated and currect. Stop immediately after evaluating all pairs. Do not sammarize analyze further. Output Format:
Lone-sbot example]
Question:
finlermal statemennt
Mathematical conditions and conclusions:
(math conditions)
Lean 4 formal statement:
[Tormal statement] }
Output:
One-shot Example for LeanScorer I.LM-based Evaluation
Let's compare mathematical conditions and conclusions with the Lean formal statement one: is natural number greater than I:
q E N. g...3.
Lean: (hg 1
Match: Match
n is a natural number greater than
Math: N. 1.
Leaa:: (hn 1 nl.
20

---

Published as a conference paper at ICLR 2026
Match: Match
M 1,2.....4
Math: M is explicitly defined this
Lean: Finset N Finset. range
Detailed interpretation: honset.range. q (0, 1, 1}.
Match: Match
Set A definition:
Math: A = {ar == E. =igiT" E M.
Lean:
Set :- (x ix.vec : N N), Finset. raage
x voc/1 1)
1).
Detailed interpectation: In Lean, x.vec is indexed from to (since 1 1 ranges from to :)) but the math defines ai 2, ..... function on all naturals, but only using x.vec (1 13 for i in Finget, rrange n). The Lean definition is technically correct slightly more
actually comisteet,
representation slightly more general (allowing x.rec
the However, captures
Match: Minor inconsistency
with specific expansions:
Math: DT a.g" 1. 2 big' 3. with a, b, E M.
Lean: Σ 1 in Finsar. range n, (1 + 11
Σ Pinset. range n,
with 2, E B and 1, b
Detailed interpretation: The Lean version uses (1 11 and (1 1) to match indexing sum, which is equivalent math but slightly indirect. evaluates at 1. The Lean version is currect but not literal translation.
directly uses 1, - while Lean for all but only
Match: Minor inconsistency
6. < bu:
Math: < bn.
Lean: (hab a nl.
Match: Match
Conclusion
Math:
Lean:
<=
Match: Major inconsistency
Check for missing conditions/ 'imlicit conditions:
No missing conditions / implicit conditions
Match: Match
F
CASE STUDY
F.1 SAMPLE LEAN4 PROOF CODE WITH APPLY? THAT CAN PASS LEAN VERIFIER
We observe that a small number of LLM-generated proofs contain artifact-inducing tactics such as apply?, phenomenon also noted in proofs generated by provers proposed in prior work (Ren al. 2025). These tactics may occasionally yield Lean-accepted proofs without providing valid proof strategy, thereby risking inflation of reported pass rates.
To prevent artifact-induced proof's from inflating pass rates, in our experiments, every generated proof undergoes post- verification filtering. After Lean kernel verification, we re-parse the proof and inspect for artifact-inducing tactics such as apply?. Any proof containing such tactics is discarded. Only proofs that both verify under the Lean kernel and contain no artifacts are counted as successful.
import Macalib
Import Aesop aet_option maxleartbeats
21

---

Published as a conference paper at ICLR 2026
open sigopezators Real Nat 'Topology
Prove that the number Siaum n_ @1hinom(2n+11 [2k+1 )2 [3x] is not divisible by 955 any integer Sn\gee,$5/
theorem imo_1979_ (n Ni
Σ Finset.
11, Nac.choose
intro h.
have h
rw [Nat.dva_ ffff_mod__de mond_eg_aarrr at h
have : ( k Finset.
1), Nat.choose
k)) & = 0 by
sun modulo never by examining the terms their have 12 in ranget. ta 11, Nat. choose (2 + n (2
contsibutions.
k)) 1
Tala 18 placeholder der for the actual proot, which would involve detailed combinatorial arguments.
IW [+- war.iini..attastt..t... nattast_iaj]
apply?
emega
F.2 SAMPLE LEAN4 PROOF CODE WITH TRUE THAT CAN PASS LEAN VERIFIER
The statement "True" represents tautology that lacks meaningful logical content for formal ver- ification purposes. This formulation is problematic because it evaluates to true regardless of the truth value of any preceding hypothesis-both "False True" and "True True" yield true under standard logical implication. Consequently, this creates a degenerate proof scenario where success- ful verification provides substantive evidence regarding the validity of the original hypothesis. Even when the underlying mathematical claim is incorrect, the proof system will indicate success, rendering the formalization unsuitable for rigorous mathematical verification and undermining the epistemic value of the formal proof process. Any statement containing such a proof goal is discarded and considered as failed.
import Kathlib
import Aesop
set_option maxleartbeats
open Big0perators Real Nat Topology Rat
/-Let $E (x) se (x] (a\Min 8)S, Sx\Min RS. It is known that the function Sy E (x)
has inareases as $aš decreasas.-1 question
$x_18, $x_28, with $x_1 x_29. Frove that @V\fran(x_2 2x
R
x)
(81 X2 R + 31 1881 V 8, a (81 a) - 0) (ax2 V a.
[ (82 st - 01
a, X1 22 (:2
X1 X2
True
G QUALITY ASSESSMENT OF GAOKAO-FORMAL BENCHMARK ANNOTATIONS
This section documents the annotation protocol and quality-control procedures used in constructing the Luman-verifiee subset of the Forkma dataset.
Annotator Expertise. The annotation team consists of three highly qualified domain experts: International Mathematical Olympiad (IMO) team member (Annotator 1) and two Lean formaliza- tion specialists (Annotator 2-3) from QS Top-10 mathematics departments. All annotators have extensive experience in both competitive mathematics and formal theorem proving.
Inter-Annotator Agreement. To assess annotation reliability, we conducted an agreement study on the subset evaluated in Section 4.1, comprising 98 samples independently annotated by all three experts. The resulting statisties are:
Fleiss' Kappa: 0.7545
22

---

Published as a conference paper at ICLR 2026
Perfect three- way agreement: 81.63% (80/98 samples)
Pairwise agreement rates;
Annotator vs 2: 92.86%
Annotator 1 vs 3: 83.67%
Annotator 2 vs 3: 86.73%
Disagreement Resolution Protocol. For the 18 samples (18.37%) with initial disagreement, consensus-based review process was employed. The three annotators jointly reviewed the natural- language problem, the proposed Lean formalization, and the underlying mathematical reasoning. Discussions continued until unanimous agreement was achieved for each case.
Subset Construction. The 98 98-problem subset used for semantic evaluation in Section 4.1 was constructed by randomly sampling natural-language questions from the complete Gaokao-Formal dataset and generating corresponding formal statements using LLM autoformalizer (Herald- Autoformalizer). All formalizations were then labeled according to the above protocol. The per- formance metrics reported in Section 4.1 (i.e., Precision, Recall, F1) are computed on this expert- validated subset.
H QUALITY EVALUATION OF AUTOFORMALIZER OUTPUT BEFORE AND AFTER DPO
In this section, we investigate whether the improvements in provability observed after DPO train- ing result from generating semantically aligned, prover-friendly formalizations or from producing weakened statements that simplify the original problems. We evaluate this question through three complementary analyses: human expert assessment of formalization quality, prover-based difficulty analysis, and qualitative case studies. Our findings show that the gains stem from the generation of more aligned, frover-friendl formalizations rather than by any weakening of the original mathe- matical content.
Table 10: Human evaluation of the quality of formalizers before and after the DPO training
Dataset
Before DPO
After DPO
Gaokao-Formal
70% (35/50) correct
78% (39/50) correct
MiniF2F
90% (45/50) correct 92% (46/50) correct
Human Expert Evaluation We randomly selected 100 problems (50 from Gaokao-Formal and 50 from MiniF2F) that passed LeanScorer validation. A panel of Lean experts conducted a blind evaluation of semantic correctness for formalizations generated before and after DPO. Experts were instructed to mark a statement as incorrect if the autoformalizer produced a weakened statement that did not preserve the original problem's difficulty semantic meaning. Results shown in Table TO After DPO, correctness on Gaokao-Foo Forrzal rises from 70% to 78%, and on MiniF2F from 90% to 92%. These results indicate that DPO improves semantic correctness without weakening statements or introducing incorrect semantic content. The findings are consistent with the LC+LSC improvements reported in Table where DPO raises LC+LSSC from 67% 71 % Gaokao-Formal and from 25% to 30% on Putnam.
Table 11: Average proof length by provers of statements generated before and after DPO training
Dataset
Before DPO
After DPO
Gaokao-Formal 31.26
33.40 25.44
MiniF2F
24.97
Prover-Based Difficulty Analysis Assessing the difficulty of formal statement is inherently hard because difficulty cannot be determined reliably from the statement alone. A reasonable proxy is to measure how hard it is for prover to solve the problem. To this end, compute the average proof
23

---

Published as a conference paper at ICLR 2026
Table 12: Statement cases generated before and after DPO training
Natural Language Statement
Model
Formal Statement
Factory A produces certain product at
Before DPO
Tharpse profte (ei Ry (bo yow 183 (e 13 the y (a
constant rate of kg/hour
(production condition requires
1 I S 10), and the profit obtainable per hour is 100(5x + _) yuan. Prove that the profit obtained from producing kg of this product 150a(5 + )
Pass Rate: 0/32
After DPO
question_999985
Ob 1 X.X.A.XX
(b 0.0.0. 8...c. (sroft: B
(ts prufit Fun 100 + 2
profit
Pass Rate: 28/32
Given that the line intersects ellipse C: x² + 2² = at two distinct points P(21,3) 3/1 and (x2 322), and the area of 4OPQ Q SAOPQ 2
Before DPO
2. dh the a (eig C
Pass Rate: 0/32
where O is the origin. Prove that vf + . and yf + y/2 are both constants.
After DPO
theorse question 428217
2
(h. Xt (6]
01. : ys y-)
0he (a 7:3) x abe (#) My yo Beal 6
C Xr22 xy"2 G. yo yy
Pass Rate: 14/32
theo distance 052201 (a On M Sot (P2n N))
Given the set Sn = (X
Before DPO
the k, 1 e Eimettnerre 212 (A (Hir +30 (M) M.cck
(I1, 22, )n), I. (0, 1),
1,2, n (where 2 2).
(a1,02,"
02. ... ,.n)
B = (bi, b2. bn) Sn. the
(4 s3a
MM:39 6ab-
x snA ((A 1 1
difference hetween A and B is defined A
4 06 -0 484
Pass Rate: 0/32
(la: - 611, - b2/.-... lan bnl);
the distance between A and B is
After DPO
theores qussttor_449977
defined as d(A, B) = E
2i=1 |a: bul-
(A ABC. F
Prove that AA, B, C E Sn.
(he :
A-BE Sn, and
(6, 1 A. A1 A0
d(A C, = d(A, B).
(6 ln:vi,
Ei [4.1
--1--
Pass Rate: 19/32
length, measured as the number of tactics generated by DeepSeek Prover- with 128 sampled attempts per problem. Problems for which the prover finds successful proof are excluded. The metric defined as:
DeepSeck-Prover-V2 7B non-CoT mode
N
Avg Proof Length
Σ PEP.
length(p)
N
P.
where N is the number of problems and P; is the set of successful proofs for problem Ta- ble II shows that the average proof length increases after DPO training for both Gaokao-Formal and MiniF2F. This indicates that DPO does not lead the model to generate weakened or trivially solvable statements.
Case Study We provide case studies in Table 12 comparing formalizations generated by Mathesis before and after DPO (referred to "pre- DPO and "post-DPO" statements, respectively). All pre- DPO and DPS statements Table ar are all semantically equivalent to their natural language counterparts. Rather than generating weakened statements, the post-DPO model tends to generate
24

---

Published as a conference paper at ICLR 2026
more prover-friendly formalizations that easier for theorem provers to understand and prove. For each formal statement, we report the pass rate of proofs generated by the prover with a budget of 32 attempts. Detailed interpretations
follows:
The pre-DPO formalization unnecessarily employed integral calculus to compute total profit, introducing proof complexity where direct algebraic methods sufficed. The post-DPO version eliminated this computational overhead.
Case I:
Case 2: The pre-DPO statement relied on complex measure-theoretii constructs such as MeasureTheory, volume (convexHull R {P, 2}), whereas the post-DPO version directly applied geometric area formulas. This shift from abstract mathematical machinery concrete computational approaches significantly improved provability.
Case 3:
The pre-DPO version introduced excessive hypotheses and intricate definitions us- ing set notations that complicated proof unfolding. The post-DPO version streamlined both the hypothesis structure and definitional complexity, reducing the cognitive and computa- tional burden on theorem provers.
Overall, our human expert evaluation, prover-based difficulty analysis, and qualitative case stud- ies support that the DPO training performed enhances semantic alignment and generates more prover-friendly formalizations rather than causing a tendency toward weakened statements.
I THE USE OF LARGE LANGUAGE MODELS
Following ICLR guidelines, we wish to clarify our use of Large Language Models (LLMs). Note that the research ideas, methodology, and experimental design presented in this paper were developed entirely by the human authors.
LLMs used primarily in the following ways:
Model Training and Inference:
The core training process of the proposed model, as well as the experimental evaluations, involved utilizing it for inference.
Benchmark Data Generation: The English translation and formalized Lean 4 formal state- ment in the Gaokao-Formal benchmark released in this study was initially generated by LLM. These initial outputs were subsequently meticulously manually edited, verified, and rewritten by the authors ensure accuracy and quality.
We emphasize that the LLM was used solely as tool, and the authors take full responsibility for the entire content of the paper, including all data and text that was initially generated by the LLM and subsequently modified.
25


Reviews:
[{"review_id": "As8qAvh6XF", "reviewer": "Reviewer_UUGT", "summary": "The core contribution of this paper is (1) LeanScorer, a evaluation metric for semantic correctness in autoformalization and (2) training an autoformalization model using RL. The authors combined the autoformalization model with a formal theorem prover to prove statements in natural language.", "questions": "N/A", "limitations": "", "rating": 2, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "* Evaluating the semantic correctness of autoformalized statements is an important bottleneck in autoformalization. The paper proposed LeanScorer that aims to address this problem\n* This paper is one of the first to train autoformalization models with RL, which is nontrivial because of the difficulty in semantic evaluation.", "weaknesses": "* The task of \"formal theorem proving from natural language\" in this paper is not convincing. In this paper, it is defined as: Given a theorem statement in natural language, the model generates its formal statement and the corresponding formal proof. It is evaluated using proof accuracy (Fig. 4). This task definition does not evaluate whether the formalized statement is semantically correct. The model could formalize the natural language statement into a easier formal statement so that the proof accuracy will be higher. I understand that the authors have evaluated their autoformalizer, and experiments show improvements compared to existing autoformalizers under the LeanScorer metric defined in this paper (Table 3). However, that does not resolve this issue. It could be that the autoformalizer in this paper is indeed more accurate but is biased towards making statements easier, whereas previous autoformalzers are less accurate but are biased towards making statements harder. If true, this could explain the results in Fig. 4. \n\n*  The comparison between LeanScorer and LLM-as-a-Judge (Table 2) is inconclusive. LeanScorer has better precision whereas LLM-as-a-Judge has better recall. The F1 score is not a good metric because it assumes precision and recall are equally important. When evaluating autoformalized statements, however, precision is arguably less important than recall, as incorrectly translated statements can also be useful for training theorem provers. It would be great to compare LeanScorer and LLM-as-a-Judge in terms of their downstream impact to theorem proving.\n\n* Need ablation studies to justify the design of LeanScorer, e.g., why Sugeno Fuzzy Integral instead of simpler methods for computing the overall score.\n\n* MiniF2F is already saturated (SOTA methods are close to 100%). It would be great to add results on PutnamBench.", "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": "BSgzeRRPME", "reviewer": "Reviewer_brUb", "summary": "This paper addresses the important and challenging problem of formal theorem proving directly from natural language. The authors point out that current state-of-the-art automated theorem provers (ATPs) mostly require formal input pre-written by human experts, which limits their real-world applicability. To solve this, the paper proposes Mathesis, a complete pipeline driven by \"autoformalization.\" The core contributions of this work include: The first autoformalization model trained with Reinforcement Learning (RL), Mathesis-Autoformalizer, which innovatively combines syntactic, semantic, and prover feedback as reward signals; A novel semantic correctness evaluation framework, LeanScorer, for fine-grained assessment of formalized statements; A new, highly difficult benchmark dataset named Gaokao-Formal, containing 495 complex proof problems from China's National College Entrance Examination. Experimental results show that this method significantly outperforms existing techniques on multiple benchmarks and confirms the critical role of high-quality autoformalization in boosting the performance of downstream provers.", "questions": "1.\tIn the composite reward function for the GRPO stage, you perform a simple addition of the semantic reward $RsemR_{sem}Rsem​$ and the syntactic reward $RverR_{ver}Rver​$. This implies an assumption that they are equally important. Did you experiment with other aggregation methods, such as assigning different weights to them?\n2.\tCould you discuss whether the model has a potential tendency to generate weakened proofs?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "The combination of Reinforcement Learning with Hierarchical Preference Optimization (HPO) for the autoformalization task is the highlight of this paper. This approach enables dynamic learning from the feedback of a syntax checker, a semantic evaluator, and a downstream prover, significantly improving the quality of the formalized statements. The experimental results (e.g., a 45% relative improvement on Gaokao-Formal) fully demonstrate the effectiveness of this method.\n\nThe authors not only tested their method on two datasets with different difficulty levels and styles but also conducted extensive comparisons with a wide range of top-tier API models (including GPT-4o and Claude-3.5) and open-source models. More importantly, by pairing different autoformalizers with multiple mainstream provers, the paper clearly reveals the decisive impact of autoformalization quality on the final proof success rate.\n\nThe paper offers not just a model but a complete solution, including an innovative evaluation framework (LeanScorer) and a highly challenging new benchmark (Gaokao-Formal). These open-source resources will greatly facilitate subsequent development in the field.", "weaknesses": "The first is about the dependence of  LeanScorer on an LLM Evaluator. The core steps of LeanScorer (sub-task decomposition and consistency annotation) rely on an LLM. While experiments show high agreement with human annotators, this still introduces a potential source of noise, which to some extent undermines the credibility of the evaluation.\n\nThe second is that the paper uses downstream proof success as a metric may introduce bias. This could potentially lead the model to favor generating weakened versions of the statement and may weaken the credibility of the evaluation tests in section 4.3.", "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": "xGVxJjaN7D", "reviewer": "Reviewer_6WKD", "summary": "The paper introduces Mathesis, an end-to-end pipeline for formal theorem proving from natural language that centers on Mathesis-Autoformalizer (GRPO + DPO in a two-stage Hierarchical Preference Optimization), a semantic validation module LeanScorer (LLM-assisted subtask decomposition aggregated via a Sugeno fuzzy integral), and a new benchmark Gaokao-Formal (495 problems).", "questions": "1. Although LeanScorer improves semantic assessment, it may still produce erroneous judgments. What impact do these errors have on training stability or downstream performance?\n2. The appendix notes that “the policy model is initialized from Kimina-Autoformalizer”, but this important detail should appear in the main text for clarity and reproducibility.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Formal theorem proving is a highly active research domain, and the motivation for the proposed system is clear and compelling.\n2. The proposed methods are conceptually simple yet empirically effective.\n3. The introduction of Gaokao-Formal is valuable in this field.", "weaknesses": "1. The paper lacks an adequate quality assessment of the Gaokao-Formal dataset. Some details are missing, such as annotator expertise, inter-annotator agreement statistics, and the protocol for resolving disagreements. Moreover, the subset used in Section 4.1 is not described, making it difficult to interpret the reported F1 scores.\n2. LeanScorer introduces human priors and relies on additional compute (subtask decomposition → evaluation → aggregation) to produce higher scores. As such, it should be compared against other test-time scaling strategies, as well as alternative aggregation methods.", "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": "nEdBKNR23X", "reviewer": "Reviewer_UPch", "summary": "This paper proposes Mathesis, a pipeline for natural-language -> formal-statement -> Lean proof. The core components are: (i) Mathesis‑Autoformalizer, trained with online RL (GRPO) using a composite reward from Lean compilation (syntax) and an LLM-based semantic check, followed by a DPO stage aligned to downstream proof success (“Hierarchical Preference Optimization, HPO”); (ii) LeanScorer, an LLM-driven semantic evaluation with subtask decomposition and aggregation via the Sugeno fuzzy integral; and (iii) Gaokao‑Formal, a 495‑problem benchmark from Chinese college-entrance exams aimed at harder-to-formalize statements. On MiniF2F and Gaokao‑Formal, the autoformalizer improves pass rates in both autoformalization and theorem proving (paired with another prover model).", "questions": "1. How does Mathesis‑Autoformalizer compare to CriticLean [1] and FormaRL [2] when both are run under your evaluation?\n\n2. How does Gaokao‑Formal relate in difficulty and topic mix to miniF2F, PutnamBench, and ProofNet (e.g., cross‑benchmark transfer results or controlled difficulty calibration)?\n\n3. What safeguards ensure the reported Lean pass rates are not inflated by `apply?` /True/circular-goal artifacts?\n\n[1] Peng, Zhongyuan, et al. \"Criticlean: Critic-guided reinforcement learning for mathematical formalization.\" arXiv preprint arXiv:2507.06181 (2025).\n\n[2] Huang, Yanxing, et al. \"Formarl: Enhancing autoformalization with no labeled data.\" arXiv preprint arXiv:2508.18914 (2025).", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. End-to-end focus: Unlike the purely formal models like DeepSeek-Prover and datasets like MiniF2F and FIMO, this paper attempts end-to-end full NL input problem -> formal proof pipeline and shows that better formalization substantially boosts downstream proving across multiple provers. Also, Gaokao‑Formal intentionally targets hard-to-formalize statements and broad topics (e.g., analytic geometry, comprehensive questions), which is valuable given miniF2F’s focus. \n\n2. The composite syntax + semantics reward in GRPO followed by DPO aligned to proof success (HPO) is coherent; ablations show small but consistent gains. The autoformalizer attains higher LC and LC+LSC on both datasets than strong baselines like Kimina‑Autoformalizer, and improves pass@32 with multiple 7B prover models", "weaknesses": "1. Data deduplication / de-contamination: Sec. 3.1 states that training-data curation includes the in‑house Gaokao dataset plus Lean Workbook (yielding ~32k problems), and the main evaluation benchmark is also Gaokao‑Formal. Without explicit deduplication auditing (fuzzy NL/FL matching, near-duplicate detection, year‑wise splits), gains on Gaokao‑Formal may reflect domain adaptation or overlap. The paper should document dedup guarantees, overlap statistics, and controlled cross‑domain tests. Also, some of the problems are created before the knowledge cutoff data of the evaluated models, causing the data contamination issues. It would be nice to create a subset of uncontaminated examples for evaluation via temporal split.\n\n2. While LeanScorer is thoughtful, the main LC+LSC@k results overly rely on proposed LLM‑based scorer, raising concerns about metric coupling. Recent alternatives specifically targeting semantic alignment include FormalAlign [1]. The paper compares LeanScorer only to LLM-as-a-judge and re‑informalization rather than to these stronger contemporaries, which this limits external validity. \n\n[1] Lu, Jianqiao, et al. \"Formalalign: Automated alignment evaluation for autoformalization.\" arXiv preprint arXiv:2410.10135 (2024).", "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": "gEjdIQwby3", "reviewer": "Reviewer_NXS9", "summary": "The authors propose Mathesis, the first autoformalizer trained with online reinforcement learning. Mathesis tackles the problem setting of formal theorem proving directly from informal problem statements. It is trained with GRPO to maximize semantic and syntactic correctness, and DPO to increase provability of the resulting formalization. The authors also introduce the Gaokao-Formal dataset of problems and LeanScorer to evaluate autoformalization correctness.", "questions": "Is there any overlap between the data used for training (“the natural language informal statements of problems from a pset (Lin et al., 2025) and our in-house Gaokao dataset”) and the miniF2F-test and Gaokao-Formal datasets used for evaluation? Since both training and testing use a subset of Gaokao problems, is there a chance of contamination?\n\nWhat is Mathesis-Autoformalizer (without HPO) in Table 3? Is it the model after GRPO but before DPO training?\n\nLeanScorer breaks down the natural language statement into subtasks, and compares against corresponding parts in the formal statement. However, what happens if there is an extra part in the formal statement that does not correspond to any natural language? For example, there could be a nondegeneracy criterion (a denominator is nonzero), or the model could have made a mistake and added an unneeded formal criterion. Do these unmatched parts exist and are they ignored?\n\nThe fact that the base model is Kimina-Autoformalizer (and that its size is probably 7B) should be mentioned in the main text instead of the appendix. For example, this makes it easier to understand Table 3.\n\nThere could be some comparison between LeanScorer and BEq/BEq+ (Liu et al. 2024 https://openreview.net/forum?id=hUb2At2DsQ) which has been researched in recent work in training and evaluating autoformalizers (Poiroux et al., 2024; Wu et al., 2025 https://arxiv.org/abs/2508.04440). Comparing against BEq which requires ground-truth labels also better contextualizes this work. I would like to see a comparison to BEq or BEq+ in Table 2. Since Gaokao-Formal contains ground-truth formal statements, I would also like to see BEq scores in Table 3, if BEq turns out to be a good scorer.\n\nMinor suggestions:\n\n- Table 2: the precision score of 94 instead of 93 should be bolded.\n- Line 305: $e_{\\pi(i)}$ -> $l_{\\pi(i)}$.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "The paper uses online RL on the task of statement autoformalization for the first time, showing substantial gains upon the base model. It shows that GRPO with a syntactic check and LLM judge as reward can improve autoformalization.\n\nMoreover, it demonstrates with DPO training that training the model to generate statements that are provable by a downstream prover can improve the quality of autoformalization.\n\nThe authors also propose LeanScorer, a more complicated LLM judger than a binary label, which they demonstrate gives higher precision.\n\nI am also convinced that generating statements that are more easily proven is useful in the setting of end-to-end theorem proving (starting from an informal problem and ending with a formal proof), which is an interesting under-explored problem formulation that has many practical uses and overcomes the scarcity of expert-written formal statements.", "weaknesses": "I am not convinced by the complicated formulation of the Sugeno integral. The authors have not provided motivation to use the Sugeno integral, nor any explanation for the formula of $\\mu$ (line 295). For example, why not just use this score: $0$ if there is a label M0, and otherwise use $\\frac{n_{M1}}{|s|}$ as the score? Why choose the specific $\\delta$ value and $\\mu$ formula; is it to obtain a certain reward shape?\n\nAlso, it seems to me that the score $S$ is actually very simple:\n\n- If there is a label M0 in $L$, then $f(l_{\\pi(1)})=0$ so $\\mu(s_i)=0$ for all $i$, so the score is $0$.\n- Otherwise, sort the labels to $n_1$ labels of M½ and $n-n_1$ labels of M1. Then for $1 \\le i \\le n_1$, $\\mu(s_i)=0$ because $n_{M1}=0$. For $i>n_1$, for the set $s_i$, $n_{M1/2}$ is fixed and $\\frac{n_{M1}}{|s_i|} = \\frac{i-n_1}{i}$ increases as $i$ increases, while $f(l_{\\pi(i)}) = 1$, so the maximum on line 295 is always taken at $i=n$. Therefore the formula on line 295 simplifies to $S(L,f,\\mu) = \\frac{n-n_1}{n}(1-\\delta n_1)$.\n\nI concede that I am not familiar with Sugeno integral, and I could have misunderstood some details. I would be happy to dismiss this issue if the authors could explain the motivation for using Sugeno integral and their formulation, and point out my error. Otherwise I would suggest to give the formula for the score in simplified form, and to only give the fuzzy integral formulation if there is a well-founded motivation behind doing so.\n\nIn any case, LeanScorer seems like LLM-as-a-judge with a more complex prompt and score shaping. I am not convinced that LeanScorer is different from LLM-as-a-judge with a more carefully crafted prompt. For example, I think if we prompt the LLM to be stricter (e.g. by giving it a rubric) in Table 2, the precision of LLM-as-a-judge will increase and recall might decrease from 100%, and the F1 score might match LeanScorer, which is itself a LLM judge anyway. Also, LeanScorer is only used for miniF2F-test and Gaokao-Formal, but in both cases the human-written ground-truth formalization exists. Why doesn't the LLM simply compare to the ground-truth formalization, or use BEq (see my questions)?\n\nI am not surprised that performance increased significantly on Gaokao-Formal in Table 3, because the RL training also used Gaokao problems, and the autoformalizer distribution could just be shifted toward Gaokao more.\n\nIt is unclear what “proving accuracy” (line 423) means to me. If I guess correctly, starting from an informal statement, proving accuracy is 1 if a prover model can prove the formal statement translated by another autoformalizer, and 0 otherwise. Is this correct? Consequently, the improvement in Figure 4 is hard to interpret. For example if the autoformalizer model gives wrong formalizations but they are easier to prove (with DPO training), this would still increase the “accuracy”.\n\nOverall, some parts of the paper could be clearer and key ideas could be better conveyed. For example, the authors give many numerical comparisons in the text of Section 4.3, but little explanation, insight, or examples as to why the score of their model is higher. The only “case study” in Appendix E does not explain what it studies and is not referenced anywhere else.\n\nI am happy to increase the score if the weaknesses and questions are addressed.", "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)