arXiv cs.AI· Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman·· 11 小时前AI 评分31
SemantEq：形式化语句的忠实双向等价关系
SemantEq: Faithful Bidirectional Equivalence of Formal Statements
AI 导读
SemantEq 提出一种更严格的形式化语句等价关系，要求两个语句只能通过逻辑重排和库内等式重写等允许步骤相互转化，而非依赖证明器各自证明后经 True 中转。
正文 · AI 翻译
摘要：语句自动形式化将数学从自然语言翻译为 Lean 4 等证明助手，而模型如今已能大规模完成这一任务。随着证明器日益强大，正确性的负担从证明转移到语句本身，即形式语句是否忠实翻译了其来源。给定可信的参考形式化，自然的检验是逻辑等价，但这一检验证明得太多。$P \leftrightarrow Q$ 对库能证明的任意两个语句 $P$ 和 $Q$ 都平凡成立，因为证明器可以分别证明二者，并通过 $P \leftrightarrow \mathrm{True} \leftrightarrow Q$ 传递。证明器越强，通过的不相关语句对就越多。早期方法限制证明器，并检查每个证明是否指名另一语句。我们引入 SemantEq，一种更有原则的关系，它要求每个语句只能通过一系列允许的步骤（如逻辑重排和用库自身的等式重写）转化为另一语句。我们的程序依据 Lean 检查的证明项而非其策略脚本来评判证明。SemantEq-Eval 是一种无模型的搜索，在我们裁定的标签下，于 ProofNetVerif 测试划分上达到 100% 精确率和 65.6% 召回率，而 BEq+ 为 95.8% 和 61.8%；其 CPU 时间增加 8.9 倍最多只多出三对。语言模型能找到更多证明，但在四种提示中的两种下，它对约五分之二的非等价语句对证明了双向。SemantEq-ProofAudit 依据由该关系导出的策略审计每个模型编写的证明，在 104 个非等价语句对中一个都不接受，并在最佳提示下将 407 个等价语句对的召回率从 65.4% 提升到 81.1%。将等价性证明的生成与其接受分离，使更强的证明器能提高召回率而不改变接受的含义。我们在以下地址发布代码和数据：此 https URL
| 评论： | 37 页，4 幅图，6 张表。代码和数据：此 https URL |
| 主题： | 人工智能（cs.AI）；机器学习（cs.LG） |
| 引用为： | arXiv:2610.32919 [cs.AI] |
| （或 arXiv:2610.32919v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.32919 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Xinrui Li [查看邮箱]
[v1]
2026 年 10 月 23 日星期五 17:20:12 UTC（309 KB）
来源：arXiv cs.AI · arxiv.org