論文の概要: LemmaHead: RAG Assisted Proof Generation Using Large Language Models

• arxiv url: http://arxiv.org/abs/2501.15797v4
• Date: Mon, 10 Feb 2025 05:31:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-11 14:27:37.712614
• Title: LemmaHead: RAG Assisted Proof Generation Using Large Language Models
• Title（参考訳）: LemmaHead: 大規模言語モデルを用いたRAG支援証明生成
• Authors: Tianbo Yang, Mingqi Yan, Hongyi Zhao, Tianshuo Yang,
• Abstract要約: 我々は、関連する数学的文脈でモデルにクエリを補足する知識ベースであるLemmaHeadを開発した。 数学的推論におけるモデルの性能を測定するため、我々のテストパラダイムは自動定理証明の課題に焦点を当てている。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consists of fine-tuning the model on written mathematical content such as academic publications and textbooks, so that the model can learn to emulate the style of mathematical writing. In this project, we explore the effectiveness of using retrieval augmented generation (RAG) to address gaps in the mathematical reasoning of LLMs. We develop LemmaHead, a RAG knowledge base that supplements queries to the model with relevant mathematical context, with particular focus on context from published textbooks. To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving via generating proofs to a given mathematical claim in the Lean formal language.
• Abstract（参考訳）: 数学的な問題を解くか、数学的証明を書くのに必要な論理を開発することは、大きな言語モデル(LLMS)にとってより難しい目標の1つである。 現在、文学における最も一般的な手法は、学術出版物や教科書などの数学的内容のモデルを微調整することで、モデルが数学的記述のスタイルをエミュレートすることを学べるようにしている。 本稿では,LLMの数学的推論におけるギャップに対処するために,検索拡張生成(RAG)の有効性について検討する。 本稿では,関係のある数学的文脈を持つモデルにクエリを補足するRAG知識ベースであるLemmaHeadを開発し,特に教科書の文脈に着目した。 数学的推論における我々のモデルの性能を測定するために、我々のテストパラダイムは、リーン形式言語における与えられた数学的主張に対する証明を生成することによって自動定理証明のタスクに焦点を当てている。

関連論文リスト

• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• Benchmarking Large Language Models for Math Reasoning Tasks [12.91916443702145]
  我々は、4つの強力な基礎モデル上の5つの広く使われている数学的データセットの数学的問題解決のための、最先端の文脈内学習アルゴリズムを7つ比較した。 以上の結果から, GPT-4o や LLaMA 3-70B のような大規模基盤モデルでは, 具体的なプロンプト戦略とは独立に数学的推論を解くことが可能であることが示唆された。 将来の研究で追加モデルの統合をサポートするために、ベンチマークコードをオープンソースにしています。
  論文  参考訳（メタデータ） (2024-08-20T13:34:17Z)
• MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
  MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。 MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
  論文  参考訳（メタデータ） (2024-05-20T17:52:29Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)
• Large Language Models as Analogical Reasoners [155.9617224350088]
  CoT(Chain-of- Thought)は、言語モデルのプロンプトとして、推論タスク全体で素晴らしいパフォーマンスを示す。 そこで本稿では,大規模言語モデルの推論プロセスを自動的にガイドする,新たなプロンプト手法であるアナログプロンプトを導入する。
  論文  参考訳（メタデータ） (2023-10-03T00:57:26Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• 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)

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

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