論文の概要: Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
- arxiv url: http://arxiv.org/abs/2605.13171v1
- Date: Wed, 13 May 2026 08:33:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-14 23:30:27.916288
- Title: Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
- Title（参考訳）: Formal Conjectures: 数学における検証された発見のためのオープンで進化するベンチマーク
- Authors: Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, Pushmeet Kohli,
- Abstract要約: フォーマル・コンジェクチャ(Formal Conjectures)は、Lean 4.0で形式化された2615の数学的問題文の進化ベンチマークである。
このデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンリサーチ予想を特徴としている。
我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
- 参考スコア（独自算出の注目度）: 9.38309744591661
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.
- Abstract（参考訳）: 自動推論システムが急速に進歩するにつれて、それらの能力を正確に評価するために研究レベルの形式的な数学的問題の必要性が高まっている。
これを解決するために、Lean 4で形式化された2615の数学的問題文の進化ベンチマークであるFormal Conjecturesを紹介します。
活発な数学的研究の分野から導かれたこのデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンな研究予想と、証明オートフォーマライゼーションのための836の解決問題を特徴としている。
特に、このリポジトリは、AIシステムとそれを解決しようとする人間との問題を形式化し、明らかにする数学者を接続する構造化インターフェイスを提供する。
その即時効用を実証するために、このベンチマークは、オープンな研究予想の解決を含む新しい数学的発見のために既に活用されている。
我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
このフレームワークでは、AIが生成した証明と耐障害性は、ベンチマークの忠実度を反復的に改善するための貴重な監査メカニズムとして役立ちます。
最後に,研究レベルの数学における自動推論の現在のフロンティアを測定するために,凍結評価サブセットの標準化された評価設定とベースライン結果の報告を行う。
関連論文リスト
- Automated Conjecture Resolution with Formal Verification [21.763678203045973]
本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。
我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。
このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
論文 参考訳（メタデータ） (2026-04-04T16:35:16Z) - HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification [54.06301039725887]
計算および応用数学において8つの領域にまたがる100以上の未解決問題のベンチマークであるHorizonMathを紹介する。
我々のベンチマークは、発見が困難であり、意味のある数学的洞察を必要とする問題のクラスをターゲットにしているが、検証は計算的に効率的で簡単なものである。
論文 参考訳（メタデータ） (2026-03-16T17:59:53Z) - Towards Autonomous Mathematics Research [48.29504087871558]
Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。
具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。
我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
論文 参考訳（メタデータ） (2026-02-10T18:50:15Z) - EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery [23.517907682810932]
我々は、フロンティア数学的推論を評価するための完全自動化された定理基底パイプラインを提案する。
このパイプラインは、最近のピアレビューされた数学的文献を実行可能で検証可能な推論タスクに変換する。
このパイプラインを適用すると、現代の研究論文から派生した進化的評価スイートである textbfEternalMath が生成される。
論文 参考訳（メタデータ） (2026-01-04T06:40:25Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。
このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。
実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
論文 参考訳（メタデータ） (2025-01-21T06:32:25Z) - Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。
既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
論文 参考訳（メタデータ） (2024-12-20T17:19:24Z) - LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。
実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-06-20T06:42:27Z) - GLUECons: A Generic Benchmark for Learning Under Constraints [102.78051169725455]
本研究では,自然言語処理とコンピュータビジョンの分野における9つのタスクの集合であるベンチマークを作成する。
外部知識を制約としてモデル化し、各タスクの制約のソースを特定し、これらの制約を使用するさまざまなモデルを実装します。
論文 参考訳（メタデータ） (2023-02-16T16:45:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。