論文の概要: VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
- arxiv url: http://arxiv.org/abs/2601.20055v1
- Date: Tue, 27 Jan 2026 20:59:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-29 15:46:06.662067
- Title: VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
- Title（参考訳）: VERGE:検証LDM推論のための形式的リファインメントとガイダンスエンジン
- Authors: Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless,
- Abstract要約: 本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。
本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。
GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
- 参考スコア（独自算出の注目度）: 4.3414302048068745
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- 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.
- Abstract（参考訳）: LLM(Large Language Models)の構文的流行にもかかわらず、高い領域における論理的正当性を保証することは、依然として根本的な課題である。
本稿では, LLM と SMT ソルバを組み合わせることで, 反復的改善による検証誘導型回答を生成するニューロシンボリック・フレームワークを提案する。
提案手法は LLM の出力を原子的クレームに分解し,それらを一階述語論理に自動変換し,その論理的一貫性を自動定理証明を用いて検証する。
提案手法では,(1)形式的意味論的同値性チェックによる論理レベルの整合性確保,(2)論理的クレームを適切な検証戦略に導く意味的ルーティング,(3)論理的クレームのシンボリックソルバ,そして(3)最小補正サブセット(MCS)による正確な論理的誤りローカライゼーション,(2)二項故障信号の正確なサブセットを修正可能なフィードバックに変換する,という3つの重要なイノベーションを紹介する。
本フレームワークは,複数の検証信号を分散に基づくペナルティ付き統一スコアに集約し,その論理的ステータスでクレームを分類する。
このシステムは、受け入れ基準を満たすか収束を達成するまで、構造化されたフィードバックを用いて回答を反復的に洗練する。
このハイブリッドアプローチは、可能な場所で正式な保証とコンセンサス検証を提供し、信頼できるAIを前進させる。
GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
関連論文リスト
- Memorization, Emergence, and Explaining Reversal Failures: A Controlled Study of Relational Semantics in LLMs [43.414287127130684]
本稿では,対称/逆三重項からテキストを生成する合成フレームワークを提案し,GPTスタイルの自己回帰モデルをスクラッチから訓練し,記憶,論理推論,文脈内一般化を評価する。
浅層(2-3層)モデルにおいても,関係性セマンティクスが十分な論理量制御によって出現し,その一般化が安定な中間層信号と一致していることが判明した。
論文 参考訳（メタデータ） (2026-01-06T11:20:38Z) - Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。
FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。
本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
論文 参考訳（メタデータ） (2026-01-06T02:51:56Z) - Formal that "Floats" High: Formal Verification of Floating Point Arithmetic [0.0]
本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。
この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。
その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
論文 参考訳（メタデータ） (2025-12-07T14:03:44Z) - Less Is More for Multi-Step Logical Reasoning of LLM Generalisation Under Rule Removal, Paraphrasing, and Compression [3.3492355863487275]
大規模言語モデル(LLM)は多くの自然言語処理において高い性能を達成するが、論理規則系の構造的摂動下での一般化は依然として不十分である。
本研究では,4つの応力試験による推理信頼性の検証を行う制御評価フレームワークを提案する。
論文 参考訳（メタデータ） (2025-12-06T10:49:50Z) - seqBench: A Tunable Benchmark to Quantify Sequential Reasoning Limits of LLMs [1.0519693622157462]
我々は,Large Language Models (LLMs) における逐次推論限界を探索するベンチマークであるseqBenchを紹介する。
検索の複雑さが最小限であるにもかかわらず、セクベンチの構造的推論タスクでは、トップパフォーマンスモデルでさえ体系的に失敗することがわかった。
論文 参考訳（メタデータ） (2025-09-21T01:32:13Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - Explainable Rule Application via Structured Prompting: A Neural-Symbolic Approach [0.0]
大規模言語モデル(LLM)は複雑な推論タスクでは優れているが、一貫性のあるルールアプリケーション、例外処理、説明可能性に苦慮している。
本稿では、推論を3つの検証可能なステップ(エンティティ識別、プロパティ抽出、シンボリックルール適用)に分解する構造化プロンプトフレームワークを提案する。
論文 参考訳（メタデータ） (2025-06-19T14:14:01Z) - CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。
我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
論文 参考訳（メタデータ） (2025-06-05T17:02:52Z) - Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
Retrieval-augmented Generation (RAG) は知識基底型大規模言語モデル(LLM)を実現するためのパラダイムとして広く採用されている。
RAGパイプラインは、モデル推論が得られた証拠と整合性を維持するのに失敗することが多く、事実上の矛盾や否定的な結論につながる。
批判駆動アライメント(CDA)に基づく新しい反復的枠組みであるAlignRAGを提案する。
AlignRAG-autoは、動的に洗練を終了し、批判的な反復回数を事前に指定する必要がなくなる自律的な変種である。
論文 参考訳（メタデータ） (2025-04-21T04:56:47Z) - Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
本稿では,直接推論 (DR) と間接推論 (IR) を並列な複数の推論経路として考慮し,最終解を導出する直接間接推論 (DIR) 手法を提案する。
我々のDIR法は単純だが有効であり、既存のCoT法と簡単に統合できる。
論文 参考訳（メタデータ） (2024-02-06T03:41:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。