Statement Equivalence Checking

Sources#

• SemantEq: Faithful Bidirectional Equivalence of Formal Statements
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Summary#

When a trusted reference formalization exists, checking a candidate statement reduces to one question: do the two say the same thing? That is the mechanical half of the Statement Drift problem. The obvious test is logical equivalence, proved in Lean, and it fails in a specific way. If the library proves both P and Q, then P → Q holds by ignoring P and proving Q outright, so Nat.Prime 5 and Irrational (Real.sqrt 2) are "equivalent". The stronger the prover, the more unrelated pairs pass. Every proof-based checker in the corpus is a different answer to the question of which equivalence proofs to accept.

SemantEq: Faithful Bidirectional Equivalence of Formal Statements (Li, Ammanamanchi, Bhat, Jamdar, Lin & Biderman, EleutherAI / CMU / Cambridge, arXiv 2610.32919, 2026-10-23, empirical) gives the sharpest answer so far. It fixes the allowed steps first, defines equivalence as a chain of them in each direction, and then judges the proof term the kernel checks rather than the tactic script that produced it. Because acceptance is fixed separately from generation, any prover, including a language model, can search for the proof without changing what an acceptance means.

The ladder of checks#

SemantEq's Appendix E shows both BEq+ failures on pairs that ProofNetVerif labels not equivalent. In the first, associativity in ZMod n against a natural-number remainder identity, each side has its own direct proof (mul_assoc, Nat.mul_mod), and noncomm_ring closes one direction without the antecedent. In the second, Rudin 2.19a, the antecedent never appears in one direction's proof term (apply_rules elaborates to have this:= hAB), and in the other it appears but is not needed.

SemantEq: equivalence as a chain of allowed steps#

Definition 1 allows four kinds of step, each defined by its effect on a statement:

• Logical rearrangement: same atoms, equivalent under every interpretation, every atom mattering on both sides. Covers commutativity, De Morgan, currying and similar; excludes adding a true conjunct, case splits and the laws of equality.
• Bridge rewriting: rewrite with a library theorem whose conclusion is = or ↔ (a bridge), with its hypotheses provable in context. B is every such theorem in Mathlib, so no bridge is chosen by hand.
• Change of variables: add a fresh universal variable, or instantiate one with a term built from the prefix (a structure argument must be one the statement already carries).
• Structural weakening: drop a conjunct, add a disjunct, witness an existential, add a hypothesis, or remove one the others imply, at positive occurrences or in the prefix.

No step proves anything. Two statements are SemantEq when a chain leads from each to the other, and the last two step kinds need not reverse, so the chains can differ. Proposition 1: the relation is an equivalence relation that implies L ⊢ P ↔ Q. Proposition 2: without bridges it is strictly finer than logical equivalence, so even 4 = 4 cannot be added as a conjunct.

The one judgment call. Everything that distinguishes rephrasing from new content rests on the assumption that Mathlib's equations and biconditionals reflect how the community identifies objects of the same meaning. The authors concede Mathlib does not meet this everywhere, and both programs patch for it. Their own limitation: a bridge whose hypotheses a library proof meets can connect any two statements the library proves equivalent, so acceptance is evidence of faithful reformulation, not a proof of it.

SemantEq-Eval: a model-free search with four audits#

A deterministic Lean metaprogram runs five stages per direction, cheapest first: apply the antecedent directly; normalize both sides with a fixed set of logical and cast identities; destructure and match components; then two stages that rewrite with a pool of at most 40 discovered bridges. The first three use no library fact outside the fixed set and settle about three quarters of all directions. Median 2 s per pair on a laptop CPU, no GPU.

Four audits gate acceptance, and passing them is the criterion, not a consequence of Proposition 1: relevance (refuse if part of the goal the antecedent does not assert is provable without it), proof-term grading (expand auxiliary constants; admit only the antecedent, logical rules, bridges and 16 numeral facts), no proof ex falso, and antecedent-free replay (discard an acceptance that still closes with the antecedent withheld).

Results on ProofNetVerif (1,303 of 1,452 test pairs that elaborate on the toolchain; BEq+ ported with two compatibility fixes and no change of method):

The ablation. On 100 non-equivalent pairs (50 benchmark pairs including all 10 BEq+ accepts, and 50 constructed: 18 added-claim, 14 neighbouring-theorem, 14 unrelated-true-fact, 4 vacuous-hypothesis), the full system accepts 0 and BEq+ accepts 54. Removing relevance admits 19 (15 of them added claims), proof-term grading 8, the explosion check 3, replay 2, and all four together 35, more than the 32 of the single removals combined. The restricted steps alone still reject 20 of BEq+'s 54. The constructed half is designed to be easy to prove, so it tests the audits, not how often such pairs occur.

Search saturates. On 407 equivalent pairs the base configuration accepts 65.4%. Doubling the bridge pool adds 2 pairs, a second chained rewrite 1 more (66.1%), and eight stronger configurations nothing, while mean time per pair rises from 30.5 s to 271.3 s (3.45 to 30.67 CPU hours; median stays 2.0 s). The missed pairs need a step the search is built not to take: constructing an object before the antecedent applies, or a bridge the library does not state or states one way only. The bottleneck is the operation set, not the budget. BEq+ is the cheaper judge below about 15 s per pair.

SemantEq-ProofAudit: decouple generation from acceptance#

The second program lets any prover write the proofs and audits the result. GPT-5.6 Sol in Codex wrote both directions for the 511 pairs ProofNetVerif labelled equivalent (471 benchmark plus 40 recall-suite pairs), one session per pair under each of four prompt styles (expedient, unrestricted, faithful, rewrite). After adjudication 104 of the 511 are non-equivalent.

Compilation is not a judge. Under the expedient and unrestricted prompts the model's proofs compile in both directions for 43 and 45 of the 104 non-equivalent pairs. A compile-only check would accept them all.

The auditor reads the elaborated proof term and gives each position one of three roles: goal derivation, an argument to the antecedent, or the justification of a rewrite. On the goal derivation only the antecedent, logical rules and bridges are admitted, and a bridge must convert the goal rather than state it. The same library fact can therefore pass as a rewrite justification and fail when it proves the goal outright. The antecedent must do work in every part (each case-split branch, each conjunct), its arguments must come from the goal's own objects, and local lemmas are audited in turn. Every rejection names the rule broken, so the auditor can also feed a prover in a loop.

Search and model together certify 341 of 407 (83.8%). The model adds 75 pairs the search never closes and misses 11 it does. A stricter policy, which also fails a library fact meeting an antecedent hypothesis with no local grounding, lowers the faithful count to 323 and keeps precision at 100. Many non-equivalent pairs are certified in one direction, which is informative: it shows which statement is the stronger one.

The rejected proofs are diagnostic. One instantiates a linear-order antecedent at Prop, a type the goal never mentions. Another applies the antecedent to a set that exists only after the goal's conclusion is unfolded. A third destructures the antecedent, never uses it, and closes the goal with Set.center_prod. All three pairs are labelled equivalent in ProofNetVerif.

The labels moved, and the tools moved them#

Weigh the adjudicated numbers with this in view. The authors reviewed only the test pairs labelled equivalent and relabelled 102 of them non-equivalent (about 22% of the 471 that elaborate). The review of 88 was prompted by their own tools: no SemantEq-Eval configuration accepted those pairs and ProofAudit certified them in at most one direction. The other 14 came from a Claude Fable 5 screen and manual rulings, and a person made every final call. Pairs labelled non-equivalent were never reviewed, so the review could only lower recall denominators and raise SemantEq's precision, never expose a false rejection. A selection effect favouring the reviewers' own system follows from that design (wiki reasoning). The published labels guard against it: on them SemantEq-Eval is still 100.0 against 96.6 in precision and 51.4 against 48.8 in recall, so the ranking does not depend on the relabelling.

Part of the relabelling is a change of criterion, not a benchmark error. ProofNetVerif labels faithfulness to the informal statement. SemantEq labels equivalence to the reference. At least eight changes follow from that difference (four Artin 2.8.6 candidates state a set equality where the reference states an isomorphism; four Rudin 1.4 candidates assume a linear order where the reference has a partial one, which is closer to Rudin but less general). The IMO 1983 recall pair shows the criterion's edge: a candidate that puts positivity in a conjunct instead of a type is logically equivalent (a hand proof exists, and a strong model called it equivalent) but makes a claim the reference does not, and the auditor's remaining objection after four revision rounds located exactly that.

Where it sits#

• It addresses one route of Statement Drift. Misformalization against a trusted reference. It is blind to a wrong reference, to spec-level looseness, and to translation drift. The authors are explicit: a candidate that copies the reference's mistake passes, and a rejection only means no proof passed the search and audits.
• It is the reference-relative analogue of Kernel-Level Proof Auditing. That page's ladder audits whether a proof is a proof (#print axioms) and whether the statement is the trusted copy (Comparator identity). Equivalence checking sits between identity and nothing: it accepts rephrasings that identity rejects, and its audits apply the "what did the proof actually use" discipline to the antecedent instead of to axioms.
• Generation and acceptance separate, as in The Verifiability Thesis. Recall rises with a stronger prover (65.4% search, 81.1% model) while precision stays fixed by the audit. That is the same split as a generator–verifier loop with a sound verifier. The verifier here is a policy over proof terms, not the kernel.
• Why it matters beyond benchmarks. Equivalence checkers are also the reward for training formalizers and the filter on their outputs. A checker that accepts unfaithful statements trains a formalizer to write them (Reward Hacking against an unsound grader). The paper argues this and does not measure it.

A tension with SA-Pass (wiki reasoning). ShadowBench's SA-Pass is also bidirectional implication, against shadow theorems rather than one reference, and it reports precision 1.000 against experts. Its checker proofs are fixed at construction and appended to each candidate. SemantEq's argument predicts a blind spot there: a shadow the library proves outright passes its forward check for any candidate, and a candidate the library proves outright can satisfy a backward checker that never uses the shadows. ShadowBench's expert agreement says this did not bite on its sample. Neither paper audits the checker proofs' use of the antecedent. ShadowBench also reports BEq+ precision against experts of 0.400 on its own generated outputs and 0.887 on ProofNet outputs. It attributes the drop to auxiliary declarations that BEq+ ignores, a different mechanism from the library-only proofs SemantEq documents. Both papers find that BEq+ accepts pairs it should not, for different reasons.

Connections#

• Statement Drift — the failure family; this page is the mechanical defense for its first route (misformalization against a reference), and its check table's implication row now carries the P ↔ True ↔ Q caveat
• Kernel-Level Proof Auditing — the proof-side ladder; SemantEq audits the proof term's use of the antecedent the way #print axioms audits its use of axioms, and its ShadowBench section is where SA-Pass is placed
• LLM-Judge Validation — the alternative to a proof-backed checker is a model judge, and Biderman et al.'s "Key Problem" (the best equivalence detectors are the models being evaluated) is why the authors prefer a proof
• OEIS Open Benchmark — given statements taken as-is; reference-equivalence checking needs an independent second formalization, which that benchmark lacks
• Reward Hacking — equivalence checkers serve as rewards for formalizers, so an unsound one is a hackable grader by construction
• Lean — the proof terms audited, and Mathlib's equation and biconditional theorems as the bridge set
• The Verifiability Thesis (hub) — separating proof generation from acceptance keeps precision fixed while a stronger prover raises recall
• Verification as the New Bottleneck (hub) — "as provers get stronger, the burden of correctness shifts from the proof to the statement"
• Library-Grade Formalization — Comparator as a registry entry condition (Palomar) and Formal Conjectures as the vetted reference statements announcers are asked to reuse

Open Questions#

• Does ProofAudit's 0-of-104 hold when a prover is optimized against it? Every certified proof came from one model in one session per pair that never saw a verdict. The auditor is built to give feedback in a loop, which is also an optimization target. The falsifiable test is to run a prover with auditor feedback over many rounds, rewarded only for certification, on the 104 non-equivalent pairs and the 50 constructed ablation pairs, and count pairs certified in both directions.
• How large is BEq+'s false-acceptance rate on unrelated pairs at scale, and does SemantEq-Eval stay at zero there? The ablation's 54 of 100 is on pairs built to be easy to prove and does not estimate frequency. The settler is a large unrelated-pair sweep. The sibling paper ACE (arXiv 2610.25018, queued, not yet in this corpus) reportedly runs one for BEq+. Re-scoring SemantEq-Eval on the same pairs would settle it.

Sources#

• SemantEq: Faithful Bidirectional Equivalence of Formal Statements — Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin & Stella Biderman (EleutherAI, CMU, Cambridge, XTX Markets), arXiv 2610.32919, 2026-10-23, 37 pp, empirical. Code and data released. Cited for the relation (Definition 1, Propositions 1–2), SemantEq-Eval's stages and audits, Table 1, the Table 2 ablation, the Table 5–6 saturation grid, Table 3's certification counts, the stricter policy (Table 4), the Appendix E BEq+ failures, the Appendix J case studies and the Appendix H adjudication. All tables reconciled against the prose: Table 1's TP/FN columns reproduce the stated precisions and recalls (242/369 = 65.6%, 228/238 = 95.8%), and Tables 2–4 match every count the text restates. Table 3's spanning "by prompt style" row is a header repeated across columns by the parse, harmless. Figures not opened; Figure 3's plateau values are in its caption. The authors build and evaluate their own system and adjudicated the labels it is scored on, with 88 of 102 relabellings prompted by its outputs (see above). The published-label results are the clean comparison.
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han et al., arXiv 2608.29270, 2026-08-29, empirical. Cited for SA-Pass's checker design (fixed checker theorems appended to the candidate) and its BEq+ precision against expert labels on ShadowBench (Table 4, 0.400, attributed to ignored auxiliary declarations) and on ProofNet Llama 3.1 8B outputs (Table 6, 0.887). Full treatment on Kernel-Level Proof Auditing.