論文の概要: math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories

• arxiv url: http://arxiv.org/abs/2310.17064v1
• Date: Wed, 25 Oct 2023 23:54:04 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-27 22:56:29.020253
• Title: math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories
• Title（参考訳）: Math-PVS:科学論文をPVS理論にマップする大規模言語モデルフレームワーク
• Authors: Hassen Saidi, Susmit Jha, Tuhin Sahai
• Abstract要約: 本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
• 参考スコア（独自算出の注目度）: 10.416375584563728
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As artificial intelligence (AI) gains greater adoption in a wide variety of applications, it has immense potential to contribute to mathematical discovery, by guiding conjecture generation, constructing counterexamples, assisting in formalizing mathematics, and discovering connections between different mathematical areas, to name a few. While prior work has leveraged computers for exhaustive mathematical proof search, recent efforts based on large language models (LLMs) aspire to position computing platforms as co-contributors in the mathematical research process. Despite their current limitations in logic and mathematical tasks, there is growing interest in melding theorem proving systems with foundation models. This work investigates the applicability of LLMs in formalizing advanced mathematical concepts and proposes a framework that can critically review and check mathematical reasoning in research papers. Given the noted reasoning shortcomings of LLMs, our approach synergizes the capabilities of proof assistants, specifically PVS, with LLMs, enabling a bridge between textual descriptions in academic papers and formal specifications in PVS. By harnessing the PVS environment, coupled with data ingestion and conversion mechanisms, we envision an automated process, called \emph{math-PVS}, to extract and formalize mathematical theorems from research papers, offering an innovative tool for academic review and discovery.
• Abstract（参考訳）: 人工知能(AI)が多種多様な応用で広く採用されるにつれて、予想生成の導出、反例の構築、数学の形式化の支援、異なる数学領域間の関係の発見などにより、数学的な発見に寄与する大きな可能性を秘めている。 先行研究はコンピュータを徹底的な数学的証明探索に活用したが、近年の大規模言語モデル(llm)に基づく取り組みは、数学的研究プロセスにおいて、コンピューティングプラットフォームを共同供給者として位置づけることを目指している。 論理学や数学のタスクにおける現在の制限にもかかわらず、基礎モデルによる定理証明システムへの関心が高まっている。 本研究は、高度な数学的概念の形式化におけるllmの適用可能性を調査し、研究論文で数学的推論を批判的にレビューしチェックできる枠組みを提案する。 LLMの欠点が指摘されていることから,本手法は,学術論文のテキスト記述とPVSの形式仕様との橋渡しを可能とし,証明アシスタント,特にPVSとLLMを連携させる。 PVS環境とデータ取り込みと変換機構を組み合わせることで、研究論文から数学的定理を抽出・形式化し、学術的なレビューと発見のための革新的なツールを提供する「emph{math-PVS}」と呼ばれる自動化プロセスを構想する。

関連論文リスト

• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  大規模言語モデル(LLM)は、証明システム内で証明ステップを生成することによって、数学的定理を正式に証明することができる。 本稿では,LLMが学習した数学的直観と,記号的手法によって符号化された領域固有の洞察を相乗化する,ニューロシンボリック・戦術生成器を提案する。 複数の数学コンペティションから161の挑戦的不等式を評価する。
  論文  参考訳（メタデータ） (2025-02-19T15:54:21Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
  我々は、関連する数学的文脈でモデルにクエリを補足する知識ベースであるLemmaHeadを開発した。 数学的推論におけるモデルの性能を測定するため、我々のテストパラダイムは自動定理証明の課題に焦点を当てている。
  論文  参考訳（メタデータ） (2025-01-27T05:46:06Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  この研究は、数学的推論における重要なギャップに対処し、信頼できるAIの進歩に寄与する。 DEMI-MathAnalysisデータセットを開発した。 また,LLMの問題解決能力を高めるためのガイドフレームワークも設計した。
  論文  参考訳（メタデータ） (2024-12-28T20:37:55Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
  MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。 MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
  論文  参考訳（メタデータ） (2024-05-20T17:52:29Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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