論文の概要: Making Written Theorems Explorable by Grounding Them in Formal Representations

• arxiv url: http://arxiv.org/abs/2604.02598v1
• Date: Fri, 03 Apr 2026 00:16:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-06 17:20:24.255164
• Title: Making Written Theorems Explorable by Grounding Them in Formal Representations
• Title（参考訳）: 形式表現による接地定理の探索
• Authors: Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head,
• Abstract要約: 形式化された表現の基盤となる説明は、静的テキストがサポートしているもの以上のインタラクティブなアベイランスを可能にすると論じる。 このアイデアを、LLMを用いて定理とその記述された証明をリーンに変換するシステムである探索可能な定理を用いて、数学的証明理解のためにインスタンス化する。 読者はこの証明をステップレベルの粒度で実行し、カスタム例や逆例をテストし、各ステップをブリッジする論理的依存関係をトレースすることができる。
• 参考スコア（独自算出の注目度）: 26.38291147763785
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.
• Abstract（参考訳）: LLMが生成した説明は、技術的なコンテンツをよりアクセスしやすくするが、インタラクティブにサポートできることには天井がある。 LLM出力は静的テキストであるため、実行やステップスルーはできない。 形式化された表現の基盤となる説明は、静的テキストがサポートしているもの以上のインタラクティブなアベイランスを可能にすると論じる。 私たちは、この概念を、探索可能な定理、LLMを使って定理とその証明書をLeanに翻訳するシステム、マシンチェックされた証明のためのプログラミング言語、という数学的証明理解のアイデアをインスタンス化し、その証明書をLeanコードとリンクします。 読者はこの証明をステップレベルの粒度で実行し、カスタム例や逆例をテストし、各ステップをブリッジする論理的依存関係をトレースすることができる。 各ワークアウトステップは、その例でリーン証明を実行し、その中間状態を抽出することで作成されます。 証明読解タスクでは、提供された探索可能性機能にアクセスできた参加者は、より良く、より正しく、より詳細な回答を提供し、基礎となる数学のより深い全体的な理解を示します。

関連論文リスト

• Theorem-of-Thought: A Multi-Agent Framework for Abductive, Deductive, and Inductive Reasoning in Language Models [2.172419551358714]
  大規模言語モデル(LLM)は、自然言語推論タスク全体で強いパフォーマンスを示しているが、その推論プロセスは脆弱で解釈が難しいままである。 Theorem-of-Thought (ToTh)は、3つの並列エージェント間の協調として推論をモデル化する新しいフレームワークである。 シンボリック(WebOfLies)と数値(MultiArithm)の推論ベンチマークの実験は、ToThがCoT、セルフ一貫性、CoT-デコーディングを一貫して上回っていることを示している。
  論文  参考訳（メタデータ） (2025-06-08T12:28:38Z)
• 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 Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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