論文の概要: Evaluating Research-Level Math Proofs via Strict Step-Level Verification
- arxiv url: http://arxiv.org/abs/2606.10799v1
- Date: Tue, 09 Jun 2026 12:46:35 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-10 15:40:58.500558
- Title: Evaluating Research-Level Math Proofs via Strict Step-Level Verification
- Title（参考訳）: Strict Step-Level Verificationによる研究レベル数学証明の評価
- Authors: Yifeng Sun,
- Abstract要約: 大規模言語モデル(LLM)は、複雑な数学的証明の厳密な検証に苦慮している。
このフレームワークは、各推論ステップの詳細なコンテキストを維持し、適用定理のソースを厳格に制限する。
本研究は, エージェントに対して, 慎重な人-数学的な方法で検証ノートを整理するよう促すことによって, 厳密な証明を欠陥と区別する能力を大幅に向上させることを示唆している。
- 参考スコア（独自算出の注目度）: 0.1269104766024433
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) struggle to rigorously verify complex mathematical proofs. Standard global evaluation approaches suffer from "context poisoning," in which superficially plausible statements mask subtle logical flaws, leading to hallucination or over-skepticism. To address this, we shift from global evaluation to strict step-level verification: our framework maintains detailed context for each deduction step and strictly constrains the sources of applied theorems. We evaluate on a carefully curated adversarial diagnostic suite of research-level proofs drawn from the FirstProof challenge. A systematic ablation study demonstrates that these deductive constraints are indispensable, as unconstrained global prompting consistently fails to localize subtle logical errors. Beyond outperforming global evaluation, our approach fundamentally alters the failure taxonomy. Error analysis reveals that, rather than exhibiting severe logical hallucinations, remaining rejections are primarily instances of "pedantic hyper-rigor" stemming from unstated domain conventions, effectively exposing implicit ambiguities within the expert benchmark itself. Our findings suggest that prompting agents to organize their verification notes in a cautious, human-mathematician-like manner can substantially improve their ability to distinguish rigorous proofs from flawed ones, with the potential to strengthen agentic reasoning on frontier mathematical concepts that the base model does not already know well, and to lay a theoretical foundation for future automated proof-review systems. Code and prompts are available at GitHub.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、複雑な数学的証明の厳密な検証に苦慮している。
標準的な国際的評価アプローチは「コンテキスト中毒(context poisoning)」に悩まされ、表面的確固たる説明が微妙な論理的欠陥を隠蔽し、幻覚や過度懐疑を招いた。
この問題に対処するため、我々はグローバル評価から厳格なステップレベルの検証へと移行した:我々のフレームワークは、各推論ステップの詳細なコンテキストを維持し、適用定理のソースを厳格に制約する。
我々は、FirstProofチャレンジから得られた研究レベルの証明を、慎重に検証した対向的診断スイートについて評価した。
体系的アブレーション研究は、これらの誘因的制約が不可欠であることを示し、非制約な大域的プロンプトは微妙な論理的誤りの局所化に一貫して失敗する。
グローバルな評価に勝るだけでなく、我々のアプローチは失敗の分類を根本的に変えます。
誤り分析は、厳密な論理幻覚を示すのではなく、残余の拒絶は、未定の領域規則から生じる「ペダニックな超厳密さ」の事例であり、専門家ベンチマーク自体の暗黙の曖昧さを効果的に露呈することを明らかにする。
本研究は, エージェントによる検証ノートの組織化を促すことによって, 厳密な証明と欠陥を区別する能力が大幅に向上し, 基礎モデルがまだよく分かっていないフロンティア数学的概念に基づくエージェント推論が強化され, 将来的な自動証明レビューシステムの理論的基盤が築かれる可能性が示唆された。
コードとプロンプトはGitHubで入手できる。
関連論文リスト
- AEGIS: From Clues to Verdicts -- Graph-Guided Deep Vulnerability Reasoning via Dialectics and Meta-Auditing [9.271196825503417]
大きな言語モデル(LLM)は、脆弱性検出にますます採用されているが、その推論は基本的には正しくない。
AEGISは、未解決の投機から、クローズドな事実ベース上の法医学的検証へ、検出をシフトする新しいマルチエージェントフレームワークである。
これは、主要なベースラインと比較して偽陽性率を最大54.40%削減し、1サンプルあたりの平均コストはタスク固有のトレーニングなしで0.09ドルである。
論文 参考訳（メタデータ） (2026-03-21T04:12:04Z) - Anatomy of a Lie: A Multi-Stage Diagnostic Framework for Tracing Hallucinations in Vision-Language Models [62.932580559941414]
VLM(Vision-Language Models)は、しばしば「ハロシン化(hallucinate)」する。
本稿では,静的な出力誤差からモデル計算認知の動的病理へ再キャストし,幻覚を診断するための新しいパラダイムを提案する。
論文 参考訳（メタデータ） (2026-03-16T17:20:38Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - Reasoning-Driven Amodal Completion: Collaborative Agents and Perceptual Evaluation [17.405818788700234]
本稿では,視覚合成から意味的計画を明確に分離する協調的マルチエージェント推論フレームワークを提案する。
提案手法は,画素生成前の構造的,明示的なプランを生成し,視覚的,意味的に整合した単一パス合成を可能にする。
従来の評価基準の限界に対処し,新しい人間対応評価指標MAC-Scoreを導入する。
論文 参考訳（メタデータ） (2025-12-24T04:39:45Z) - AlignCheck: a Semantic Open-Domain Metric for Factual Consistency Assessment [0.0]
ドメイン内およびオープンドメインテキストの事実整合性評価のための解釈可能なフレームワークを提案する。
提案手法では,テキストをアトミックな事実に分解し,フレキシブルでスキーマフリーな手法を導入する。
一般的な一般的なデータセットと臨床データセットにアプローチをベンチマークし、事実認識モデルトレーニングをサポートするためにコードをリリースします。
論文 参考訳（メタデータ） (2025-12-03T10:14:31Z) - Deliberative Reasoning Network: An Uncertainty-Driven Paradigm for Belief-Tracked Inference with Pretrained Language Models [7.095344389368656]
Deliberative Reasoning Network (DRN) は、確率から不確実性への論理的推論を再構成する新しいパラダイムである。
DRNは、信念状態を明示的に追跡し、競合する仮説の不確実性を定量化することによって、本質的な解釈可能性を達成する。
我々は、DRNを、より信頼できるAIシステムを構築するための、基礎的で検証可能なシステム2推論コンポーネントとして位置付ける。
論文 参考訳（メタデータ） (2025-08-06T11:33:35Z) - 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) - Controllable Logical Hypothesis Generation for Abductive Reasoning in Knowledge Graphs [54.596180382762036]
知識グラフの帰納的推論は、観測された実体からもっともらしい論理的仮説を生成することを目的としている。
可制御性の欠如により、単一の観測は、多くの妥当だが冗長あるいは無関係な仮説をもたらす可能性がある。
帰納的推論の実用性を改善するために,制御可能な仮説生成タスクを導入する。
論文 参考訳（メタデータ） (2025-05-27T09:36:47Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Causality can systematically address the monsters under the bench(marks) [64.36592889550431]
ベンチマークはさまざまなバイアス、アーティファクト、リークに悩まされている。
モデルは、調査の不十分な障害モードのため、信頼できない振る舞いをする可能性がある。
因果関係はこれらの課題を体系的に解決するための 理想的な枠組みを提供します
論文 参考訳（メタデータ） (2025-02-07T17:01:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。