A proof assistant can prove a formal statement correctly even when that statement mistranslates the original mathematics. The SemantEq paper studies the acceptance rule needed when comparing an autoformalized statement with a trusted reference.
Logical equivalence can be too permissive
If a library can prove two statements separately, a prover can establish their logical equivalence through the fact that both are true. That does not show that they express the same mathematical claim. A more capable prover can consequently make a permissive translation test less informative.
SemantEq requires a statement to turn into the other through a chain of allowed steps, such as logical rearrangement and rewriting with library equations. Its programs examine the proof term Lean checks, rather than relying on the tactic script's appearance.
Separate proof generation from acceptance
On the adjudicated ProofNetVerif test split, the model-free SemantEq-Eval search reports 100% precision and 65.6% recall. The paper compares that with 95.8% precision and 61.8% recall for BEq+. Increasing search CPU time by 8.9 times adds at most three pairs in that evaluation.
A language model can find more proofs, but it also produces misleading equivalence proofs. SemantEq-ProofAudit accepts none of the 104 non-equivalent pairs in the study. Under the best prompt, its recall on 407 equivalent pairs rises from 65.4% to 81.1%.
Keep the acceptance policy visible
Those figures belong to the paper's labelled pairs, prompts and allowed transformations. They are not a guarantee that every future mistranslation will be rejected. A reproduction should preserve the reference statement, proof term, acceptance policy and adjudication criteria.
The practical idea is to let a stronger generator search for useful proofs while keeping a separate rule for what counts as faithful equivalence. That distinction matters when a formally valid answer could still certify the wrong interpretation of the source mathematics.
Comments