arXiv cs.AI· Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless·· 3 天前AI 评分31
VERGE：面向可验证 LLM 推理的形式化精化与引导引擎
VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
AI 导读
VERGE 是一个神经符号框架，将 LLM 与 SMT 求解器结合，通过迭代精化生成经形式化验证的答案。它把 LLM 输出拆解为原子断言并自动形式化为一阶逻辑，用自动定理证明检查逻辑一致性，并引入多模型共识、语义路由和基于最小修正子集（MCS）的逻辑错误定位三项机制。在 GPT-OSS-120B 上，VERGE 在多个推理基准上收敛时平均性能较单次生成提升 18.7%。
正文 · AI 翻译
摘要：尽管大型语言模型（LLM）在句法上流畅，但在高风险领域确保其逻辑正确性仍是一项根本性挑战。我们提出了一种神经符号框架，将 LLM 与 SMT 求解器相结合，通过迭代细化生成验证引导的答案。我们的方法将 LLM 输出分解为原子声明，将其自动形式化为一阶逻辑，并使用自动定理证明验证其逻辑一致性。我们引入了三项关键创新：（1）通过形式语义等价检查实现多模型共识，以确保候选之间的逻辑层面一致性，消除表面形式指标的句法偏差；（2）语义路由，将不同类型的声明导向适当的验证策略：逻辑声明使用符号求解器，常识推理使用 LLM 集成；（3）通过最小修正子集（MCS）进行精确的逻辑错误定位，精确定位需要修正的确切声明子集，将二元失败信号转化为可操作的反馈。我们的框架根据声明的逻辑状态对其进行分类，并将多个验证信号聚合为带有基于方差的惩罚的统一分数。系统使用结构化反馈迭代细化答案，直到满足接受标准或达到收敛。这种混合方法在可能的情况下提供形式保证，在其他情况下提供共识验证，推动可信 AI 的发展。在 GPT-OSS-120B 模型上，VERGE 在一组推理基准测试中，与单次通过方法相比，在收敛时平均性能提升 18.7%。
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI） |
| 引用为： | arXiv:2601.20055 [cs.CL] |
| （或 arXiv:2601.20055v3 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2601.20055 arXiv 颁发的 DOI 通过 DataCite |
提交历史
来自：Vikash Singh [查看电子邮件]
[v1]
2026年1月27日星期二 20:59:11 UTC（550 KB）
[v2]
2026年5月2日星期六 03:45:31 UTC（554 KB）
[v3]
2026年10月11日星期日 01:28:54 UTC（509 KB）
来源：arXiv cs.AI · arxiv.org