現代の科学的展望において、人工知能は単なるデータ処理の役割から、発見者としての役割へと踏み出し始めています。私たちは、新しい化学物質を提案し、斬新な材料を提言し、さらには人間がまだ考慮していない数学的予想さえも定式化できる機械を目にしています。この変化は、深遠な問いを投げかけます。もし機械が画期的な成果のように見える答えを生み出したとき、それが単に学習中に記憶したものを巧みに繰り返しているだけではなく、真に創造的であると、どのようにして判断すればよいのでしょうか。科学における真の創造性には、二つのことが必要です。すなわち、解決策が独創的であること（つまり、以前に見たことがないものであること）、そして効果的であること（つまり、実際に機能し、目の前の問題を解決すること）です。困難は、これらの性質を検証することにあります。多くの分野では、新しいアイデアが妥当かどうかを判断するために、人間の専門家がその結果を見て判断する必要がありますが、これは遅く、主観的なプロセスです。答えを絶対的な確実性をもってチェックできる数学においては、課題は異なります。問題があまりにも複雑であるため、コンピュータはすべての可能性を単純に探索して答えを見つけることができず、また、問題自体が機械がすでに学習済みである可能性のある固定された集合であることも多いのです。
このジレンマを解決するために、バージニア大学の研究者たちは、人工知能をテストするための新しい方法、彼らがALPSと呼ぶベンチマークを開発しました。このシステムは、記憶や標準的なルーチンに従うことでは解決できない特定の種類の数学パズルを提示することで、「妥当な創造性」を測定するように設計されています。パズルは、一連のアイテムをどのように組み合わせることができるかというルールに基づいています。オブジェクトのコレクションと、それらのうち任意の二つを混ぜ合わせるためのルールを想像してください。研究者たちは、これらのオブジェクトがどのように振る舞わなければならないかを記述する、特定のルール、あるいは「法則」を生成します。機械の任務は、次の二つのうちいずれかを決定することです。そのルールが非常に制限的であり、すべてのオブジェクトを同一のものにするのか、あるいは、そのルールが条件を満たす複雑で無限の構造を持つオブジェクトを許容するのか、という点です。もし機械がその構造が存在すると主張する場合、その記述を構築しなければなりません。もしオブジェクトが同一でなければならないと主張する場合、他に可能性が存在しないことを証明しなければなりません。このセットアップの素晴らしさは、人間が結果を見る必要なく、コンピュータによって完璧な精度で答えをチェックできる点にあります。さらに、このシステムはこれらの一連のパズルを無限に生成できるため、機械は常に一度も見聞きしたことのない問題に直面することになります。
研究者たちは、論理的な問題を解くために設計された特化したコンピュータプログラムである、さまざまな強力な自動推論ツールを用いてこのシステムをテストしました。彼らは、生成された四千件以上の法則のプールに対してこれらのツールを実行しました。結果は明白でした。計算能力を大幅に増大させたとしても、自動化されたツールはごくわずかな問題しか解決できませんでした。具体的には、最高のプロバー（証明器）を用いた8つの異なる構成のポートフォリオは、わずか約2パーセントの法則しか解決できませんでした。研究者が計算予算を20倍に増やしたところ、追加の解決策はわずか数件しか見つからず、それらは探していた複雑な構造ではなく、オブジェクトが同一であることを示す証明に過ぎませんでした。このことは、これらの問題を解決する上での障壁が、計算能力の不足ではなく、それぞれの固有の法則に合わせた特定の構造を発明する方法の欠如であることを示唆しています。機械は、適切な種類の無限の構造をゼロから構築する方法を知らないのです。
研究者たちは、その後、今日の対話型ツールを動かしているものと同じタイプの人工知能である、大規模言語モデルに目を向けました。彼らは最強の推論モデルに対し、同じパズルと、答えを証明するための同じ機会を与えてテストを行いました。機械がすべてのオブジェクトが同一であることを証明するというタスクの側では、最高のモデルは約14パーセントのケースで成功しましたが、それは単純な問題に限られていました。一方で、機械が新しい無限の構造を構築しなければならない側のタスクでは、結果はさらに明白でした。どのモデルも成功しませんでした。モデルが構造を構築しようと試みた際、それらは一貫して二つの方法のいずれかで失敗しました。あるいは、構造が硬すぎて、すべてのオブジェクトを単一の点へと崩壊させ、複雑な解を示すことに失敗するか、あるいは、構造が緩すぎて、従おうとしている法則のルールを守ることができなかったかのどちらかでした。あらゆる事例において、機械はルールの遵守と、新しい複雑なものを創造することのバランスを取ることができなかったのです。
この研究は、これらの人工知能システムは指示に従ったり、自身の作業をチェックしたりすることは上手くなっているものの、科学的発見の核心である「制約に適合する新しい構造を発明すること」には依然として苦戦していると結論付けています。研究者たちは、パズルを生成するジェネレーターと、答えをチェックする自動判定器を含むシステム全体を公開しました。これにより、他の科学者たちが、新鮮な問題が尽きることを心配することなく、これらのモデルをテストし、改善し続けることができます。今回の知見は、科学におけるAIの進むべき道は、より多くのデータや時間を機械に与えることではなく、創造と検証のループの中で、自らのアイデアを提案し、洗練させる方法を教えることにあるかもしれないと示唆しています。機械がこれらのカスタマイズされた解決策を確実に構築できるようになるまで、科学的発見における彼らの役割は限定的なままであり、情報の処理と、真に妥当で独創的な知識の生成との間の溝を越えることはできないでしょう。
技術要約：ALPS – 数学的構成を用いた大規模言語モデルにおける妥当な創造性の測定
1. 問題提起
科学的領域（例：定理証明、分子設計）における大規模言語モデル（LLM）の現在の評価は、**妥当な創造性（valid creativity）**と、単なる記憶や定型的な実行を区別することに苦慮している。ある解決策が「妥当に創造的」であると見なされるには、以下の2つの基準を同時に満たさなければならない：
- 独創性（Originality）： その解決策が訓練データの反復や既知の一般的手続きではないこと。
- 有効性（Effectiveness）： その解決策が客観的に正しく、特定のタスクに対して価値を提供すること。
既存のベンチマークは、以下の3つの特性のうち少なくとも1つを欠いているため、この組み合わせを確実に測定できていない：
- 検証可能性（Verifiability）： 解決策が（主観的な判断ではなく）客観的にチェック可能であること。
- 更新可能性（Renewability）： 訓練データの汚染を防ぐために、新しい問題インスタンスを無制限に生成できること。
- 構成性（Constructiveness）： タスクが特定のインスタンスに合わせた解決策を要求し、記憶や標準的なアルゴリズムによる解決を防ぐこと。
静的なコーパス（例：MATH, miniF2F）は更新可能性に欠け、合成パズル（例：ランダムなSAT）はしばしば定型的な手続きによって解けてしまうため構成性に欠け、オープンな発見タスク（例：分子設計）は主観的な人間による判断のために検証可能性に欠けることが多い。
2. 手法：ALPS ベンチマーク
著者らは、等式理論の領域内でこれら3つの特性を同時に満たすように設計されたベンチマーク、ALPS (Austin-Law Proof-Synthesis) を導入する。
問題の定式化：
- 領域： ALPSは、マグマ（単一の二項演算 ⋄ を持つ集合）および等式法則（全称量化された恒等式）を扱う。
- タスク： 各インスタンスは、項 T が5次以上の順序を持つ形式 x=T[x,y,z,…] の法則 L である。
- 二分法： このような法則に対し、以下の2つの条件のいずれか一方のみが成立する：
- 自明（Trivial）： 法則が x=y を導き、すべてのモデルが単一の要素に崩壊する。
- オースティン（Austin）： 法則が非自明なモデルを持ち、そのモデルは必然的に無限である（すべての有限な非自明モデルは、本ベンチマークの認証プロセスによって排除されているため）。
- 課題： ソルバーは、L⊨x=y という演繹的証明（自明な側）を提示するか、あるいは L を満たす無限のマグマを構成（オースティンの側）しなければならない。
コーパスの構築：
- 生成： コーパスは拡張エンジンを通じて成長する。既知のオースティン法則から出発し、項 T 内の変数を新しい演算（例：v→v⋄w）で再帰的に置き換える。これにより、未見の新鮮な問題を無制限に生成できることが保証される。
- スクリーニングと適格性： 候補は厳格なスクリーニング・パイプラインを経る：
- 有限モデル・フィルター： 非自明な有限モデルを持つ法則を破棄する。
- 適格性プローバー： 自動証明器を用いて、非自明な有限モデルが存在しないことを認証する。これは、有限な担体において単射写像は全射であるという論理的帰結に基づいている。プローバーは、法則と部分項の全射性から矛盾を導き出し、いかなるモデルも無限であることを認証する。
- 重複排除： 同値な法則（相互に含意関係にあるもの）を等価クラスにグループ化し、個別の問題数を確保する。
- 結果としてのプール： 生成された候補から、著者らは4,141個の未解決の法則（「ハード・ティア」）と、より小規模な「認証済み容易（certified-easy）」な法則のセットを作成した。
回答検証（自動ジャッジ）：
ジャッジは、人間の介入なしに、2つの異なる完全に自動化されたチャネルを通じて提出物を検証する：
- 自明な側： LLMは等式の連鎖を提出する。ハーネスはこれを Lean 証明へと自動形式化し（Lean カーネルによってチェックされる）、L⟹∀a,b:a=b であることを検証する。
- 構成の側： LLMは有限の等式の集合 E（プレゼンテーション）を提出する。ジャッジは、自動定理証明器（Vampire, E, Tweeなど）を用いて2つの主張を検証する：
- 導出： E⊢L （E のすべてのモデルは L を満たす）。
- 充足可能性： E∪{a=b} は充足可能である（E の少なくとも2つの異なる要素を持つモデルが存在する）。
- 両方が成立する場合、インスタンスの適格性証明により、そのモデルは無限であることが保証される。
3. 主な貢献
- 二面的な構成タスク： すべてのインスタンスが確定した答え（自明または無限）を持つように認証されており、創造的な構成の必要性を孤立させたベンチマーク。
- 更新可能なコーパスとジェネレーター： 訓練データによる汚染を避けるため、制限なく新鮮なインスタンスを生成できる公開ジェネレーター。
- 自動ジャッジ： 人間の判定なしに、独立したチャネル（自明性のためのLean、構成のための自動証明器の証明書）を通じて提出物を認証するシステム。
- 強力な自動ベースライン： 先行するプローバーの8つの構成のポートフォリオにより、自動化の「手法による限界（method-bound limit）」を確立した。
4. 実験結果
自動プローバーの性能：
- 8つの構成からなるポートフォリオは、4,141個の法則の評価プールに対してわずか 2.2% しか解決できなかった。
- 計算予算を20倍に増やしても、解決された法則はわずか 0.6% の増加にとどまった（すべて自明性の証明であり、新しいモデルは見つからなかった）。
- テストされたどの構成によっても 97.2% のプールが未解決のままであり、これは障害が計算量の不足ではなく、適合した無限構造を構成する手法の欠如にあることを示している。
- 副次的発見： 著者らは、Equational Theories Project (ETP) によって未解決のまま残されていた5次の法則を解決し、飽和を通じて無限モデルの存在を確認した。
LLMの性能：
- 自明な側： 63個の「認証済み容易」な法則のセットにおいて、最も強力なモデルである o3 は、ウェイポイント（プローバーによる導出された補題）を用いることで 14% のパス率（9つの解決策）を達成し、用いない場合は 9.5% であった。GPT-4.1 および o4-mini は 0% であった。
- 失敗モード： LLMは主に、法則から導出できないステップを含む連鎖を提出したことが原因で失敗し、ハーネスによって拒絶された。
- 構成の側： 「ハード・ティア」のサンプル（自動化によって未解決の法則）25個において、どのLLMも 検証済みの解決策を生成できなかった。
- 失敗モード： 提出物は、強すぎる（法則を包含しているが、単一要素に崩壊してしまい、区別性のチェックに失敗した）か、あるいは弱すぎる（異なる要素を許容しているが、法則を満たしていない）かのいずれかであった。
- o3 は、25個の法則すべてにおいて、正確に一方のチェックのみをクリアした。o4-mini と GPT-4.1 は、多くの法則において両方のチェックに失敗した。
5. 意義と主張
本論文は、ALPSが記憶や定型的な実行という混同要因を取り除くことで、妥当な創造性をうまく分離できていると主張している。
- 創造性の必要性： 自動プローバーおよびLLMの失敗率の高さは、これらの問題が既存の一般的な手続きや総当たり探索では解決できないことを示している。
- 失敗の性質： 特徴的な失敗プロファイル（自明な証明における無効なステップ、構成における「強すぎる／弱すぎる」プレゼンテーション）は、現在のモデルが制約下での創造的な生成に苦慮していることを浮き彫りにしている。構造をドラフトすることはできても、退化した解決策に陥ることなくグローバルな仕様のバランスを取ることに失敗している。
- 科学的パラレル： 本論文は、科学的発見（例：分子設計）における「特定・構成・検証」のサイクルとの類似性を指摘しており、ALPSはすべてのフェーズを機械的に検証可能にしている。
- 今後の方向性： 著者らは、今後の道筋は「検証と洗練（verify-and-refine）」のループ（Counterexample-Guided Inductive Synthesis、CEGISに類似）にあると考えている。ここでは、ソルバーが構造をドラフトし、妥当性に関する自動化されたフィードバックを受け取り、それを修正していく。
著者らは、最強のLLMが容易なインスタンスに対してある程度の能力を示しているものの、現在はハードなインスタンスにおける有効な無限構造の構成に失敗しており、このベンチマークは依然として大部分が未解決であることを述べ、謙虚な姿勢を維持している。
毎週最高の AI 論文をお届け。
スタンフォード、ケンブリッジ、フランス科学アカデミーの研究者に信頼されています。
受信トレイを確認して登録を完了してください。
問題が発生しました。もう一度お試しください。
スパムなし、いつでも解除可能。
週刊ダイジェスト — 最新の研究をわかりやすく。登録