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

• arxiv url: http://arxiv.org/abs/2409.05977v2
• Date: Thu, 31 Oct 2024 16:01:59 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-07 22:27:40.728364
• Title: Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
• Title（参考訳）: リーン4の異なる分野における数学的形式化された問題解決と定理証明
• Authors: Xichen Tang,
• Abstract要約: 数学の定理を証明するためにLean 4のようなコンピュータ化された形式言語を使うことは、数学的形式化に大きな影響を与える。 本稿では、基本構造と戦術を概ね紹介し、AIが数学的形式化プロセスをどのように支援し、その性能を向上させるかを決定する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Using computerized verifiable formal languages like Lean 4 to prove mathematical theorems has a significant impact on mathematical formalization. Lean 4 offers prominent potential for advancing mathematical reasoning. However, existing efforts are limited to mathematical formalization languages in substantial online corpora and are dedicated to keeping pace with rapidly evolving languages. To bridge the gap between the traditional and computerized proof, my approach to formalizing theorem proving involves generating formal steps and complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. The method is to introduce the basic structure and tactics in general, determine how AI can assist the mathematical formalization process to improve its performance, and give examples of solving problems in Lean 4 comparing to NL, mainly in IMO, and a sample theorem proving in abstract algebra.
• Abstract（参考訳）: 数学の定理を証明するために、Lean 4のようなコンピュータで検証可能な形式言語を使うことは、数学的形式化に大きな影響を与える。 リーン4は、数学的推論を前進させる大きな可能性を提供します。 しかし、既存の取り組みは、実質的なオンラインコーパスにおける数学的形式化言語に限られており、急速に進化する言語とのペースを維持することに専念している。 従来の証明と計算機化された証明のギャップを埋めるために、私の定理証明へのアプローチは、自然言語(NL)の証明に基づいたLarge Language Models(LLM)を用いて形式的なステップと完全証明を生成することである。 この方法は、基本構造と戦術を一般に導入し、AIが数学的形式化プロセスをどのように支援し、その性能を改善するかを決定し、IMOを中心にしてNLと比較したLean 4の問題解決の例と抽象代数学で証明されたサンプル定理を提示する。

関連論文リスト

• 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)

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

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