論文の概要: What Was Said, Not What Was 'Thought': Type-6 Logic for CoT Verification

• arxiv url: http://arxiv.org/abs/2609.38420v1
• Date: Tue, 29 Sep 2026 19:13:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-01 18:57:26.632878
• Title: What Was Said, Not What Was 'Thought': Type-6 Logic for CoT Verification
• Title（参考訳）: CoT 検証のための Type-6 ロジック
• Abstract要約: 2つの演算子で拡張された動的論理の変種であるType-6ロジックを導入する(不確かさと再発)。 Type-6は、ライセンスされていないリビジョン、エントロメム、ループバック、検証不可能/不正なクレームなど、一般的な推論の病因を説明できる。 本稿では,そのトレースをグラフ化したType-6論理に基づく検証器を提案し,それをType-6の公理や推論規則と比較する。
• 参考スコア（独自算出の注目度）: 12.037650994342664
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: We introduce Type-6 logic, a variant of dynamic epistemic logic augmented with two operators (uncertainty and recurrence), designed to model the inferential dynamics of contemporary large language model (LLM) chain-of-thought (CoT) reasoning. Type-6 accounts for common LLM reasoning pathologies such as unlicensed revision, enthymemes, loopbacks, and unverifiable/incorrect claims. We propose a verifier based on Type-6 logic that builds a graph out the trace, and checks it against Type-6's axioms and inference rules. We evaluate our framework on LLM-generated CoTs four splits spanning formal and informal reasoning. Our verifier detects structurally unsound reasoning steps that surface-level heuristics miss, and allows for easy visualisation of the model's reasoning process. In our corpus, our verifier shows that derived contradiction is the most common hard-fail category in CoT, and that only about 3\% of the propositions of a trace have impact on the final derivation. Ablation studies show that other verification methods (LLMs-as-judges, other neurosymbolic approaches, etc.) cannot be considered interchangeable: for example, agreement between LLMs-as-judges and LINC is $κ\approx 0.034$, and this persists within a method across underlying models. Type-6, however, is the most agreed-with method amongst the ones we tested. We prove our verifier runs on average-case linear time; and release our logic specification and artefacts.
• Abstract（参考訳）: 現代大言語モデル (LLM) チェーン・オブ・シント (CoT) 推論の推論をモデル化するための2つの演算子(不確かさと再帰性)を付加した動的認識論理の変種であるType-6ロジックを導入する。 Type-6は、ライセンスされていないリビジョン、エントロメム、ループバック、検証不可能/不正なクレームなど、一般的なLCM推論の病因を説明できる。 本稿では,そのトレースをグラフ化したType-6論理に基づく検証器を提案し,それをType-6の公理や推論規則と比較する。 フォーマルな推論と非公式な推論にまたがる4つの分割をLCMで生成するCoTの枠組みについて検討した。 我々の検証器は、表面レベルのヒューリスティックスが見逃す構造的無音推論ステップを検出し、モデルの推論プロセスを簡単に可視化することができる。 我々のコーパスでは、導出矛盾がCoTの最も一般的なハードフェイルカテゴリであり、トレースの命題の約3倍しか最終導出に影響を与えないことを示す。 アブレーション研究では、他の検証方法(LLMs-as-judges、その他のニューロシンボリックアプローチなど)は交換可能とみなせないことが示されており、例えば、LLMs-as-judgesとLINCの合意は、κ\approx 0.034$であり、基礎となるモデルにまたがるメソッド内で持続する。 しかし、私たちがテストした中では、Type 6が最も合意されたメソッドです。 検証は平均ケースの線形時間で実行され、論理仕様とアーティファクトがリリースされます。

関連論文リスト

• The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics [0.9668407688201359]
  チェーン・オブ・思想(CoT)推論は、大きな言語モデル(LLM)のパフォーマンスを改善する。 言語化されたCoTを利用して推論の正しさをモニタリングする既存のアプローチは、個々の中間ステップの意味的正しさまたは整合性を大きく評価する。 機能障害は、可視的推論の構造において、タスク依存の分散変化として表れることを示す。
  論文  参考訳（メタデータ） (2026-08-04T08:04:36Z)
• ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics [3.848983210046659]
  我々は Martin-Lof Dependent Type (MLTT) の保守的な拡張である ZX-Calculus (Knowledge Evolution Calculus) を提案する。 これは、トレースインデクシングされたタイプ、プレシーフ非モノトーン意味論、建設的なAGM信条修正を統合している。 Coq の機械化は論文に付随する(34の完全証明、0は2つの中心的な結果を認めている)。
  論文  参考訳（メタデータ） (2026-06-02T02:51:41Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。 本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。 我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
  論文  参考訳（メタデータ） (2026-01-30T07:01:25Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。 本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。 GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
  論文  参考訳（メタデータ） (2026-01-27T20:59:11Z)
• ARCHE: A Novel Task to Evaluate LLMs on Latent Reasoning Chain Extraction [70.53044880892196]
  本稿では、複雑な推論引数を標準推論パラダイムの組み合わせに分解し、Reasoning Logic Tree (RLT) という形で分解しなければならない、ARCHE(Latent Reasoning Chain extract)という新しいタスクを紹介する。 この作業を容易にするために,我々は,1,900以上の参照と38,000の視点を含む70のNature Communicationsの記事から得られた新しいベンチマークであるARCHE Benchをリリースする。 ARCHE Bench上での10のLLMの評価では、モデルがREAとECのトレードオフを示しており、完全な標準推論チェーンを抽出することはできません。
  論文  参考訳（メタデータ） (2025-11-16T07:37:09Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
  大型言語モデル (LLM) は, CoT (Chain-of-Thought) による数学的問題に対して高い性能を示す 我々は、有向非巡回グラフ(DAG)上の一定の規則に基づくプロセスとしてCoTをモデル化することを提案する。 ここでは,モデルのCoT軌道がDAG構造にどの程度よく依存するかを定量化する計量である論理的近接性を導入する。
  論文  参考訳（メタデータ） (2025-10-19T21:05:17Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。 本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。 我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
  論文  参考訳（メタデータ） (2025-10-01T16:06:40Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• Zero-Shot Verification-guided Chain of Thoughts [64.862738244735]
  我々は,COTプロンプトによる自己生成推論ステップの自己検証に着目する。 この設定を探索するため、我々はCOT STEPと呼ばれる新しいゼロショットプロンプトを設計し、推論ステップのゼロショット分解を支援する。 我々は,検証者の推論連鎖の正しさを分類する能力を評価し,推論の導出に検証者のスコアを使用する方法を探究する。
  論文  参考訳（メタデータ） (2025-01-21T03:52:54Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。