論文の概要: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

• arxiv url: http://arxiv.org/abs/2302.12433v1
• Date: Fri, 24 Feb 2023 03:28:46 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-27 14:41:52.983740
• Title: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
• Title（参考訳）: proofnet: 学生レベルの数学の自己形式化と形式証明
• Authors: Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
• Abstract要約: 本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。 ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。 テキスト内学習による文の自動書式化のベースライン結果について報告する。
• 参考スコア（独自算出の注目度）: 7.607254619341369
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.
• Abstract（参考訳）: 本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。 ProofNetベンチマークは371の例で構成され、それぞれがLean 3の正式な定理文、自然言語の定理文、自然言語の証明で構成されている。 問題は、主に一般的な学部生の純粋数学の教科書から引き出され、実数や複素解析、線形代数、抽象代数学、トポロジーなどのトピックをカバーしている。 ProofNetは、自動形式化と自動定理証明の進歩を促す、挑戦的なベンチマークになる予定です。 文脈内学習による文の自動形式化に関する基礎的結果について報告する。 さらに, 迅速検索法と蒸留逆翻訳法という2つの新しいステートメント自動形式化手法を導入する。

関連論文リスト

• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  数学の定理を証明するためにLean 4のようなコンピュータ化された形式言語を使うことは、数学的形式化に大きな影響を与える。 本稿では、基本構造と戦術を概ね紹介し、AIが数学的形式化プロセスをどのように支援し、その性能を向上させるかを決定する。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• 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)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• 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)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)
• 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)

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

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