技術要約：MECA – 明確に規定され、価値のある数学的予想を構築するためのメカニズム中心型エージェント

1. 問題提起

自動化された数学的発見において、明確に規定され、かつ価値のある数学的予想（conjecture）の構築は、依然として中心的な課題である。既存のアプローチは、問題が広範すぎたり、規定が不十分であったり、あるいは妥当な証明または反証戦略から乖離していたりすることが多い。現在のシステムは、通常、定義された探索空間内で動作するか、あるいは既に選択された研究対象から開始するものであり、広範な数学的ソースから境界付けられた予想を構築し、それを支持するメカニズムと共に共同で洗練させるための一般的な手法を欠いている。

核心的な困難は、候補となる命題とそれを支持する推論との共同の洗練にある。命題をあまりに早く固定してしまうと、不適切なターゲットが保持されてしまう可能性があり、一方で、利用可能な議論に合わせて命題を自由に適応させすぎると、命題が自明なものや既に解決済みのものになってしまう可能性がある。目標は、精密であり、妥当な証明または反証の経路によって支持されており、かつ、どちらの結果になっても価値があり、真に未解決の核（unresolved core）を保持する予想を生み出すことである。

2. 手法：MECAフレームワーク

著者らは、候補となる命題とそれを支持する数学的メカニズムを、結合された探索オブジェクトとして扱うマルチエージェント・フレームワークである**MECA (MEchanism-centered Conjecture Agent)**を導入する。

2.1 核心的概念：数学的メカニズム

メカニズムは、一連の仮定とそれに対応する結論を結びつける、再利用可能な推論モード（例：不等式、不変量、分解、簡約など）として定義される。MECAにおけるメカニズムは、漠然とした証明技法とは異なり、以下の特性を持つ具体的な条件付き議論である：

• $Req(m)$: 必要とされる仮定、または既知の事実。
• $Prov(m)$: その議論によって確立される帰結。
• $Gap(m)$: 未解決のまま残されている、非定型的（non-routine）な条件または下流の義務。

メカニズムはメカニズムグラフ ($G_t$) に整理される。これは、エッジが依存関係（すなわち、あるメカニズムの結論があるメカニズムが必要とする条件を供給すること）を表す有向グラフである。このグラフは、議論がいかに構成されるかを記録し、相互の互換性と非循環性を保証する。

2.2 3段階のパイプライン

MECAは、以下の3つの異なるステージを経て動作する：

1. ソースに基づいたシード構築 (Source-Grounded Seed Construction):

   • 入力: 構造化された数学文献、または手動でキュレーションされた広範な未解決問題。
   • プロセス: シード生成器 (Seed Generator) が、資料を「最も近い既知の結果」「提案される進展」「予備的なターゲット」「予想されるボトルネック」を記録した「シード」へと変換する。
   • 検証: シード検証器 (Seed Validator) が、研究としての価値（単なる言い換えや自明な変種を排除する）および数学的正当性（定義、量化子、境界事例のチェック）をレビューする。検証されたシードのみが次に進む。

2. メカニズムと問題の共同探索 (Mechanism–Problem Co-Exploration):

   • エージェント:
     • メカニズム–問題探索者 (Mechanism–Problem Explorer): 証明または反証のメカニズムを提案し、証拠に基づいて候補となる命題を修正し、必要に応じて候補を分割する。
     • メカニズム・クリティック (Mechanism Critic): メカニズムの正当性、非循環性、および適用可能性を独立して監査する。
     • 候補クリティック (Candidate Critic): 候補の各バージョンについて、適切に規定されているか、および「凍結されたターゲット・アンカー（fixed research boundary）」との整合性をレビューする。
     • カバレッジ判定員 (Coverage Judge): 受理されたメカニズムが、候補への一貫した経路を形成するように構成されているかを評価し、「支持不足 (Insufficient Support)」、「実質的な部分的サポート (Substantive Partial: 明確な未解決の核を伴う意味のあるサポート)」、「完全なカバレッジ (Full Coverage)」を区別する。
   • プロセス: 候補となる命題とメカニズムグラフは、共同で洗練される。メカニズムによって不足している仮定や過度に強い結論が明らかになった場合、候補となる命題は修正される。

3. 証明者向けの課題構築 (Prover-Facing Problem Construction):

   • 最終チャレンジャー (Final Challenger): メカニズムグラフや探索履歴にアクセスすることなく、候補を監査する独立したエージェント。命題の閉鎖性、反例に対する耐性、および価値をチェックする。
   • 投影 (Projection): 受理された候補は、決定論的に自己完結型の問題文 ($q = \Theta(A, p, G')$) へと投影される。未解決の核は、具体的な証明義務へと変換される。
   • ブラインド・プローブ (Blind Probes): 最終的な命題は、難易度と解決可能性を評価するために、独立した証明器（MECAの内部推論にアクセスしない状態）によってテストされる。

3. 主な貢献

本論文は主に以下の3つの貢献を行う：

1. 定式化: 予想の構築を、監査された部分的なサポートと明示的な未解決の障害に導かれた、候補となる命題とそれを支持するメカニズムの共同の洗練として定式化した。
2. フレームワーク: 数学文献や広範な未解決問題から精密な予想を構築できる、メカニズム中心のマルチエージェント・フレームワークであるMECAを導入した。
3. データセット: 明確な仮定と数学的動機付けを持つ、100個の証明者向け未解決問題を寄贈し、現在の自動証明および反証システムの限界を露呈させる設計とした。

4. 実験的評価

MECAは、2つの補完的な設定で評価された。

4.1 ターゲット条件付きの結論復元

• 設定: システムに対し、2023年以降のターゲット論文20本から、2024年以前の「記事ブラインド（article-blind）」なソース資料（ターゲットごとに7本の論文）のみを用いて結論を再構成するよう課した。
• ベースライン: 「ドラフト–監査–修正 (Draft–Audit–Revise)」ベースラインと比較した。
• 結果: MECAはベースラインを大幅に上回り、平均ターゲット整合スコアを 48.0 から 69.0 に向上させた。最大の改善は、中心的な結論の復元（+6.0）と定量的正確性（+5.5）に見られ、これはメカニズム中心の構築が、精密な定理レベルの主張とその妥当性の範囲の復元を向上させることを示している。

4.2 予想の生成と検証

• 設定: 文献シードと既存の未解決問題から100個の準オープン問題（semi-open problems）を構築した。これらを、5時間の時間制限を設けて、オープンソースのマルチエージェント定理証明器である QED に投入した。
• 結果:
  • 35% が証明された。
  • 11% が反証された（検証された反例）。
  • 54% が未解決のままとなった。
• 未解決ケースの分析: 未解決となった54ケースのうち、81.5% は「技術的な証明の困難さ（命題は適切に規定され支持されていたが、証明が現行のソルバーの能力を超えていた）」に起因していた。生成された予想のわずか 10% しか、定式化または準備不足の欠陥（例：仮定の欠落、曖昧さ）を示していなかった。このことは、MECAが、実質的な数学的困難さを保持しつつ、スタンドアロンのタスクとして利用可能な予想を生成していることを示唆している。

5. 意義と主張

本論文は、MECAが広範な研究方向を、明確に特定された未解決の核を保持しつつ、実質的な数学的サポートを伴う精密な予想へと正常に変換できることを主張している。メカニズムに基づいて洗練を行うことで、以下のことが保証される：

• 候補は単なる推測ではなく、監査された部分的な進展によって支持されている。
• 「未解決の核」が明示的に分離されており、サポートの欠如と真の未解決問題が区別されている。
• 生成された予想は、定式化の欠陥よりも「技術的困難さ」の結果として現れることから、現在の自動証明器にとって挑戦的なものであることが示されている。

著者らは、MECAがこれらの問題を解決することや、絶対的な意味での歴史的新規性を保証することを主張しているのではない。むしろ、限定された数学的証拠から、明確に規定された、研究に値する予想を構築するための信頼できる手法を示すものであると強調している。本フレームワークは、孤立した命題を生成することと、それを検証するために必要な構造的推論を共に発展させることとの間のギャップに対処している。