論文の概要: ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning

• arxiv url: http://arxiv.org/abs/2604.06401v1
• Date: Tue, 07 Apr 2026 19:33:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-09 17:30:51.209117
• Title: ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
• Title（参考訳）: ProofSketcher:Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
• Authors: Kranthi Kommuru, Kunal Khanvilkar, Gaurav Parekh,
• Abstract要約: 大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。 LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields, although such argument often includes some minor missteps, including the entire omission of side conditions, invalid inference patterns, or appeals to a lemma that cannot be derived logically out of the context being discussed. These omissions are infamously hard to notice solely out of the text, as even the misconstrued construction still may seem mostly accurate. Conversely, interactive theorem provers like Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program which is a small trusted kernel of the language type-checks with. Despite the fact that this technique provides strong guarantees, it comes at quite a heavy price: the evidence must be completely formalized, and the evidence user or a auxiliary search program must provide an avalanche of low-level information. This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
• Abstract（参考訳）: 大きな言語モデル(LLM)は、数学的および論理的分野において説得力のある議論を生み出すかもしれないが、そのような議論には、サイド条件の完全な省略、無効な推論パターン、あるいは議論される文脈から論理的に導出できない補題へのアピールなど、いくつかの小さな誤りを含むことが多い。 これらの欠落は、テキストからのみに気づくことが悪名高いが、誤解された構成でさえも、ほとんど正確であるように思える。 逆に、LeanやCoqのようなインタラクティブな定理証明者は、言語型チェックの小さな信頼できるカーネルであるプログラムにおいて、構文的および意味論的ステートメントがすべての構文的および意味的なステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 証拠は完全に形式化されなければならないし、エビデンスユーザまたは補助的な検索プログラムは、低レベルの情報の雪崩を提供する必要がある。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。

関連論文リスト

• Making Written Theorems Explorable by Grounding Them in Formal Representations [26.38291147763785]
  形式化された表現の基盤となる説明は、静的テキストがサポートしているもの以上のインタラクティブなアベイランスを可能にすると論じる。 このアイデアを、LLMを用いて定理とその記述された証明をリーンに変換するシステムである探索可能な定理を用いて、数学的証明理解のためにインスタンス化する。 読者はこの証明をステップレベルの粒度で実行し、カスタム例や逆例をテストし、各ステップをブリッジする論理的依存関係をトレースすることができる。
  論文  参考訳（メタデータ） (2026-04-03T00:16:52Z)
• HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs [32.234133057592935]
  Hermesはツール支援エージェントで、リーンシステムにおける検証段階と非公式な推論をインターリーブする。 パラメータスケールの異なる LLM を用いて,Hermes を4つの挑戦的数学的推論ベンチマークで評価する。
  論文  参考訳（メタデータ） (2025-11-24T04:50:18Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
  論文  参考訳（メタデータ） (2025-10-17T14:20:50Z)
• 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)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)

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

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