論文の概要: Automated Conjecture Resolution with Formal Verification

• arxiv url: http://arxiv.org/abs/2604.03789v1
• Date: Sat, 04 Apr 2026 16:35:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-07 15:49:18.771453
• Title: Automated Conjecture Resolution with Formal Verification
• Title（参考訳）: 形式的検証による自動対物分解能
• Authors: Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, Bin Dong,
• Abstract要約: 本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。 我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。 このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
• 参考スコア（独自算出の注目度）: 21.763678203045973
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework for tackling research-level mathematical problems that integrates natural language reasoning with formal verification, enabling end-to-end problem solving with minimal human intervention. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas mimics the workflow of human mathematicians by combining reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with our formal theorem search engine LeanSearch, translates informal arguments into formalized Lean 4 projects through structured task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent is capable of autonomously filling nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, substantially reduce human effort, and offer a concrete instantiation of human-AI collaborative mathematical research.
• Abstract（参考訳）: 大規模言語モデルの最近の進歩は、基礎的な問題解決から研究レベルの問題における能力向上まで、数学的推論の能力を大幅に向上させてきた。 しかし、自然言語推論の本質的な曖昧さのため、そのような問題を確実に解き、検証することは依然として困難である。 本稿では,自然言語推論を形式的検証と統合し,人間の介入を最小限に抑えたエンドツーエンドの問題解決を可能にする,研究レベルの数学的問題に取り組むための自動フレームワークを提案する。 我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。 Rethlasは、推論プリミティブと定理検索エンジンMatlasを組み合わせることで、人間の数学者のワークフローを模倣し、ソリューション戦略を探求し、候補証明を構築する。 フォーマルな定理検索エンジンであるLeanSearchを装備したArchonは、非公式な議論を構造化されたタスク分解、反復的洗練、自動証明合成を通じて形式化されたLean 4プロジェクトに翻訳し、マシンチェック可能な正確性を保証する。 このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。 実験の結果,強い定理検索ツールによってクロスドメインな数学的手法の発見と適用が可能であり,形式的エージェントは非自明な間隙を非公式に埋めることができることがわかった。 より広範に、本研究は、定理検索ツールを備えた非公式で形式的な推論システムが、検証可能な結果を生成するためにタンデムで動作し、人間の努力を大幅に削減し、人間とAIの協調的な数学的研究の具体的なインスタンス化を提供する、数学研究のための有望なパラダイムを描いている。

関連論文リスト

• Towards Autonomous Mathematics Research [48.29504087871558]
  Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。 具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。 我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
  論文  参考訳（メタデータ） (2026-02-10T18:50:15Z)
• Advancing Mathematical Research via Human-AI Interactive Theorem Proving [16.40852561664514]
  LLMを用いた対話型定理証明と発見のためのヒューマン・イン・ザ・ループ・ワークフローを提案する。 人間の専門家は問題定式化と許容可能な仮定の制御を維持し、モデルは証明や矛盾を探索する。 このワークフローを、多様体最適化とグロバーの量子探索アルゴリズムの接続に関するケーススタディでインスタンス化する。
  論文  参考訳（メタデータ） (2025-12-10T09:16:27Z)
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch [8.80477323574638]
  IndiMathBenchは、数学的定理の証明を評価するために設計された人間検証ベンチマークである。 IndiMathBenchは312の形式的Lean 4定理とそれに対応する非公式な問題文を組み合わせて構成されている。
  論文  参考訳（メタデータ） (2025-11-30T17:40:13Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Why Reasoning Matters? A Survey of Advancements in Multimodal Reasoning (v1) [66.51642638034822]
  推論は人間の知性の中心であり、多様なタスクにまたがる構造化された問題解決を可能にする。 大規模言語モデル(LLM)の最近の進歩は、算術、常識、記号領域における推論能力を大幅に向上させてきた。 本稿では,テキストおよびマルチモーダルLLMにおける推論手法の簡潔かつ洞察に富んだ概要について述べる。
  論文  参考訳（メタデータ） (2025-04-04T04:04:56Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。 我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。 また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
  論文  参考訳（メタデータ） (2022-12-06T04:37:51Z)
• Formal Mathematics Statement Curriculum Learning [64.45821687940946]
  同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。 また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
  論文  参考訳（メタデータ） (2022-02-03T00:17:00Z)

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

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