論文の概要: LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs

• arxiv url: http://arxiv.org/abs/2506.08321v1
• Date: Tue, 10 Jun 2025 01:12:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-11 15:11:40.965548
• Title: LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs
• Title（参考訳）: LeanTutor: 数学的証明のための形式的に検証されたAIチュータ
• Authors: Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade,
• Abstract要約: 本稿では,Large Language Model(LLM)に基づく算数証明学習システムであるLeanTutorを紹介する。 LeanTutorは自然言語で学生と対話し、Leanで学生が書いた数学の証明を正式に検証し、次のステップを正しく生成し、適切な指導指導を提供する。 本システムを評価するために,自然数ゲームから派生した人文データセットであるPeanoBenchを紹介した。
• 参考スコア（独自算出の注目度）: 7.468772576199917
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present LeanTutor, a Large Language Model (LLM)-based tutoring system for math proofs. LeanTutor interacts with the student in natural language, formally verifies student-written math proofs in Lean, generates correct next steps, and provides the appropriate instructional guidance. LeanTutor is composed of three modules: (i) an autoformalizer/proof-checker, (ii) a next-step generator, and (iii) a natural language feedback generator. The first module faithfully autoformalizes student proofs into Lean and verifies proof accuracy via successful code compilation. If the proof has an error, the incorrect step is identified. The next-step generator module outputs a valid next Lean tactic for incorrect proofs via LLM-based candidate generation and proof search. The feedback generator module leverages Lean data to produce a pedagogically-motivated natural language hint for the student user. To evaluate our system, we introduce PeanoBench, a human-written dataset derived from the Natural Numbers Game, consisting of 371 Peano Arithmetic proofs, where each natural language proof step is paired with the corresponding logically equivalent tactic in Lean. The Autoformalizer correctly formalizes 57% of tactics in correct proofs and accurately identifies the incorrect step in 30% of incorrect proofs. In generating natural language hints for erroneous proofs, LeanTutor outperforms a simple baseline on accuracy and relevance metrics.
• Abstract（参考訳）: 本稿では,Large Language Model (LLM) を用いた算数証明学習システムであるLeanTutorを紹介する。 LeanTutorは自然言語で学生と対話し、Leanで学生が書いた数学の証明を正式に検証し、次のステップを正しく生成し、適切な指導指導を提供する。 LeanTutorは3つのモジュールで構成されています。 (i)オートフォーマライザ/防犯チェック装置 (ii)次段発生器、及び (iii)自然言語フィードバックジェネレータ。 最初のモジュールは生徒の証明をリーンに忠実に自己形式化し、コードコンパイルを成功させることで証明の正確さを検証する。 証明に誤りがある場合、誤ったステップが特定される。 次のステップジェネレータモジュールは、LLMベースの候補生成と証明検索を通じて、誤った証明のための有効な次のリーン戦術を出力する。 フィードバックジェネレータモジュールは、Leanデータを活用して、学生ユーザに教育的な動機付けを持つ自然言語ヒントを生成する。 本システムを評価するために,371個のペアノ算術証明からなる自然数ゲームから派生した人文データセットであるPeanoBenchを導入し,各自然言語証明ステップをリーンの論理的に等価な戦術と組み合わせた。 Autoformalizerは正しい証明で57%の戦術を正しく定式化し、不正な証明の30%で間違ったステップを正確に識別する。 誤った証明のための自然言語ヒントを生成する場合、LeanTutorは正確性と関連性メトリクスの単純なベースラインを上回ります。

関連論文リスト

• 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)
• A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems [0.0]
  リーンの残りのIMO問題に対する完全な、オリジナルの公式な証明を書いています。 この取り組みは,5,880行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。
  論文  参考訳（メタデータ） (2024-11-28T02:50:42Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。 ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。 テキスト内学習による文の自動書式化のベースライン結果について報告する。
  論文  参考訳（メタデータ） (2023-02-24T03:28:46Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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