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 339 papers

The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements
Jun 15, 2026Noor Islam S. Mohammad, Tamim SheikhFormal Verification Lean Theorem Proving
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.
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
Jun 30, 2026Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3LLM-as-a-Judge Lean Theorem Proving
University of California, Riverside · University of Arizona · University of California, San Diego
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenLarge Language Model-Guided Theorem Proving Automated Theorem Proving
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Jun 15, 2026J/K move · Enter open · S save

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

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

Open paper AskPDF arXiv

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/

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