VERGE: 検証可能な大規模言語モデル推論のための形式的精緻化とガイダンスエンジン

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

January 27, 2026

著者: Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless

cs.AI

要旨

大規模言語モデル（LLM）の構文的流暢さにもかかわらず、高リスク領域における論理的正確性を保証することは依然として根本的な課題である。本論文は、LLMとSMTソルバーを組み合わせ、反復的な洗練を通じて検証誘導型の回答を生成する神経記号論的フレームワークを提案する。本アプローチでは、LLMの出力を原子主張に分解し、一階述語論理へ自動形式化し、自動定理証明を用いてそれらの論理的整合性を検証する。我々は三つの重要な革新を導入する：（1）形式的意味等価性検査によるマルチモデル合意により、候補間の論理レベルでの整合性を確保し、表層形式指標の構文的バイアスを排除する、（2）異なる主張タイプを適切な検証戦略に振り分ける意味的ルーティング：論理的主张には記号的ソルバーを、常識的推論にはLLMアンサンブルを適用する、（3）最小修正部分集合（MCS）による精密な論理誤り局在化。これは修正すべき主張の正確な部分集合を特定し、二値的失敗信号を実践的フィードバックへ変換する。本フレームワークは主張を論理状態に基づき分類し、複数の検証信号を分散ベースのペナルティを伴う統一スコアに集約する。システムは構造化フィードバックを用いて回答を反復的に洗練し、受容基準が満たされるか収束が達成されるまで継続する。このハイブリッドアプローチは、可能な場合には形式的保証を、それ以外の場合は合意検証を提供し、信頼できるAIを推進する。GPT-OSS-120Bモデルを用いたVERGEは、一連の推論ベンチマークにおいて、単一パスアプローチと比較して収束時平均18.7%の性能向上を示した。

English

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.