論文の概要: A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems

• arxiv url: http://arxiv.org/abs/2411.18872v1
• Date: Thu, 28 Nov 2024 02:50:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-02 15:19:31.399454
• Title: A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems
• Title（参考訳）: 国際数学オリンピックのためのリーンデータセット - 難しい問題に対する数学の証明を書くための小さなステップ
• Authors: Roozbeh Yousefzadeh, Xuenan Cao,
• Abstract要約: IMO 2022と2023の3つの余分な問題とともに、Leanの残りの13のIMO問題に対する完全な、オリジナルの公式な証明を書いています。 論文の目的は、MiniF2F以降のすべてのIMO問題の正式な証明を自動で書けるAIモデルを開発するための道を開くことである。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the proofs in formal language can be challenging for humans and machines. The miniF2F benchmark has 20 IMO problems in its testing set, yet formal proofs are available only for 7 of these problems (3 of which are written only by mathematicians). The model with best accuracy can only prove 4 of these 20 IMO problems, from 1950s and 60s, while its training set is a secret. In this work, we write complete, original formal proofs for the remaining 13 IMO problems in Lean along with 3 extra problems from IMO 2022 and 2023. This effort expands the availability of proof currently in the public domain by creating 5,150 lines of Lean proof. The goal of the paper is to pave the way for developing AI models that can automatically write the formal proofs for all the IMO problems in miniF2F and beyond. In this pursuit, we devise a method to decompose the proof of these problems into their building blocks, constructing a dataset of about 900 lemmas with 25,500 lines of Lean code. These lemmas are not trivial, yet they are approachable, providing the opportunity to evaluate and diagnose the failures and successes of AI models. We then evaluate the ability of GPT-4 in writing formal proofs for these lemmas with zero shot prompting, CoT reasoning and lemma retrieval. In evaluating the responses, we also analyze the confounding factor of LLM's ability to write the proofs in natural language vs Lean language.
• Abstract（参考訳）: 数学的な問題に対する公式な証明を書くためにAIを使うことは、近年進歩している課題である。 Leanのような自動システムは、形式言語で書かれた証明の正しさを検証することができるが、形式言語で証明を書くことは人間や機械にとって難しい。 miniF2Fベンチマークはテストセットに20のIMO問題があるが、公式な証明は7つの問題に対してのみ利用可能である(うち3つは数学者によってのみ記述されている)。 最良の精度を持つモデルは、1950年代から60年代にかけての20のIMOのうち4つしか証明できないが、トレーニングセットは秘密である。 本稿では、リーンにおける13のIMO問題と、2022年と2023年の3つの追加の問題について、完全な、オリジナルの公式な証明を書いています。 この取り組みは,5,150行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。 論文の目的は、MiniF2F以降のすべてのIMO問題の正式な証明を自動で書けるAIモデルを開発するための道を開くことである。 この追求において、我々は、これらの問題の証明をビルディングブロックに分解する方法を考案し、約900のレムマと25,500行のリーンコードからなるデータセットを構築しました。 これらの補題は簡単ではないが、アプローチ可能であり、AIモデルの失敗と成功を評価し診断する機会を提供する。 次に,0ショットプロンプト,CoT推論,レムマ検索によるこれらの補題の形式的証明をGPT-4で記述する能力を評価する。 反応を評価する際には、LLMが自然言語とリーン言語で証明を書く能力の欠点も分析します。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems [47.93470713879515]
  InternLM2.5-SteperはMiniF2F、Lean-Workbook-Plus、ProofNet、Patnamベンチマークのオープンソースステート・オブ・ザ・アートを実現している。 MiniF2Fテストでは65.9%をパスし、Lean-Workbook-Plusの17.0%の問題を証明(あるいは否定)している。
  論文  参考訳（メタデータ） (2024-10-21T07:18:23Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
  大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-06-06T08:25:43Z)
• 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)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
  本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。 大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
  論文  参考訳（メタデータ） (2022-10-21T22:37:22Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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