SemantEq: Faithful Bidirectional Equivalence of Formal Statements

Xinrui Li; Pawan Sasanka Ammanamanchi; Siddharth Bhat; Rianna Jamdar; Yongxi Lin; Stella Biderman

cs.AIOct 23, 2026

SemantEq: Faithful Bidirectional Equivalence of Formal Statements

Authors: Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman

Organizations: EleutherAI · Carnegie Mellon University · University of Cambridge · XTX Markets

Abstract

Statement autoformalization translates mathematics from natural language into a proof assistant such as Lean 4, and models now do it at scale. As provers get stronger, the burden of correctness shifts from the proof to the statement, that is, to whether the formal statement faithfully translates its source. Given a trusted reference formalization, the natural test is logical equivalence, and it proves too much. $P \leftrightarrow Q$ holds trivially for any two statements $P$ and $Q$ that the library proves, because a prover can prove each separately and pass through $P \leftrightarrow \mathrm{True} \leftrightarrow Q$ . The stronger the prover, the more unrelated pairs pass. Earlier methods restrict the prover and check that each proof names the other statement. We introduce SemantEq, a more principled relation that instead requires each statement to turn into the other only through a chain of allowed steps, such as logical rearrangement and rewriting with the library's own equations. Our programs judge a proof by the proof term Lean checks, not by its tactic script. SemantEq-Eval, a search without a model, reaches 100% precision and 65.6% recall on the ProofNetVerif test split under our adjudicated labels, against 95.8% and 61.8% for BEq+, and an 8.9-fold increase in its CPU time adds at most three pairs. A language model finds more proofs, but under two of four prompts it proves both directions of about two in five of the non-equivalent pairs. SemantEq-ProofAudit audits each model-written proof under a policy derived from the relation and accepts none of the 104 non-equivalent pairs, and it raises recall on 407 equivalent pairs from 65.4% to 81.1% under the best prompt. Separating the generation of equivalence proofs from their acceptance lets a stronger prover raise recall without changing what an acceptance means. We release code and data at: https://github.com/hlxr89/SemantEq

Figures & tables

Panel of Figure 1 — Figure 1: Chains witnessing $P\simeq_{Sem,\ \mathcal{L}}Q$ . Rearrangement and bridge rewriting can be reversed, but a change of variables or a weakening need not be, so a separate chain leads back from $Q$ to $P$ .

Panel of Figure 2 — Figure 2: One implication direction. The relevance gate runs before the search. Each proof that a stage finds must pass the three audits below it, or the search moves on to the next stage.

Labels	System	TP	FP	FN	TN	Precision	Recall	F1
Published	Ours	242	0	229	832	100.0	51.4	67.9
	$\texttt{BEq}+$ ‡	230	8	241	824	96.6	48.8	64.9
Adjudicated	Ours	242	0	127	934	100.0	65.6	79.2
	$\texttt{BEq}+$ ‡	228	10	141	924	95.8	61.8	75.1

Table 1: Equivalence judgements on the ProofNetVerif test split, scored on the 1,303 of 1,452 pairs that elaborate on our toolchain, under the published labels and under our adjudicated labels.

	ProofNetVerif test split (50)	Added claim (18)	Neighbouring theorem (14)	Unrelated true fact (14)	Vacuous hypotheses (4)	Total
Ours, all checks	0	0	0	0	0	0
without relevance	0	15	4	0	0	19
without proof-term grading	0	0	2	6	0	8
without explosion check	2	0	0	0	1	3
without antecedent-free replay	0	0	1	1	0	2
without all four	2	17	7	7	2	35

Table 2: Contribution of each audit of § 2.2 on the ablation set of 100 non-equivalent pairs, fifty from the ProofNetVerif test split and fifty constructed. Entries count erroneous acceptances.

Figure 3: (A) Recall attainable when each pair is allowed at most $\tau$ seconds, computed from the uncapped runs on the equivalent set . $\texttt{BEq}+$ leads below roughly 15 s per pair, and the curves level off at $65.4\%$ for SemantEq-Eval and at $61.4\%$ and $60.2\%$ for $\texttt{BEq}+$ on Lean v4.8 and on our toolchain. (B) Recall against mean cost per pair for each search configuration (Appendix I ).

Figure 4: The auditor gives each position in a proof term a role. The same library fact can be admitted as the justification of a rewrite and refused when it proves the goal directly.

SemantEq-ProofAudit , by prompt style
	Equivalent (407)			Non-equivalent (104)
	both	one	neither	both	one	neither	Precision	Recall
$\texttt{BEq}+$	245	29	133	2	26	76	99.2	60.2
SemantEq-Eval (default)	266	58	83	0	34	70	100.0	65.4
Expedient	309	40	58	0	49	55	100.0	75.9
Unrestricted	322	53	32	0	57	47	100.0	79.1

Table 3: Certificates on the certification set, the 407 equivalent pairs and the 104 that our review relabelled non-equivalent. A pair is accepted only when both directions are certified, and precision and recall are over that acceptance. The reference rows apply the same count to SemantEq-Eval and

\texttt{BEq}+

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Prompt style	both	one	neither	both	one	neither	Precision	Recall
	Equivalent (407)			Non-equivalent (104)
Expedient	303	45	59	0	46	58	100.0	74.4
Unrestricted	317	56	34	0	50	54	100.0	77.9
Faithful	323	56	28	0	59	45	100.0	79.4
Rewrite	323	56	28	0	64	40	100.0	79.4

Appendix

Table 4: The campaign of Table 3 under the stricter audit policy, in which a severe use, a library fact meeting a hypothesis of the antecedent while drawing on no local hypothesis, fails the proof wherever it occurs. Pairs are counted as both directions, one direction, or neither, and precision and recall are over pair-level acceptance, as in Table 3 .

Configuration	Median	Mean	Max	Total	New	Recall
	(s)	(s)	(s)	CPU
BEq+	1.0	6.3	74	0.71 h	—	60.2%
D1 (base)	2.0	30.5	489	3.45 h	—	65.4%
D1 $+$ W1	2.0	43.2	541	4.88 h	$+2$	65.8%
D2	2.0	50.7	606	5.73 h	$+1$	66.1%
D8 $+$ W2 $+$ DW2	2.0	271.3	3126	30.67 h	0	66.1%

Appendix

Table 5: Effect of search strength on recall and cost over the equivalent set .

D

is the depth of chained rewrites;

W_{k}

and

DW_{k}

double

k

times the per-step bridge budgets and the number of intermediate statements retained at each depth. Recall is not comparable with Table 1 , which does not contain the recall suite. The full grid is Table 6 .

Configuration	Median	Mean	Max	Total	New	Recall
	(s)	(s)	(s)	CPU
Reference point
BEq+	1.0	6.3	74	0.71 h	—	60.2%
D1 (base)	2.0	30.5	489	3.45 h	—	65.4%
D1 $+$ W1	2.0	43.2	541	4.88 h	$+2$	65.8%
D2	2.0	50.7	606	5.73 h	$+1$	66.1%

Appendix

Table 6: Effect of search strength on recall and cost over the 407 adjudicated-equivalent pairs, all configurations.

D

W

and

DW

are defined in Appendix F . “New” counts pairs accepted by the configuration and by none cheaper.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 336 papers

Jun 15, 2026

The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

Autoformalization, translating natural-language mathematics into formal proof assistants, is bottlenecked not by translation fluency but by faithfulness: a formal statement can typecheck and be provable, yet still encode a different theorem than the source intended. We introduce Bidirectional Provability Fingerprinting (\bpf{}), a framework that certifies faithfulness by characterizing each candidate through its forward and backward consequence neighborhoods in the ambient theory and matching these against probes derived from the natural-language statement. We further introduce four novel components: (i) Counterfactual Probe Generation (\cpg{}), a contrastive procedure that synthesizes probes targeting specific drift directions; (ii) the Equivalence Spectrum, a continuous faithfulness score that replaces brittle binary verdicts; (iii) Adaptive Probe Budget Allocation (\apba{}), an information-theoretic budget router; and (iv) Faithfulness-Guided Decoding (\fgd{}), which uses \bpf{} signals as a reward during autoformalization. We prove a drift detection theorem and a PAC-faithfulness result establishing that the equivalence class of a natural language statement is learnable from

\mathcal{O}(\log(1/δ)/\varepsilon)

probes under mild assumptions. We release \driftbench{}, a benchmark of

2{,}183

NL/Lean~4 pairs with controlled drift labels across six subfields of mathlib4. \bpf{},+,\cpg{} detects

89.6\%

of drifted formalizations at a

3.0\%

false-positive rate-against

41.2\%

for typecheck and

63.3\%

for LLM-judge baselines, and \fgd{} reduces the rate at which a state-of-the-art autoformalizer emits drifted statements by

47\%

. https://pmlrbd.github.io/BPF/

Noor Islam S. Mohammad, Tamim Sheikh

Department of Computer Science, Informatics Institute, Istanbul Technical University, Istanbul, Türkiye · Department of Computer Science and Engineering, Jashore University of Science and Technology, Bangladesh.

Formal Verification Lean Theorem Proving Autoformalization

Ask PDF

Jun 30, 2026

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Lean verifies that a generated declaration is well typed, but cannot check whether it states what the user intended. We measure how far compilation overstates faithfulness in statement autoformalization without canonical Lean targets. Our criterion requires Lean compilation and agreement of two LLM judges from different model families. On an independent random audit, it agrees with the human majority on 91.5% of cases; it rarely accepts an unfaithful output but rejects some faithful ones. Across eight systems on 227 university-level statements, the gap between compiling and accepted outputs ranges from 1.3 to 29.5 percentage points: our tool-augmented agent compiles 87.2% of the statements, but only 57.7% are accepted. Human review of all the agent's rejections confirms that 23.8 of its 29.5 points are real translation errors. For the gaps of the seven one-shot systems, a two-stage review by Claude Opus 5.5 with Lean and GPT-6.1 Sol, validated on these human labels, finds that 78-100% are real translation errors for six of them. When GPT-5.2, one of the two judges, grades the translations of two models released after it, GPT-6 Astra and Claude Opus 5.5, it accepts 83% of the statements for each, against 21% for one-shot GPT-5.2. For these two models, the same review classifies only 4 of their 54 rejections (7%) as translation errors, so most of their measured gap is judge errors rather than translation errors. This is consistent with these systems erring less while the judge does not: the fewer errors a system makes, the smaller the share of its rejections that are translation errors. Finally, a 2^3 tool ablation of the agent shows that Lean feedback drives most of its compilation gain, and that nearly half of this gain fails the semantic criterion. Code and data are available at https://github.com/grenadeComing/beyond-compilation.

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3

University of California, Riverside · University of Arizona · University of California, San Diego

LLM-as-a-Judge Lean Theorem Proving Autoformalization

Ask PDF

May 26, 2026

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.

Jinzheng Li, Zeru Zhu, Yuanjie Ren

1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Large Language Model-Guided Theorem Proving Automated Theorem Proving Lean Theorem Proving

Ask PDF

Abstract

Formal Verification

Explore similar work

The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving