💻 computer science

COMPOSE: Composing Future Theorems from Citations and Formal Structure

本論文は、科学的引用文脈と形式的定理依存性を同時に活用して妥当な将来の数学的定理を生成する二重グラフフレームワーク「COMPOSE」を導入し、新たに構築されたデータセットとベンチマークを通じて優れた性能を実証する。

原著者： David Busbib, Michael Werman

公開日 2026-05-29

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

原著者： David Busbib, Michael Werman

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

特定の数学分野における次の大ヒットを予測しようとしていると想像してください。将来の論文が何を述べるか推測したいが、単にランダムな数学用語を捏造するわけではありません。あなたの推測は妥当であること、つまり現在の議論に合致しつつ、数学が要求する厳密な論理の規則に従っていることを意味します。

本論文は、まさにそれを実現するために設計された新しいシステムCOMPOSE（引用と形式的構造から将来の定理を構成する）を紹介します。

その仕組みを、簡単な概念に分解して説明します。

問題：2 つの異なる地図

数学の未来を予測するには、通常 2 つの要素が必要ですが、既存のツールは片方しか見ていません。

「社会的」地図（引用）：これはパーティーで誰が誰と話しているかを見るようなものです。論文 A が論文 B を引用している場合、彼らは会話を行っています。これにより、どのトピックが人気で、研究がどこに向かっているかがわかります。
「論理」地図（形式的構造）：これはゲームのルールブックのようなものです。数学では、何でも言えるわけではなく、過去のステップを用いて証明する必要があります。この地図は、厳密な依存関係を示します。「定理 X を証明するには、まず補題 Y を知っている必要がある」といった具合です。

問題点：

「社会的」地図だけを見ると、人気はあるが論理的に不可能なトピック（基礎なしで家を建てようとするような）を推測してしまう可能性があります。
「論理」地図だけを見ると、論理的に完璧な証明が見つかるかもしれませんが、それはもう誰も関心を持っていないトピックに関するものか、あるいは分野が向かっている「全体像」を見逃している可能性があります。

解決策：COMPOSE

著者たちは、バイリンガルの通訳者でありながら探偵のような役割を果たすシステムを構築しました。これは、両方の地図を同時に見ています。

入力：システムに「アンカー論文」（現在の数学論文）を与えます。
二重グラフ：
- 科学グラフの構築：アンカー論文とそれが引用する論文を見て、アイデアと会話のウェブを作成します。
- 形式グラフの構築：それらの論文に含まれる数学的定理を取り出し、それらの「公式」バージョンをMathlib（検証済みの数学証明の巨大なデジタル図書館のようなもの）の中で見つけます。その後、それらの公式バージョン間の論理的依存関係を追跡します。
融合：システムは、特別な「ニューラルネットワーク」（AI の一種）を使用して、これら 2 つの地図を統合します。会話（引用）が規則（形式的論理）とどのように結びついているかを学習します。
出力：システムは、現在の議論に合致し、かつ論理的規則に従う新しい妥当な数学的主張（「将来の定理」）を生成します。

類比：チェスにおける次の手を予測する

複雑なチェスのゲームで次の手を予測しようとしていると想像してください。

古い手法は、人気のあるチェスのオープニングのリスト（「社会的」地図）を見るようなものでした。「キングズ・ギャンビット」を指すかもしれないと推測できましたが、その手が実際に合法かどうか、あるいは即座にチェックメイトされてしまうかどうかは知りませんでした。
COMPOSEは、ゲームの歴史（誰が以前に何を指したか）とチェスの厳密な規則（駒の動き方）の両方を見るグランドマスターのようなものです。それは、単に人気のある戦略であるだけでなく、現在の盤面状態に適合する合法で堅実な手を予測します。

検証方法

研究者たちは単に推測したわけではありません。彼らは大規模なテストセットを構築しました。

108,000 件の論文とそれに対応する形式的論理構造の例を収集しました。
2024 年後半と 2025 年に発表された論文（モデルがまだ見ていないもの）を用いて「将来テスト」を作成しました。
モデルに尋ねました。「この古い論文に基づいて、次の論文は何を述べるでしょうか？」

結果：

より優れた推測：COMPOSE は、他の AI モデルよりも将来の論文の正確なトピックを推測する能力がはるかに優れていました。
より根拠のある内容：人間の審査員（および他の AI）が出力をレビューした際、COMPOSE の推測は、数学的に深みがあり、具体的で正確であるという点で高い評価を受けました。
秘密の武器：「社会的」地図または「論理」地図のいずれかを無効にしたとき、システムの性能は低下しました。これは、良い予測を行うためには両方が本当に必要であることを証明しました。

限界（「盲点」）

本論文は、1 つの弱点を認めています。システムが機能するには「論理地図」（Mathlib）に依存しています。数学のトピックが非常に新しく、あるいはニッチで、まだ形式的な図書館に記述されていない場合、システムは混乱し、新しいトピックを古い無関係なカテゴリーに無理やり当てはめようとする可能性があります（異なる楽器の規則を使って新しい種類の音楽を説明しようとするようなものです）。

まとめ

COMPOSEは、数学者たちが何について話しているかと、彼らの論理が実際にどのように機能するかを組み合わせることで、数学の未来を予測するのを助けるツールです。これは、将来の予測が単に流暢に聞こえるだけのナンセンスではなく、分野の歴史と数学の厳密な規則の両方に根ざしたものになることを保証します。

技術的サマリー：COMPOSE – 引用と形式的構造からの未来の定理の構成

問題定義

本論文は、与えられた「アンカー」論文に対して、妥当な未来の数学的主張（定理に似た記述）を予測する課題であるグラウンデッドな未来の数学的生成の課題に取り組む。著者らは、有効な予測は以下の 2 つの同時制約を満たさなければならないと主張する：

科学的軌道：科学的引用グラフおよび文献におけるアイデアの進化が示す研究方向を拡張しなければならない。
形式的グラウンディング：形式的数学に内在する論理的依存関係を尊重し、主張が既存の定義、補題、定理から妥当に導出可能であることを保証しなければならない。

既存のアプローチは通常、これらのソースのいずれか一方のみをモデル化する。科学テキストのみに基づいて訓練されたモデルは、流暢だが論理的にグラウンディングされていない主張を生成する可能性があり、一方、定理証明システムは形式的構造上で推論するが、有望な研究方向を特定するための科学的文脈を欠いている。本論文は、科学論文と形式的ライブラリ（Mathlib など）が知識を組織化する方法に根本的な違いがあるため、これらの相補的なソースを組み合わせることは容易ではないと位置づけている。

手法：COMPOSE フレームワーク

著者らは、科学的引用文脈と形式的定理構造の両方に言語モデルを条件付けるCOMPOSEという双グラフフレームワークを提案する。このアプローチは、以下の 3 つの主要な構成要素からなる：

1. データ構築

著者らは、arXiv の数学論文（2000 年～2023 年）と Lean Mathlib ライブラリから導出された108,000 件のペア化された科学 - 形式グラフ例のデータセットを構築した。

科学グラフ ( $G_s$ )：アンカー論文とその引用文脈（最大 2 ホップ）から構築される。論文の要約ノードと、テキストから抽出された定理ノードを含む。エッジは引用リンクと論文内の依存関係を表す。
形式グラフ ( $G_f$ )：抽出された非形式的な定理を Mathlib の対応する定理に整合させることで構築される。この整合には、直接の自動形式化のノイズを回避するために、Mathlib の定理に対する人間による非形式的記述のコーパスであるFrenzyMathを用いた非形式から非形式への検索が用いられる。形式グラフは、LeanDojo を介して抽出された依存エッジを用いて、一致した定理のルートから拡張される。
ベンチマーク：2024 年末および 2025 年の実際の出版された結果を予測するモデルの能力を評価するために使用される、2024 年末および 2025 年の47,000 件の未来の論文からなる時間的に保持されたテストセット。

2. モデルアーキテクチャ

COMPOSE は、双エンコーダアーキテクチャにグラフ条件付きデコーダを続けた構成を採用する：

双エンコーダ：2 つの専用グラフニューラルネットワーク（GNN）が $G_s$ $G_{s}$ と $G_f$ $G_{f}$ を個別に処理する。
- $G_s$ のノードは、E5 埋め込み（科学テキスト）で初期化される。
- $G_f$ のノードは、DeepSeek-Math 埋め込み（形式的署名）で初期化される。
- 両方とも、ゲート付き残差接続を備えた、有向かつエッジタイプ固有のメッセージパッシングを使用する。
融合モジュール：両方のグラフからの表現は共有潜在空間に投影され、双方向のクロスアテンション機構を介して融合される。これにより、モデルは科学的方向性を形式的制約と統合できる。
デコーダ：LoRA で適応された事前学習済みの数学特化型 LLM（DeepSeek-Math-7B または Mistral-7B）。クロスアテンション層がデコーダに挿入され、融合されたグラフ埋め込みに基づいて生成を条件付けることで、トークン生成中にモデルが完全なグラフ構造にアテンションできるようにする。

3. 2 段階学習

ステージ 1（表現学習）：デコーダなしで、グラフエンコーダと融合モジュールを 3 つの目的関数を用いて訓練する：
- リンク予測：エンコーダがグラフ構造を捉えることを保証するため。
- 対照的整合：融合されたグラフ表現をターゲット論文の要約と主要な主張に整合させるため。
- クロス整合：非形式的な定理ノードを一致した形式的対応物に明示的に整合させるため。
ステージ 2（生成）：デコーダを追加し、以下の手法で微調整する：
- 自己回帰損失：標準的な次のトークン予測。
- グラフマージン損失：不一致のグラフペアに対して同じテキストを生成した場合にモデルを罰する正則化項であり、モデルに特定のグラフ文脈に依存させる。

主要な結果

実験は、47K 未来論文ベンチマークで行われ、COMPOSE は強力なベースライン（GIANTS、FutureGen、GoAI、および各種テキストのみまたはプロンプトのみの変種を含む）と比較された。

検索性能：COMPOSE は、生成されたテキストと真の未来の論文との間のコサイン類似度と、無関係な論文との間の差として定義される最高値のGap（0.240）を達成した。また、H@10（50.8%）およびH@100（80.8%）においてベースラインを大幅に上回り、生成された主張がプールから正しい未来の論文を検索する可能性がはるかに高いことを示している。
新規数学的主張の予測（NMCP）：COMPOSE は、Precision（0.560）および Match（0.730）で首位となり、その出力がトピックだけでなく、形式的および非形式的の両方のレベルで未来の定理と整合していることを示した。
LLM ジャッジ評価：LLM ジャッジ（GPT-4.0）が、内容、深さ、新規性、精度、具体性の観点から出力を評価した。COMPOSE は、全体スコア（3.36/5）で最高を記録し、特に技術的深さ（3.52）と具体性（3.52）において、しばしば曖昧な要約を生成するベースラインよりも具体的で数学的に豊かな出力を生成した。
アブレーション研究：科学的または形式的グラフエンコーダのいずれかを除去すると、性能が大幅に低下し、両方のモダリティが相補的なシグナルを提供していることが確認された。形式グラフはグラウンディングに不可欠であり、科学的グラフは正しい研究方向を特定するために不可欠であった。

意義と主張

本論文は、未来の数学的生成は、科学的文脈と形式的構造を組み合わせることで恩恵を受けると主張する。

グラウンデッドな生成：著者らは、科学テキストのみに依存すると、トピック的には関連しているが論理的にグラウンディングされていない主張が生じ、形式的構造のみに依存すると、モデルは既知の定理に限定され、新しい方向性を予測できなくなることを実証した。COMPOSE はこのギャップを成功裏に埋めている。
データ貢献：108K のペア化データセットと 47K の未来論文ベンチマークの構築は、この分野における時間的ベンチマークの欠如に対処し、グラウンデッドな数学的生成を評価するための新たなリソースを提供する。
方法論的進展：クロスアテンション融合を備えた双グラフフレームワークは、非形式的文献対形式的論理といった異種知識ソースを生成タスクに統合するための新たなアプローチを提供する。

著者らは、この手法が近似された非形式 - 形式の整合（Mathlib のカバレッジが希薄な領域ではノイズを導入する可能性がある）に依存しており、生成された主張が証明アシスタントによって検証されるのではなく、検索や LLM ベースの評価を代理シグナルとして依存しているという限界を指摘している。彼らは、将来の研究において、生成された主張の形式的正確性を直接検証するために、証明を意識した検証を組み込むことを提案している。