論文の概要: 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のためのより効率的で信頼性の高い定理証明の道を開くことを示唆している。
関連論文リスト
- Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - 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) - 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) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳（メタデータ） (2022-11-14T16:52:32Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。