🤖 AI

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

本論文は、大規模言語モデルを用いて近似した平方和の予想を提案し、記号計算によってそれらを正確で機械検証可能な Lean 証明へと洗練させる神経記号フレームワークである NSPI を紹介し、これにより最大 10 変数の多項式不等式の拡張可能な自動証明を実現する。

原著者： Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

公開日 2026-05-18

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

複雑で多層構造のケーキが、切り方を変えたり材料を変更したりしても、常に「十分に甘い」（数学的には非負）であることを証明しようとしていると想像してください。数学の世界では、これは多項式不等式の証明と呼ばれます。

長年、数学者はこの作業を行うための主に 2 つの方法を持っていましたが、どちらも重大な欠点がありました：

「純粋な論理」アプローチ（記号的）： これは、黒板に材料の化学反応を一つ一つ書き出してケーキの問題を解こうとするようなものです。完全に正確ですが、ケーキに材料（変数）が多すぎると、黒板は瞬く間に埋め尽くされ、この方法は破綻してしまいます。大規模な問題には、あまりにも遅く、かつ煩雑すぎます。
「AI 推測」アプローチ（LLM）： これは、非常に賢く創造的なシェフにレシピを推測させるようなものです。シェフは迅速で、小さなケーキには得意ですが、ケーキが巨大で複雑になると、存在しない材料を幻覚のように思い込んだり、数学的な誤りを犯したりし始めます。彼らは自分の答えが 100% 真実であることを証明できません。

この論文は、NSPI（Neuro-Symbolic Polynomial Inequality proving：ニューロ・シンボリック多項式不等式証明）と呼ばれる新しいチームを紹介しています。NSPI を、創造的なシェフと厳格な品質検査官の完璧なパートナーシップと想像してください。

彼らの「組立ライン」がどのように機能するか、ステップごとに説明します：

ステップ 1：創造的なシェフ（LLM）

まず、チームは「シェフ」である大規模言語モデルに、難しい数学の問題を見てもらうように依頼します。シェフはすぐに難しい数学を行おうとはしません。代わりに、その創造性を用いて構造を推測します。

比喩： シェフが「このケーキは、3 つの特定の砂糖の角砂糖の層が積み重なってできているに違いない」と言うのを想像してください。
数学的には、LLM が平方和（SOS）分解を推測します。「この複雑な式は、おそらくいくつかのより単純なものの和を二乗しただけだ」と提案します。
重要な点： シェフの推測は通常、近似値です。近い値ですが、小さな小数点の誤差があるかもしれません（例えば、砂糖の角砂糖の重さを正確に 1 グラムではなく 1.0000001 グラムと言うような場合です）。

ステップ 2：品質検査官（記号的修正）

シェフの推測は、「品質検査官」である強力なコンピュータ代数システムに渡されます。

比喩： 検査官はシェフのラフなスケッチを受け取り、顕微鏡を使って小さな誤差を修正します。これには、正確な答えにズームインする数学的な手法であるニュートン法と、汚れた小数をきれいな正確な分数に変換する有理数復元という技術が用いられます。
シェフが層の厚さを「おおよそ」1.5、2.3、0.7 と推測した場合、検査官は正確な数値を計算します：3/2、23/10、7/10。
これで、推測は完璧で正確な数学的証明書へと変換されました。

ステップ 3：法廷の判事（Lean 検証）

最後に、チームはこの正確な証明書をLeanという名前の「判事」に持ち込みます。

比喩： Lean は、検査官の作業のすべてのステップを厳しく、瞬きもせずにチェックする厳格な判事です。これは「感覚」や「推測」には関心を持ちません。論理的に隙のない証明のみを受け入れます。
検査官が正確な証明書を提供してくれたおかげで、判事は簡単に検証できます。「はい、これらの正確な数を二乗して足し合わせれば、元のケーキになります。そして、二乗は常に正であるため、このケーキは常に甘いのです」。
判事はその後、100% 正確であることが保証された機械検証済み証明を発行します。

なぜこれが重要なのか？

この論文は、このチームを522 個の非常に難しい数学問題でテストしました。その中には、最大10 個の変数（材料）を持つものもありました。

従来の論理手法は、問題が大きくなりすぎると（材料が多くなりすぎると）、諦めてしまいました。
従来の AI 手法は、大きな問題になると混乱し、誤りを犯しました。
NSPI チームは、他が失敗した場所で成功しました。彼らは、他のどの手法も手をつけられなかった 10 変数の問題を解くことができました。

結論

この論文は、AI に解の形状を推測させ、その後、数学的なツールを使って詳細を修正し、コンピュータを使って真実を検証させることで、これまでにない速度と信頼性で複雑な不等式問題を解決できるシステムを構築したと主張しています。彼らは単に推測しただけではなく、「良い推測」から「証明された事実」へと架橋したのです。

彼らが主張しなかったこと：

この技術が病気を治したり、株式市場を予測したりするとは言っていません。
すべての種類の数学問題に機能するとは主張していません。特定の多項式式が常に正であることを証明する場合に限られます。
人間の数学者を完全に代替するとは主張していません。むしろ、非常に特定された困難な推論のタイプを自動化するものです。

技術的概要：LLM 生成の予想から Lean 形式化へ

問題定義

多項式不等式の自動証明は、数学的推論における根本的な課題であり、特に高次元および多変数のケースにおいて顕著である。既存のアプローチは重大なスケーラビリティの限界に直面している：

純粋な記号的手法： 強力な保証を提供する一方で、平方和（SOS）分解および半正定値計画（SDP）に基づく手法は、変数の数や次数が増加するにつれて、組み合わせの爆発と中間式の急激な増大に悩まされる。それらはしばしば構造化され、人間が読める証明を生成することに失敗する。
純粋な LLM 基盤手法： 証明支援系（例：Lean、Isabelle）と統合された大規模言語モデル（LLM）は有望さを示しているが、高品質な形式化されたトレーニングデータの不足によって制限されている。それらは複雑な代数的不等式、特に 5 変数を超えるものに対処するのに苦しみ、厳密で機械検証可能な証明書を生成する能力を欠くことが多い。

核心的な課題は、ヒューリスティックな発見と厳密な形式検証の間のギャップを埋めることであり、機械検証された正しさを備えたまま、高次元設定（最大 10 変数）における制約のない多項式不等式の自動証明を可能にすることである。

手法：NSPI フレームワーク

著者は、LLM と記号計算の相補的な強みをエンドツーエンドのパイプラインに統合する NSPI（Neuro-Symbolic SOS-based Polynomial Inequality Proving：ニューロ・シンボリック SOS 基盤多項式不等式証明）を提案する。このプロセスは主に 3 つの段階から構成される：

1. ニューラル予想（LLM 誘導 SOS 生成）

LLM を単なる探索ガイダンスとして使用するのではなく、NSPI はそれらを主要な予想生成器へと昇格させる。

データ構築： 著者は 2 つの新しい戦略を用いて、非負多項式–SOS ペアの大規模データセットを構築する：
- 計算駆動型： 制御された係数で半正定値（PSD）を確保するために、スペクトルシフトまたは LMI 最適化を通じてグラム行列を生成する。
- 構造駆動型： 対角優位（dd）およびスケーリング対角優位（sdd）行列のような代数的構造を活用する。これらは設計上 PSD 特性を保証する。
トレーニング： 2 段階のトレーニングスキームが採用される：
- コールドスタート： 基礎的な構造的推論を確立するために、100 万を超える合成多項式–SOS ペアに対する教師あり微調整（SFT）を行う。
- 段階的強化学習： 変数の数を 3–5 から 9–10 に増やすなど、困難なインスタンスに対してカリキュラムベースのグループ相対方策最適化（GRPO）を適用する。報酬関数は、精度（数値忠実度）、形式準拠、および代数的構造のペナルティを組み合わせ、LLM が妥当な SOS 構造を生成することを保証する。
出力： LLM は、与えられた多項式に対する近似 SOS 分解（平方項の和）を提案する。

2. 記号的補正（正確な有理数回復）

LLM の近似予想を厳密な証明に変換するために、記号的補正モジュールが出力を洗練させる：

ガウス・ニュートン法による洗練： 近似 SOS 構造を、ニュートン型反復法を用いて洗練させ、予想された平方和と対象多項式との間の後方誤差を最小化する。これにより、高精度な数値グラム行列が得られる。
有理数回復： 数値行列を正確な有理数 PSD 行列に変換する。解が PSD コンの内部にあるか境界上にあるかに応じて、システムは直交射影または同時ディオファントス近似を組み合わせた切断された LDL $^\top$ 分解を採用する。このステップにより、生成される SOS 証明書が正確であり、浮動小数点エラーから自由であることを保証する。

3. 形式検証（Lean 証明生成）

正確な有理数 SOS 証明書は、自動的に機械検証可能な Lean 証明に変換される。

証明テンプレート： 定義済みの Lean テンプレートに、正確な SOS 項が埋め込まれる。
検証： Lean 証明器は 2 つの条件を検証する：
1. 等式： 対象多項式は展開された SOS 式と等しい（linear_combination によって検証される）。
2. 非負性： SOS 式は非負である（positivity 戦術によって検証される。これは $x^2 \ge 0$ のような規則を再帰的に適用する）。

主要な貢献

ニューロ・シンボリックパイプライン： 神経的予想、記号的補正、形式検証を連鎖させることで、多項式不等式に対する完全な形式証明の生成を自動化するエンドツーエンドフレームワークである NSPI の提案。
原理的信頼性の架け橋： LLM 基盤のヒューリスティック生成と記号的正確な証明を統合する新しい手法。これにより、神経的予想が機械検証可能な証明へと変換され、膨大な既存の形式化トレーニングデータに依存することなく、高次元多変数のケース（最大 10 変数）へのスケーラビリティが可能になる。
ベンチマークと評価： 現実世界の競技問題および合成の高次元インスタンスを含む、3 から 10 変数の 522 の不等式問題からなる挑戦的なベンチマーク PolyIneqBench の構築。広範な実験により、NSPI が最先端の記号ソルバー（Maple、Z3）、純粋な LLM 証明器（DeepSeek-Prover-V2、Goedel-Prover）、既存のハイブリッドシステム（LIPS）、特に高次元シナリオにおいて優れていることが示された。

実験結果

性能： PolyIneqBench において、NSPI は 10 変数の問題で**11.7%**の通過率を達成したのに対し、記号的手法（Maple、Z3）および純粋な LLM 証明器はほぼ 0% または一桁に低下した。
効率性： NSPI は成功したソルバーの中で最も低い平均実行時間を維持し、いくつかの LLM 基盤証明器と比較して 10 倍以上の高速化を示した。
スケーラビリティ： 段階的強化学習戦略は、モデルの能力境界をより高次元へとシフトさせることに成功し、カリキュラムが 3–5 変数から 9–10 変数へと進むにつれて性能向上が観察された。
アブレーション： 合成コールドスタートトレーニングとカリキュラムベースの GRPO の両方が、システムの成功にとって不可欠であることを実験が確認した。

意義と主張

本論文は、LLM が単なる探索ガイドではなく核心的な記号的予想エンジンとして機能する、ニューロ・シンボリック定理証明における新たなパラダイムを確立すると主張している。LLM を SOS 構造などの記号的事前分布の生成器として扱い、正確性には記号計算を、正しさには形式検証に依存するこのアプローチは、純粋な神経的手法のデータ不足のボトルネックと、純粋な記号的手法のスケーラビリティの限界の両方を解決する。

著者は、NSPI を自動化された多項式不等式証明のフロンティアの重要な拡張として位置づけており、既存の自動化システムでは以前は解けなかった高次元のケース（最大 10 変数）を成功裡に処理している。この研究は、ヒューリスティックな発見と厳密な証明を組み合わせることで、自動化された数学的推論の実用的な範囲を大幅に拡大できることを示している。