論文の概要: FIMO: A Challenge Formal Dataset for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2309.04295v2
• Date: Tue, 5 Dec 2023 08:38:01 GMT
• ステータス: 処理完了
• システム内更新日: 2023-12-06 19:46:05.704040
• Title: FIMO: A Challenge Formal Dataset for Automated Theorem Proving
• Title（参考訳）: FIMO: 自動定理証明のための挑戦形式データセット
• Authors: Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, Qun Liu
• Abstract要約: FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。 公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
• 参考スコア（独自算出の注目度）: 31.695624833932577
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed to facilitate advanced automated theorem proving at the IMO level, FIMO is currently tailored for the Lean formal language. It comprises 149 formal problem statements, accompanied by both informal problem descriptions and their corresponding LaTeX-based informal proofs. Through initial experiments involving GPT-4, our findings underscore the existing limitations in current methodologies, indicating a substantial journey ahead before achieving satisfactory IMO-level automated theorem proving outcomes.
• Abstract（参考訳）: IMO(International Mathematical Olympiad)ショートリスト問題から得られる公式な数学的問題文からなる革新的なデータセットFIMOを提案する。 IMOレベルでの高度な自動定理の証明を容易にするために設計されたFIMOは現在、Lean形式言語用に調整されている。 149の形式的問題文と、形式的問題記述と、それに対応するラテックスに基づく形式的証明の両方からなる。 GPT-4に関する最初の実験を通じて,本研究は既存の手法の限界を浮き彫りにし,優れたIMOレベルの自動定理の証明に先立って大きな進歩をみせている。

関連論文リスト

• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• 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)
• Experimental results from applying GPT-4 to an unpublished formal language [0.0]
  最先端のシステムであるGPT-4は、未発表の形式システムのための簡潔な自然言語仕様を備えていた。 システムは全てのタスクを成功させ、広範なドメイン知識を示し、有用な新しい構文と意味論を発明し、一般化と推論能力を示した。
  論文  参考訳（メタデータ） (2023-05-20T14:00:08Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。 ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。 テキスト内学習による文の自動書式化のベースライン結果について報告する。
  論文  参考訳（メタデータ） (2023-02-24T03:28:46Z)
• Formal Mathematics Statement Curriculum Learning [64.45821687940946]
  同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。 また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
  論文  参考訳（メタデータ） (2022-02-03T00:17:00Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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