論文の概要: Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

• arxiv url: http://arxiv.org/abs/2409.05977v3
• Date: Fri, 08 Nov 2024 16:42:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-11 14:52:31.522401
• Title: Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
• Title（参考訳）: リーン4の異なる分野における数学的形式化された問題解決と定理証明
• Authors: Xichen Tang,
• Abstract要約: 本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Formalizing mathematical proofs using computerized verification languages like Lean 4 has the potential to significantly impact the field of mathematics, it offers prominent capabilities for advancing mathematical reasoning. However, existing efforts are largely limited to creating formalized versions of proofs from extensive online mathematical corpora, struggling to keep pace with the rapidly evolving nature of mathematics. To bridge the gap between traditional and computerized proof techniques, this paper explores the use of Large Language Models (LLMs) to generate formal proof steps and complete formalized proofs. By converting natural language (NL) mathematical proofs into formalized versions, this work introduces the basic structure and tactics of the Lean 4 language. The goal is to determine how AI can be leveraged to assist the mathematical formalization process and improve its performance. Several examples are provided that demonstrate solving problems using both traditional and Lean 4-based approaches. Ultimately, this paper presents an explanation of the foundations of Lean 4 and comparative analyses of the mathematical formalization process using traditional and AI-augmented techniques. The findings indicate that AI- powered tools have significant potential to accelerate and enhance the formalization of mathematical proofs, paving the way for more efficient and reliable theorem-proving for AI for Math in the future.
• Abstract（参考訳）: リーン4のようなコンピュータ検証言語を用いた数学的証明の形式化は、数学の分野に大きな影響を与える可能性がある。 しかし、既存の取り組みは、広範囲のオンライン数学的コーパスから証明の形式化されたバージョンを作成することに限定されており、急速に進化する数学の性質に追従するのに苦労している。 本稿では,従来の証明手法と計算機による証明手法のギャップを埋めるために,形式的な証明ステップと完全形式化された証明を生成するためのLarge Language Models (LLMs) の利用について検討する。 自然言語(NL)の数学的証明を形式化されたバージョンに変換することで、この研究はLean 4言語の基本構造と戦術を紹介します。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。 従来の4つのアプローチとリーン4つのアプローチの両方を使って問題解決を実証するいくつかの例が提供されている。 最終的に,本論文では,リーン4の基礎と,従来のAI拡張技術を用いた数学的形式化プロセスの比較分析について述べる。 この結果は、AIを利用したツールが数学的証明の形式化を加速し、促進する大きな可能性を秘めており、将来的には数学のためのAIのためのより効率的で信頼性の高い定理証明の道を開くことを示唆している。

関連論文リスト

• LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
  我々は、関連する数学的文脈でモデルにクエリを補足する知識ベースであるLemmaHeadを開発した。 数学的推論におけるモデルの性能を測定するため、我々のテストパラダイムは自動定理証明の課題に焦点を当てている。
  論文  参考訳（メタデータ） (2025-01-27T05:46:06Z)
• 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)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages [0.0]
  形式数学は、数学をプログラミング言語に翻訳する分野である。 本稿では、5つの形式数学コーパスの微分機械学習性に関する最初の体系的定量的分析のための進化的枠組みを紹介する。
  論文  参考訳（メタデータ） (2024-02-12T19:10:11Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• 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)

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

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