論文の概要: LeanTutor: Towards a Verified AI Mathematical Proof Tutor
- arxiv url: http://arxiv.org/abs/2601.17473v1
- Date: Sat, 24 Jan 2026 14:23:52 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-27 15:23:07.806356
- Title: LeanTutor: Towards a Verified AI Mathematical Proof Tutor
- Title（参考訳）: LeanTutor: 検証済みのAI数学的証明を目指す
- Authors: Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade,
- Abstract要約: LLMと定理証明器の相補的強度を組み合わせた概念証明システム(LeanTutor)を提案する。
LeanTutorは、3つのモジュールで構成されている: (i) オートフォーマライザ/プロテクションチェック、 (ii) 次ステップジェネレータ、 (iii) 自然言語フィードバックジェネレータ。
このシステムを評価するために,自然数ゲームから派生した人文自然言語と形式言語における371のペアノ算術的証明のデータセットであるPeanoBenchを紹介した。
- 参考スコア（独自算出の注目度）: 6.972720019122309
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper considers the development of an AI-based provably-correct mathematical proof tutor. While Large Language Models (LLMs) allow seamless communication in natural language, they are error prone. Theorem provers such as Lean allow for provable-correctness, but these are hard for students to learn. We present a proof-of-concept system (LeanTutor) by combining the complementary strengths of LLMs and theorem provers. LeanTutor is composed of three modules: (i) an autoformalizer/proof-checker, (ii) a next-step generator, and (iii) a natural language feedback generator. To evaluate the system, we introduce PeanoBench, a dataset of 371 Peano Arithmetic proofs in human-written natural language and formal language, derived from the Natural Numbers Game.
- Abstract（参考訳）: 本稿では,AIに基づく証明可能な数学的証明チューターの開発について考察する。
大規模言語モデル (LLM) は自然言語でのシームレスな通信を可能にするが、エラーを起こしやすい。
Leanのような理論の証明者は証明可能な正確さを許すが、これらは学生が学ぶのが難しい。
LLMと定理証明器の相補的な強みを組み合わせた概念証明システム(LeanTutor)を提案する。
LeanTutorは3つのモジュールで構成されています。
(i)オートフォーマライザ/防犯チェック装置
(ii)次段発生器、及び
(iii)自然言語フィードバックジェネレータ。
このシステムを評価するために,自然数ゲームから派生した人文自然言語と形式言語における371のペアノ算術的証明のデータセットであるPeanoBenchを紹介した。
関連論文リスト
- LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs [7.468772576199917]
本稿では,Large Language Model(LLM)に基づく算数証明学習システムであるLeanTutorを紹介する。
LeanTutorは自然言語で学生と対話し、Leanで学生が書いた数学の証明を正式に検証し、次のステップを正しく生成し、適切な指導指導を提供する。
本システムを評価するために,自然数ゲームから派生した人文データセットであるPeanoBenchを紹介した。
論文 参考訳（メタデータ） (2025-06-10T01:12:36Z) - 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) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳（メタデータ） (2023-10-16T08:42:39Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳（メタデータ） (2023-02-24T03:28:46Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - NaturalProver: Grounded Mathematical Proof Generation with Language
Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。
本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。
NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文 参考訳（メタデータ） (2022-05-25T17:01:18Z) - NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。
NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。
数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
論文 参考訳（メタデータ） (2021-03-24T03:14:48Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。