論文の概要: RLMEval: Evaluating Research-Level Neural Theorem Proving
- arxiv url: http://arxiv.org/abs/2510.25427v1
- Date: Wed, 29 Oct 2025 11:49:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-30 15:50:45.492083
- Title: RLMEval: Evaluating Research-Level Neural Theorem Proving
- Title（参考訳）: RLMEval: 研究レベルのニューラルネットワーク理論の実証評価
- Authors: Auguste Poiroux, Antoine Bosselut, Viktor Kunčak,
- Abstract要約: 本稿では,実世界のリーン形式化プロジェクトによる研究レベルの数学評価スイートRLMEvalを紹介する。
リーンプロジェクトの613の定理を含むRLMEvalの最先端モデルの評価では、大きなギャップが明らかになりました。
RLMEvalは、形式数学の自動推論の進歩をガイドし、加速するために設計された、新しい挑戦的なベンチマークを提供する。
- 参考スコア（独自算出の注目度）: 18.42453100491575
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still limited. We introduce RLMEval, an evaluation suite for these tasks, focusing on research-level mathematics from real-world Lean formalization projects. RLMEval targets the evaluation of neural theorem proving and proof autoformalization on challenging research-level theorems by leveraging real Lean Blueprint formalization projects. Our evaluation of state-of-the-art models on RLMEval, comprising 613 theorems from 6 Lean projects, reveals a significant gap: progress on existing benchmarks does not readily translate to these more realistic settings, with the best model achieving only a 10.3 % pass rate. RLMEval provides a new, challenging benchmark designed to guide and accelerate progress in automated reasoning for formal mathematics.
- Abstract（参考訳）: キュレートされたベンチマークに対する印象的な結果にもかかわらず、研究レベルのニューラル定理の証明と証明の自己形式化に対する大規模言語モデル(LLM)の実践的影響は依然として限られている。
本稿では,実世界のリーン形式化プロジェクトによる研究レベルの数学に焦点を当てた,これらのタスク評価スイートであるRLMEvalを紹介する。
RLMEvalは、真のリーン青写真形式化プロジェクトを活用することで、挑戦的な研究レベルの定理に対する、神経定理の証明と証明の自己形式化の評価を目標としている。
6つのリーンプロジェクトの613の定理を含むRLMEvalの最先端モデルの評価では、大きなギャップが明らかになりました。
RLMEvalは、形式数学の自動推論の進歩をガイドし、加速するために設計された、新しい挑戦的なベンチマークを提供する。
関連論文リスト
- FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。
しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。
機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
論文 参考訳（メタデータ） (2025-09-26T14:40:14Z) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。
Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。
Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
論文 参考訳（メタデータ） (2025-04-15T16:23:44Z) - Theorem Prover as a Judge for Synthetic Data Generation [22.124954482278536]
RLHF(Reinforcement Learning from Human Feedback)において、人間のアノテーションを定理証明に置き換える枠組みを提案する。
複数の大規模言語モデル(LLM)でTP-as-a-JudgeとRFを適用し、ベンチマークをわずか3,508サンプルで改善し、MultiArithmのMistral-7Bで5.56%の精度を達成した。
論文 参考訳（メタデータ） (2025-02-18T18:57:09Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。