Statement auto‑formalization translates mathematics from natural language into proof assistants such as Lean 4, and recent models can do this at scale. As provers become stronger, the burden of correctness shifts from the proof to the statement: does the formal statement faithfully capture its source? Given a trusted reference formalization, the obvious test is logical equivalence, but this is too permissive. If the library can prove $P$ and $Q$ separately, one can always derive $P \leftrightarrow \mathrm{True} \leftrightarrow Q$, so any two statements trivially satisfy $P \leftrightarrow Q$. The stronger the prover, the more unrelated pairs pass.
Earlier approaches curb the prover and require each proof to explicitly name the other statement. We introduce SemantEq, a more principled relation that demands each statement be transformed into the other only via a chain of allowed steps—logical rearrangement, rewriting with the library’s own equations, etc. Our judgment relies on the proof term that Lean checks, not on the tactic script.
Based on this, we built SemantEq‑Eval, a model‑free search that attains 100% precision and 65.6% recall on the ProofNetVerif test split under our adjudicated labels, outperforming BEq+ (95.8% precision, 61.8% recall) while incurring only an 8.9‑fold increase in CPU time and adding at most three extra pairs.
A language model can discover more proofs, but under two of four prompts it proves both directions for only about two‑fifths of the non‑equivalent pairs. We further develop SemantEq‑ProofAudit, which audits each model‑written proof under a policy derived from the relation. It rejects all 104 non‑equivalent pairs and raises recall on 407 equivalent pairs from 65.4% to 81.1% with the best prompt.
Separating the generation of equivalence proofs from their acceptance lets a stronger prover raise recall without changing the meaning of acceptance.
The code and data are released at https://github.com/hlxr89/SemantEq
Review