技術要約：デュアル・エージェントによる凸緩和のAI支援的発見

1. 問題設定

本論文は、関数解析におけるシャープな定数を持つ不等式の**証明可能な下界（certified lower bounds）**を改善するという課題に取り組んでいる。具体的には、許容される関数の無限次元空間におけるスコアのインフィマム（下限）を見つけることを目的とした、非凸最適化問題に焦点を当てている。

著者らは、Georgievら（2025）によって研究された2つの特定の定数を対象としている：

1. 第1自己相関不等式 (C6.2): シドン集合に関連する加法的組合せ論における定数。以下の不等式によって定義される：
   $$\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t-x)f(x) \, dx \ge C_{6.2} \left( \int_{-1/4}^{1/4} f(x) \, dx \right)^2$$
   ここで、$f: \mathbb{R} \to \mathbb{R}$ は非負の関数である。
2. Erdős最小オーバーラップ定数 (C6.5): 最小オーバーラップ問題の漸近挙動を支配する定数。以下の不等式によって定義される：
   $$\sup_{x \in [-2, 2]} \int_{-1}^{1} f(t)g(x+t) \, dt \ge C_{6.5}$$
   ここで、$f, g: [-1, 1] \to [0, 1]$ は非負であり、$f+g=1$ かつ $\int f = 1$ を満たす。

近年のAI主導の研究は、極値構成（ある不等式を破るような特定の関数）を探索することで**上界（upper bounds）**を改善することに成功しているが、**下界（lower bounds）の改善はそれとは性質が異なる。下界は、すべての許容される関数に対して成立しなければならないため、「いかなる関数もスコアをある一定値以下に落とすことはできない」という証明が必要となる。これは通常、元の非凸問題の凸緩和（convex relaxation）**を解くことによって達成される。緩和がタイトであればあるほど（すなわち、追加される有効な制約が多いほど）、得られる下界は強くなる。

2. 手法：デュアル・エージェント・ループ

著者らは、2つの特化した大規模言語モデル（LLM）エージェントによって駆動されるヒューマン・イン・ザ・ループのフレームワークを用いたオートリサーチ・パラダイムを構築している。このシステムは、凸緩和を強化するための有効な制約を反復的に発見し、検証するように設計されている。

エージェント

1. コーディング・エージェント (Coding Agent):

   • 役割: 凸計画問題に対する新しい制約を提案するか、既存の制約を強化する。
   • 出力: 修正された凸最適化計画を生成し、その新しい制約がすべての許容される関数に対して保持されることを正当化する「厳密な証明」（数学的議論）を出力する。
   • アクション: 制約をコード（CVXPYを使用）として実装し、プログラムを解いて候補となる下界を算出する。

2. 理論エージェント (Theory Agent):

   • 役割: 検証者および反例探索者として機能する。
   • アクション: 提案された制約とその証明を読み取る。提案された制約が、許容条件（例：$f \ge 0$）の必然的な帰結であることを確認するために、その論理を批判的に分析する。決定的なのは、提案された制約を破る係数を持つ特定の許容関数（反例）を能動的に探索することである。
   • 決定: 証明が妥当であり、かつ反例が見つからない場合は、その制約は受理される。論理的な欠陥や反例が見つかった場合、提案は拒否され、コーディング・エージェントには別の手法を試すよう指示される。

検証パイプライン

最終的な結果が**証明可能（certified）**なもの（単なる数値的な推定ではなく、数学的に証明されたもの）であることを保証するため、システムは厳密なデュアル認証プロセスを採用している：

• 双対実行可能（Dual Feasibility）: システムは凸計画問題の双対問題を構築する。
• 区間演算（Interval Arithmetic）: 双対実行可能な点 $\lambda$ を見つけ、その実行可能性と双対目的関数値を厳密な区間演算を用いて検証する。これにより、浮動小数点数の丸め誤差や、三角関数のモーメントなどの無理数データによる影響を考慮する。
• 認証（Certification）: 弱双対性により、有効な双対点 $\lambda$ とその目的関数値 $\beta$ は、元の問題の最適値（したがって真の定数）が少なくとも $\beta$ であることを証明する。報告される最終的な下界は、検証された包絡線の下限値となる。

人間の役割

人間の研究者は、最終的なレビューと**コンパクト化（compactification）**を行う。エージェントのループでは、冗長な制約が蓄積されることが多いため、人間が最終的なプログラムをレビューし、不要な制約を除去して最小限で読みやすい定式化を作成し、最終的な認証を行う前に数学的議論を検証する。

3. 主な貢献

• パラダイムの転換: 本論文は、極値の例を探索するのではなく、証明可能な下界の発見にAIエージェントを適用した新しい事例を示している。これは、存在量化（特定の関数を見つけること）ではなく、普遍量化（すべての関数に対して妥当であることの証明）を必要とする不等式の「下界」側に対処するものである。
• デュアル・エージェント・フレームワーク: コーディング・エージェントが制約を提案し、理論エージェントがその妥当性を検証し反例を探すという、数学的緩和を反復的に洗練させるための具体的なループを導入した。
• 厳密な認証: 区間演算と双対実行可能性チェックの統合により、向上した下界が、数値ソルバーの浮動小数点精度に依存せず、数学的に証明されたものであることを保証している。

4. 結果

本フレームワークは、上述の2つの定数に適用され、証明可能な下界を改善した：

• C6.2 (第1自己相関不等式):

  • 従来の最良下界: 1.28 (Cloninger & Steinerberger, 2017)。
  • 新しい証明可能な下界: 1.2937。
  • 注記: この問題に対する凸計画プログラムは以前は存在しておらず、エージェントがゼロから構築した。

• C6.5 (Erdős最小オーバーラップ定数):

  • 従来の最良下界: 0.379005 (White, 2022)。
  • 新しい証明可能な下界: 0.37912。
  • 注記: エージェントはWhiteの既存の凸計画プログラムから開始し、**ボホナーの定理（Bochner's theorem）**に基づく2つの新しい有効な制約を発見した（$f$ およびその補集合 $g=1-f$ のモーメント列が非負測量によって実現可能であることを強制するもの）。

論文では、これらの問題の上界については、探索ベースの手法（Together AI, 2026など）によって改善されているが、下界は2022年以来停滞していたことが述べられている。本研究は、これらの下界を前進させることに成功した。

5. 意義と主張

著者らは、これが特定の不等式における証明可能な下界を改善するための、オートリサーチ型のエージェント・ループの最初の使用例であると主張している。その意義は以下の点にある：

1. 補完性: 極値の例を見つけることに焦点を当てた既存のAI研究に対し、緩和を通じて下界を証明するという、より困難な問題に取り組むことで、それを補完している。
2. 発見における自律性: エージェントは、人間が設計した定式化で見落とされていた、あるいは明示的に課されていなかった数学的性質（$f$ と $1-f$ に関するボホナー条件など）を正常に特定した。
3. 汎用性: 本研究は自己相関不等式において実証されたものであるが、著者らはこのフレームワークがこれらの問題に特化したものではないと述べている。これは、下界が有効な制約によって強化され、双対性によって認証される凸緩和として表現できる、あらゆる非凸最適化問題（最適化、組合せ論、制御理論など）に適用可能である。

論文は、制約の妥当性が現在は形式的証明助手（Leanなど）による数学的議論の検証ではなく、人間のレビューに依存していることを認めつつ、控えめに結論付けているが、将来的な形式検証ツールとの統合によって、このループを完全に自律化できる可能性を示唆している。