arXiv cs.AI· Debargha Ganguly, Weicong Chen, Mohsen Hariri, Vikash Singh, Sreehari Sankar, Shouren Wang, Wang Yang, Biyao Zhang, Chaoda Song, Alexander Nemecek, Kai Ye, Osama Zafar, Erman Ayday, Joe Stubbs, Srinivasan Iyengar, Vipin Chaudhary·· 3 天前AI 评分41
Sequent-Prover：训练基于 SMT 的形式化可验证推理智能体
Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
AI 导读
Sequent-Prover 是一族使用验证器的语言模型智能体，在可执行的 SMT-LIB 草稿本中推理，通过多轮查询 Z3、检查求解器反馈并修复形式化，最终给出显式答案。
正文 · AI 翻译
作者：Debargha Ganguly、Weicong Chen、Mohsen Hariri、Vikash Singh、Sreehari Sankar、Shouren Wang、Wang Yang、Biyao Zhang、Chaoda Song、Alexander Nemecek、Kai Ye、Osama Zafar、Erman Ayday、Joe Stubbs、Srinivasan Iyengar、Vipin Chaudhary
摘要：我们提出 Sequent-Prover，一个使用验证器的语言模型智能体系列，以及产生它们的后训练框架。智能体在可执行的 SMT-LIB 草稿本中推理：它们编写完整的 SMT-LIB 程序，跨轮次查询 Z3，检查求解器反馈，修复形式化，并以显式答案终止。我们的方法——验证器条件轨迹蒸馏——从带噪的教师提议策略出发，通过采样多轮轨迹进行自举，保留正确、非平凡、有依据且可执行的成功尾部，然后应用监督微调和轨迹级偏好优化。由于求解器成功本身并不能保证语义忠实性，我们评估任务准确率、k 样本可靠性和 SMT 程序质量。在 37 个基准和每个模型系列 7,254 个问题上，后训练将 4B 模型的单次尝试准确率从 85.6% 提升到 97.0%，将四样本全对可靠性（pass^4）从 64.1% 提升到 91.7%。它还将平均 SMT 调用次数从 4.10 减少到 2.52，将每次尝试的 token 数从 18.97k 减少到 12.72k。Sequent-Prover 智能体给出的答案由可执行的形式化产物支撑。
| 学科： | 计算与语言（cs.CL）；人工智能（cs.AI）；机器学习（cs.LG）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.15258 [cs.CL] |
| （或 arXiv:2610.15258v1 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.15258 arXiv 颁发的 DOI 经由 DataCite（待注册） |
提交历史
来自：Debargha Ganguly [查看邮箱]
[v1]
2026年10月11日星期日 01:10:19 UTC（2,866 KB）
来源：arXiv cs.AI · arxiv.org