SemantEq: A New Bidirectional Equivalence Method for Formal Mathematical Statements

As AI models translate natural language mathematics into formal statements in proof assistants like Lean 4 at scale, the center of gravity for correctness is shifting from the proof itself to the statement—whether the formal statement is faithful to the original text. Recently, a paper titled "SemantEq: Faithful Bidirectional Equivalence of Formal Statements" proposed a stricter bidirectional equivalence relation aimed at solving the problem that existing logical equivalence tests are too permissive.

The Dilemma of Logical Equivalence Testing

Given a trusted reference formalization, the most natural test is logical equivalence, but research finds that this "proves too much." For any two provable statements P and Q in the library, since the prover can prove them separately and transit via P ↔ True ↔ Q, P ↔ Q easily holds. The stronger the prover, the more unrelated statement pairs pass the test.

According to the paper, earlier methods addressed this by restricting the prover and checking whether each proof references the other statement. However, this approach is not principled enough. SemantEq instead requires each statement to be transformed into the other only through a series of allowed steps (such as logical rearrangement, rewriting using the library's own equations).

Proof terms and tactic scripts: In proof assistants based on dependent type theory such as Lean 4, a tactic script is a user-written sequence of commands that guides proof search, while a proof term is the actual proof object checked by the kernel after these tactics are executed. Tactic scripts may contain automated search, macro expansion, or non-terminating loops, and their style varies by person and tool; proof terms are terms in type theory with a canonical structure, and their correctness is independently verified by a small trusted kernel. Therefore, judging equivalence based on proof terms avoids bias caused by different tactic styles or differing degrees of prover automation, making the equivalence relation closer to the semantic content of the statement itself.

Core Design of SemantEq

The core innovation of SemantEq is that the program judges proofs by the Lean-checked proof term rather than its tactic script. This means the judgment criterion does not depend on how the proof was generated, but on the structure of the proof itself.

This relation defines a chain of "allowed steps": each statement must be transformed into the other through operations such as logical rearrangement and rewriting. This design ensures that equivalence is not achieved by "cheating" through the prover's power, but is based on substantive connections between statements.

Rewriting and logical rearrangement: The steps allowed by SemantEq include logical rearrangement (such as swapping conjuncts, adjusting quantifier order, and other syntactic transformations that preserve classical logical equivalence) and rewriting using the library's own equations (replacing subterms in a statement with expressions already proven equal in the library). These steps form a transformation chain from statement P to statement Q, each step verifiable by the Lean kernel. Unlike general logical equivalence, this chain limits the room for the prover to "freely improvise": it cannot introduce auxiliary lemmas unrelated to the library, nor can it use the prover's strong automation to cross semantic gaps. Thus, SemantEq captures the substantive convertibility of statements within the library context, rather than the loose equivalence based merely on identical classical logical truth values.

Evaluation and Results

The research team built SemantEq-Eval, a model-free search method. On the ProofNetVerif test set, according to human-adjudicated labels, SemantEq-Eval achieved 100% precision and 65.6% recall, while BEq+ achieved 95.8% precision and 61.8% recall. Interestingly, increasing CPU time by 8.9x added at most three new equivalent statement pairs, indicating the method's high efficiency.

Language models can find more proofs, but under two of four prompts, for about two-fifths of non-equivalent statement pairs, the model proves both directions. SemantEq-ProofAudit audits each model-written proof based on the strategy derived from the relation, rejecting all of the 104 non-equivalent statement pairs, and raising recall on 407 equivalent statement pairs from 65.4% to 81.1% under the best prompt.

Precision and recall: In equivalence detection tasks, precision refers to the proportion of statement pairs judged equivalent that are truly equivalent, and recall refers to the proportion of all truly equivalent statement pairs that are successfully found. SemantEq-Eval achieving 100% precision means all equivalence pairs it judges are correct with no false positives; 65.6% recall indicates it found about two-thirds of equivalent pairs. In comparison, BEq+ has 95.8% precision and 61.8% recall, showing that SemantEq covers more equivalent statements while maintaining higher accuracy. High precision is especially critical for verification scenarios, because misjudging equivalence may cause formal statements to deviate from the original meaning without being detected.

Separating Generation from Acceptance

An important idea of SemantEq is to separate the generation of equivalence proofs from acceptance: stronger provers can improve recall without changing the meaning of "acceptance." This provides a more robust framework for verifying formal mathematics, so that as prover capabilities improve, verification reliability does not decrease.

The research team has open-sourced the code and data at: https://github.com/hlxr89/SemantEq.

Audit mechanism of ProofAudit: SemantEq-ProofAudit uses the SemantEq relation to audit equivalence proofs generated by language models. Specifically, when a model claims that statements P and Q are equivalent and provides a proof, the auditor checks whether the proof can be decomposed into a chain of steps allowed by SemantEq; if not, the proof is rejected. On 104 non-equivalent statement pairs, the auditor rejected all model proofs, showing that it effectively filters out false equivalences that "cheat" based on the prover's power. At the same time, under the best prompt, it raised recall on 407 equivalent statement pairs from 65.4% to 81.1%, indicating that while strictly gatekeeping, the audit mechanism can still accept legitimate equivalence proofs found by the model, thereby balancing reliability and coverage.

One-line Summary

SemantEq proposes a bidirectional equivalence relation to strictly verify the faithfulness of formal mathematical statements.

Paragraph Summary

SemantEq is a new bidirectional equivalence method for formal mathematical statements, aimed at solving the problem that traditional logical equivalence tests are too permissive. It requires two statements to be mutually transformable through a series of allowed steps (such as logical rearrangement and in-library equation rewriting), and judges based on Lean-checked proof terms rather than tactic scripts. On the ProofNetVerif test set, SemantEq-Eval achieves 100% precision and 65.6% recall, outperforming BEq+'s 95.8% and 61.8%. SemantEq-ProofAudit can audit proofs generated by language models, reject all non-equivalent statement pairs, and raise recall under the best prompt from 65.4% to 81.1%. The method separates the generation of equivalence proofs from acceptance, allowing stronger provers to improve recall without changing acceptance standards, providing a more robust framework for formal mathematical verification.