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%。
正文 · 原文
Abstract:Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. Our approach decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking to ensure logic-level alignment between candidates, eliminating the syntactic bias of surface-form metrics, (2) semantic routing that directs different claim types to appropriate verification strategies: symbolic solvers for logical claims and LLM ensembles for commonsense reasoning, and (3) precise logical error localization via Minimal Correction Subsets (MCS), which pinpoint the exact subset of claims to revise, transforming binary failure signals into actionable feedback. Our framework classifies claims by their logical status and aggregates multiple verification signals into a unified score with variance-based penalty. The system iteratively refines answers using structured feedback until acceptance criteria are met or convergence is achieved. This hybrid approach delivers formal guarantees where possible and consensus verification elsewhere, advancing trustworthy AI. With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2601.20055 [cs.CL] |
| (or arXiv:2601.20055v3 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2601.20055 arXiv-issued DOI via DataCite |
Submission history
From: Vikash Singh [view email]
[v1]
Tue, 27 Jan 2026 20:59:11 UTC (550 KB)
[v2]
Sat, 2 May 2026 03:45:31 UTC (554 KB)
[v3]
Sun, 11 Oct 2026 01:28:54 UTC (509 KB)
来源：arXiv cs.AI · arxiv.org