arXiv cs.AI· Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman·· 2 小时前AI 评分41
SemantEq：形式化语句的忠实双向等价判定方法
SemantEq: Faithful Bidirectional Equivalence of Formal Statements
AI 导读
论文提出 SemantEq，一种针对形式化语句（如 Lean 4 自动形式化）的更严格双向等价判定关系，要求证明只能通过逻辑重排和库内等式重写等允许步骤完成，避免强 prover 下 P↔Q 平凡成立的问题。
正文 · 原文
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: this https URL
| Comments: | 37 pages, 4 figures, 6 tables. Code and data: this https URL |
| Subjects: | Artificial Intelligence (cs.AI); Machine Learning (cs.LG) |
| Cite as: | arXiv:2610.32919 [cs.AI] |
| (or arXiv:2610.32919v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.32919 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Xinrui Li [view email]
[v1]
Fri, 23 Oct 2026 17:20:12 UTC (309 KB)
来源：arXiv cs.AI · arxiv.org