論文の概要: Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning
- arxiv url: http://arxiv.org/abs/2510.01069v1
- Date: Wed, 01 Oct 2025 16:06:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-03 16:59:20.659883
- Title: Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning
- Title（参考訳）: Typed Chain-of-Thought: LLM推論検証のためのカレーホワードフレームワーク
- Authors: Elija Perrier,
- Abstract要約: CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。
本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。
我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: While Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models, the faithfulness of the generated rationales remains an open problem for model interpretability. We propose a novel theoretical lens for this problem grounded in the Curry-Howard correspondence, which posits a direct relationship between formal proofs and computer programs. Under this paradigm, a faithful reasoning trace is analogous to a well-typed program, where each intermediate step corresponds to a typed logical inference. We operationalise this analogy, presenting methods to extract and map the informal, natural language steps of CoT into a formal, typed proof structure. Successfully converting a CoT trace into a well-typed proof serves as a strong, verifiable certificate of its computational faithfulness, moving beyond heuristic interpretability towards formal verification. Our framework provides a methodology to transform plausible narrative explanations into formally verifiable programs, offering a path towards building more reliable and trustworthy AI systems.
- Abstract（参考訳）: CoT(Chain-of-Thought)の促進は、大きな言語モデルの推論能力を高めるが、生成された論理の忠実さは、モデル解釈可能性のオープンな問題のままである。
本稿では,Curry-Howard対応に基礎を置き,形式証明とコンピュータプログラムの直接的な関係を示唆する新たな理論レンズを提案する。
このパラダイムの下では、忠実な推論トレースは、それぞれの中間ステップが型付き論理推論に対応する well-typed プログラムに類似する。
我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
CoTトレースを十分に型付けされた証明に変換することは、その計算忠実性の強い検証可能な証明として機能し、ヒューリスティックな解釈可能性を超えて形式的検証へと移行する。
我々のフレームワークは、もっともらしい物語の説明を形式的に検証可能なプログラムに変換するための方法論を提供し、より信頼性が高く信頼性の高いAIシステムを構築するための道筋を提供する。
関連論文リスト
- StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。
StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。
StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
論文 参考訳（メタデータ） (2025-06-12T10:31:23Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。
訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。
トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
論文 参考訳（メタデータ） (2025-04-28T19:25:29Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。