Sage: Formalization with Semantic Correction

Thomas Hirtz; Farzad Jafarrahmani; Abdelmouksit Sagueni; Xiang Zhou; Wenping Deng; Liang Zhang

cs.LGSep 16, 2026

Sage: Formalization with Semantic Correction

Authors: Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, Liang Zhang

Organizations: Huawei Lagrange Mathematics and Computing Research Center Paris, France

Abstract

While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating informal natural language into a formal language is a critical data bottleneck plagued by an "illusion of rigor": standard type-checkers accept statements that compile but drop hypotheses, introduce vacuous truths, or subtly alter mathematical bounds. To resolve this, we introduce Sage (Semantic Agent-Guided Formalization Engine), an agentic framework that replaces monolithic translation with a four-stage decomposed generation pipeline coupled with a dual-signal semantic correction loop. By pairing Lean 4 compiler diagnostics with multi-dimensional semantic feedback, our correction loop enforces mathematical fidelity alongside syntactic validity. By explicitly accounting for the gap between open-ended queries and declarative formal targets, our pipeline prevents models from achieving high formalization rates by guessing unverified answers (exhibiting a 70.9% answer leakage rate in monolithic baselines). Consequently, Sage suppresses leakage to 2.7% while achieving 73.3% pass@4 joint compilation and semantic fidelity on the Omni-MATH without proofs (compared to 42.0% for a fine-tuned Goedel-Formalizer-V2 baseline). Finally, on IMO-Unformalized, a novel frontier of 175 unformalized International Mathematical Olympiad problems, Sage demonstrates effective zero-shot generalization with 87.4% pass@4 verified fidelity compared to just 19.4% for the baseline, winning over 79% of blind pairwise evaluations.

Figures & tables

Panel of Figure 1 — Figure 1: Overview of Sage : an autoformalization example ( 1(a) ) , the multi-stage generation chain ( 1(b) ) , and the syntax/semantic feedback loop ( 1(c) ) . Blue: LLM agents; orange: verifiers.

Strategy	Lean 4 Formalization Example ( $S_{\mathrm{NL}}$ : Find an object $x$ of type $\alpha$ that satisfies the property $P$ )	Syntactic Validity?	Semantic Fidelity?	Preserves Texture?	Requires Oracle?
Explicit Answer	theorem target : P c := by sorry	Yes	Yes	No	Yes
Placeholder	def x : $\alpha$ := sorry theorem target : P x := by sorry	Breaks Read-Only	Yes	Yes	No
Existential	theorem target : $\exists$ x : $\alpha$ , P x := by sorry	Yes	Vulnerable	Yes	No

Table 1: The Formalization Feasibility Trilemma across Question Types.

Panel of Figure 2 — Figure 2: Contextual Integrity Failure Modes.

Table 4

	pass@1			pass@4
Method	Compile	Goedel-SM	Compile $\wedge$ Goedel-SM	Compile	Compile $\wedge$ Goedel-SM
IMO-Formalized ( $N=223$ , Established Benchmark)
Monolithic (Zero-Shot)	72.6	57.4	43.0	83.9	62.3
Goedel-Formalizer-V2 (Baseline)	76.7	44.4	37.2	90.6	50.7
Sage (Ours)	94.2	65.0	61.4	99.6	83.9
IMO-Unformalized ( $N=175$ , Unformalized Frontier)

Table 4: Formalization quality across the IMO landscape (Answer-Agnostic).

	pass@1		pass@4
Method	Compile	Compile $\wedge$ Goedel-SM	Compile	Compile $\wedge$ Goedel-SM
Monolithic †	73.0	40.0	87.3	59.0
Monolithic + Dual †	95.7	55.3	99.0	75.0
Decomposed	62.0	29.7	85.0	50.7
Decomposed + Syntax	95.7	42.7	99.0	61.7
Decomposed + Dual ( Sage )	94.7	50.3	98.7	73.3

Table 5: Formalization quality on Omni-MATH (Answer-Agnostic). † Monolithic variants suffer from severe answer leakage (

>

70\text{,}\mathrm{%}$$ , guessing unverified answers; see Table 6 ). Sage is the top-performing valid, leak-free method. Bold indicates best leak-free performance.

Method	Compile ( $\uparrow$ )	Goedel-SM ( $\uparrow$ )	Answer Leakage ( $\downarrow$ )	Multiple Sorries ( $\downarrow$ )
Monolithic	73.0	51.0	72.6	0.5
Monolithic + Dual	95.7	57.0	70.9	1.0
Decomposed	62.0	45.3	1.0	2.2
Decomposed + Dual ( Sage )	94.7	54.0	2.7	1.1
Goedel (Finetuned)	74.0	32.0	56.2	2.3

Table 6: Structural fidelity on Omni-MATH (Answer-Agnostic, pass@1).

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Agent	Input	Output	Description & Core Role
Distiller	$S_{\mathrm{NL}}$ , $P_{\mathrm{NL}}$ ?	Domain + Inferred Goal context	Identifies the mathematical domain and either extracts the Inferred Goal from the proof or reformulates the open query into a declarative statement.
Preprocessor	Distiller output	$S_{\mathrm{DNF}}$ , local defs, hyps, $G$	Standardizes the problem into a unified Declarative Normal Form Statement statement ( $S_{\mathrm{DNF}}$ ) and decomposes it into assumptions, local definitions, and goals.
Formalizer	$S_{\mathrm{DNF}}$ components	Lean def s + theorem … sorry	Maps assumptions and infrastructure into idiomatic Lean 4 statements, relying on Mathlib concepts while avoiding trivialization.
Formatter	Draft code	Standalone .lean file	Organizes namespaces, imports, and scaffolding into a compilable file without altering the underlying mathematical meaning.

Appendix

Table 7: Sage generation pipeline. The sequential, role-isolated agents composing the generation chain. Each stage processes specialized mathematical components, ensuring clear translation contracts before generating the final compilable Lean 4 code.

Panel of Figure 3 — Figure 3: Compositional generation walkthrough on Omni-MATH #043. The same informal question is processed under both regimes. With $P_{\mathrm{NL}}$ , the Distiller extracts an Inferred Goal ( $n=6$ ) and the Preprocessor builds a Declarative Normal Form Statement claim with hypothesis $h_{1}$ and goal $G\colon n=6$ . Without a proof, the Distiller commits to a declarative reformulation ( $\exists!\,n$ ), which flows through to an existential Lean 4 goal.

Model	Role	Temp.	Max tokens	Retries
Qwen3.6-27B	Pipeline generation + in-loop rater	0.6	16,384	2
Goedel-Formalizer-V2-32B	Fine-tuned baseline ( Goedel )	0.7	16,384	1
Gemma4-31B	Post-hoc evaluation ( Goedel-SM / PWR )	0.6	16,384	2

Appendix

Table 8: LLM decoding and sampling hyperparameters.

Method	Base Model	Architecture	Feedback Type	Rounds ( $T$ )
Monolithic Configurations
Monolithic	Qwen3.6-27B	Monolithic	None	1
Monolithic + Syntax	Qwen3.6-27B	Monolithic	Compile	5–10
Monolithic + Dual	Qwen3.6-27B	Monolithic	Compile + Sage-SM	5–10
Decomposed Configurations (Ours)
Decomposed	Qwen3.6-27B	Decomposed	None	1

Appendix

Table 9: Overview of evaluated methods and ablation variants. Iterative variants are evaluated under matching iteration budgets (

T=5

on Omni-MATH ,

T=10

on IMO-Unformalized ) on a shared base model to ensure strict test-time compute parity.

Dimension	Scale	Cutoff
Semantic Match	$0$ – $4$	$\geq 4$
Missing	$0$ – $3$	$\leq 1$
Extra	$0$ – $4$	$\leq 1$
Wrong	$0$ – $2$	$=0$
Exactness	$0$ – $3$	$\geq 1$
Naturality	$0$ – $4$	$\geq 3$

Appendix

Table 10: In-loop Sage-SM gate. Scales are those used by the Rater prompt; cutoffs are conjunctive (all must hold).

Method	$N_{\mathrm{rejection}}$	Wrong Injection (%)	Mathematically False (%)	Existential (%)
Monolithic	147	69.4	84.4	8.2
Monolithic + Dual	129	68.2	80.6	15.5
Decomposed	164	8.5	22.0	72.0
Decomposed + Dual ( Sage )	138	7.2	18.1	76.8
Goedel (Finetuned)	204	56.9	74.5	19.6

Appendix

Table 11: Goedel-SM reject reasons on Omni-MATH (Answer-Agnostic) at pass@1. Three most common categories among Inappropriate samples (multi-hot; lower is better for defect categories). Bold

=

lowest rate.

Model Backbone	Compile	Goedel-SM	Compile $\wedge$ Goedel-SM	Joint Count	Compile $\wedge$ Sage-SM ∗	Witness Injection (%)
Qwen3-32B (32B)	57.3	46.3	30.3	91 / 300	52.3	22.0
Qwen3.6-27B (27B)	96.0	80.3	77.3	232 / 300	93.7	90.2
Qwen3.8-27B (27B)	98.0	86.3	85.7	257 / 300	95.7	89.5

Appendix

Table 12: Comprehensive generator backbone ablation on Omni-MATH (Answer-Aware, pass@1,

N=300

). ∗ In-loop optimization target. All methods use Sage with identical prompting, repair budgets (

T=5

), and independent judge protocols. Joint solved counts reported out of 300 problems.

Benchmark	$N$	Accuracy (%)	Precision (%)	Recall (%)	F1 (%)	Matthews correlation	Majority baseline (%)
ConsistencyCheck ( Chen et al., 2026 )	859	85.7	88.0	90.9	89.4	0.67	66.4
ProofNetVerif ( Poiroux et al., 2025 )	3752	88.8	82.1	80.9	81.5	0.74	69.6

Appendix

Table 13: External evaluation of the Sage-SM five-core gate against gold faithfulness labels on ConsistencyCheck and ProofNetVerif. Predictor: published Pass/Fail gate; Pass is the positive class.

	Preference for Sage over Goedel (%)
Evaluation Type	Much Better	Better	Tie	Worse	Much Worse
Semantic ( PWR )	78.3	1.1	17.7	1.1	1.7

Appendix

Table 14: Blind pairwise preferences on IMO-Unformalized (Answer-Agnostic, pass@1). Percentages may not sum to

100\text{\,}\mathrm{\%}

due to rounding.

Explore similar work

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
Sep 12, 2026Joshua Ong Jun Leang, Haonan Li, Zheng Zhao +6Mathematical Reasoning Theorem Proving
Institute of Foundation Models · Imperial College London · University of Edinburgh +1
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Jun 2, 2026Po-Nien Kung, Linfeng Song, Dawsen Hwang +10Theorem Proving Formalization
Google Cloud AI Research · Google Cloud · Google DeepMind
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Autoformalization Theorem Proving

Sep 12, 2026, cs.AIJ/K move · Enter open · S save

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang+5

Institute of Foundation Models · Imperial College London · University of Edinburgh+1

Mathematical Reasoning Theorem Proving LLM Reasoning Strategies Natural Language Loop

Open paper AskPDF arXiv

Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.

Abstract

Explore similar work

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics