論文の概要: miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

• arxiv url: http://arxiv.org/abs/2511.03108v1
• Date: Wed, 05 Nov 2025 01:27:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-06 18:19:32.290975
• Title: miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
• Title（参考訳）: miniF2F-Leanが再考: 制限のレビューとパスの前方へのチャート
• Authors: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh,
• Abstract要約: ミニF2Fベンチマークの形式的および非公式なステートメントは、ミニF2Fの問題からなる数学オリンピアードに参加するように命じられたAIシステムの観点から分析する。 評価結果から,本論文の論文では,SoTAモデルを用いて,これらのパイプラインの最適精度が約36%であることが判明した。 本報告では, miniF2F-v2 を形式的および非公式な文と証明で完全検証した。
• 参考スコア（独自算出の注目度）: 16.8655558789989
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad consisting of the problems in miniF2F. In such setting, the model has to read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds to the original informal statement presented to the model. Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the miniF2F-v2 with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on miniF2F-v2 leads to the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that a higher quality benchmark can help the community better evaluate progress in the field of formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at https://github.com/roozbeh-yz/miniF2F_v2.
• Abstract（参考訳）: 我々は,MiniF2Fにおける問題からなる数学オリンピアードに参加することを任務とするAIシステムの観点から,MiniF2Fベンチマークの形式的および非公式なステートメントを徹底的に分析する。 このような設定では、モデルは自然言語の問題を読み取り、理解し、それらをリーン言語で形式化し、その問題を証明し続けなければなりません。 評価の結果,本論文の論文では,SoTAモデルを用いたパイプラインの最適精度は約36%であり,個々のSoTAアキュラシーよりも有意に低く,自動形式化と定理証明の文献では97%,69%であった。 障害モードを解析した結果、この低下のかなりの部分は、 miniF2F の問題の半分以上について、形式文と非公式文の相違に遡る。 フォーマルな文と非公式な文の誤り、相違点、簡易化を訂正し、完全に検証されたフォーマルな文と非公式な文と証明をMiniF2F-v2で提示する。 完全定理証明パイプラインを miniF2F-v2 上で評価すると、70% の精度が最高のものとなり、元の miniF2F の40% から大幅に改善されたが、自己形式化モデルと定理証明器の間にはかなりの相違が見られる。 より深い分析は、コミュニティが形式的推論の分野の進歩をよりよく評価し、また自己形式化と定理証明モデルの失敗と成功のモードをよりよく診断するのに役立つことを示唆している。 私たちのデータセットはhttps://github.com/roozbeh-yz/miniF2F_v2で公開されています。

関連論文リスト

• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models [13.498044623556737]
  本稿では,Draft,Sketch,Proveフレームワークの改良版であるtextbfDSP+を紹介する。 相ごとに微細で統合されたニューロシンボリックエンハンスメントを特徴とする。 DSP+は、MiniF2F、ProofNet、PatnamBenchから80.7%、32.8%、24の644の問題を解決する。
  論文  参考訳（メタデータ） (2025-06-13T06:25:59Z)
• Mathesis: Towards Formal Theorem Proving from Natural Languages [40.397691467863886]
  パイプライン処理の非公式な問題文を証明する最初のエンドツーエンド定理であるMathesisを開発した。 これは、自然言語問題の形式化能力を高めるために強化学習を用いた最初のオートフォーマライザであるMathesis-Autoformalizerに貢献する。 また、形式化された文から形式的な証明を生成するMathesis-Proverを提案する。
  論文  参考訳（メタデータ） (2025-06-08T09:04:14Z)
• Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving [44.5694120006447]
  決定論的マルコフ決定過程として,問題解決の原理的定式化を提案する。 また,既存のFTP環境を利用してプロセス検証問題解決を行う新しいフレームワークFPSを提案する。 我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-05-07T16:02:14Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

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

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