💻 computer science

COMPOSE: Composing Future Theorems from Citations and Formal Structure

Die Arbeit stellt COMPOSE vor, ein Dual-Graph-Framework, das plausible zukünftige mathematische Theoreme generiert, indem es wissenschaftliche Zitierkontexte und formale Theorem-Abhängigkeiten gemeinsam nutzt, und demonstriert durch einen neu erstellten Datensatz und Benchmark eine überlegene Leistung.

Ursprüngliche Autoren: David Busbib, Michael Werman

Veröffentlicht 2026-05-29

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: David Busbib, Michael Werman

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, den nächsten großen Durchbruch in einem bestimmten Bereich der Mathematik vorherzusagen. Sie möchten erraten, was eine zukünftige Arbeit aussagen wird, möchten aber nicht einfach zufällige mathematische Begriffe erfinden. Sie möchten, dass Ihre Vorhersage plausibel ist – das heißt, sie passt in die aktuelle Diskussion und folgt den strengen Regeln der Logik, die die Mathematik erfordert.

Diese Arbeit stellt ein neues System namens COMPOSE (Composing Future Theorems from Citations and Formal Structure) vor, das genau dies bewerkstelligen soll.

So funktioniert es, aufgeteilt in einfache Konzepte:

Das Problem: Zwei verschiedene Karten

Um die Zukunft der Mathematik vorherzusagen, benötigen Sie normalerweise zwei Dinge, doch bestehende Werkzeuge betrachten nur eines:

Die „soziale" Karte (Zitationen): Dies ist wie der Blick darauf, wer mit wem auf einer Party spricht. Wenn Paper A Paper B zitiert, führen sie ein Gespräch. Dies verrät Ihnen, welche Themen populär sind und wohin die Forschung strebt.
Die „Logik"-Karte (Formale Struktur): Dies ist wie das Regelbuch eines Spiels. In der Mathematik kann man nicht einfach irgendetwas behaupten; man muss es unter Verwendung vorheriger Schritte beweisen. Diese Karte zeigt die strengen Abhängigkeiten: „Sie können Theorem X nur beweisen, wenn Sie Lemma Y bereits kennen."

Das Problem:

Wenn Sie nur die soziale Karte betrachten, könnten Sie ein Thema erraten, das populär, aber logisch unmöglich ist (wie der Versuch, ein Haus ohne Fundament zu bauen).
Wenn Sie nur die Logik-Karte betrachten, könnten Sie einen logisch perfekten Beweis finden, aber er könnte ein Thema betreffen, das niemanden mehr interessiert, oder er könnte das „große Ganze" verpassen, wohin sich das Feld entwickelt.

Die Lösung: COMPOSE

Die Autoren entwickelten ein System, das wie ein zweisprachiger Übersetzer fungiert, der gleichzeitig ein Detektiv ist. Es betrachtet beide Karten gleichzeitig.

Die Eingabe: Sie geben dem System ein „Anker-Paper" (ein aktuelles mathematisches Paper) an.
Der Dual-Graph:
- Es baut einen wissenschaftlichen Graphen: Es betrachtet das Anker-Paper und die Papers, die es zitiert, und erstellt ein Netz aus Ideen und Gesprächen.
- Es baut einen formalen Graphen: Es nimmt die mathematischen Theoreme innerhalb dieser Papers und findet ihre „offiziellen" Versionen in einer riesigen digitalen Bibliothek namens Mathlib (die wie eine verifizierte Enzyklopädie mathematischer Beweise ist). Anschließend verfolgt es die logischen Abhängigkeiten zwischen diesen offiziellen Versionen.
Die Fusion: Das System verwendet ein spezielles „neuronales Netz" (eine Art KI), um diese beiden Karten zu verschmelzen. Es lernt, wie das Gespräch (Zitationen) mit den Regeln (formale Logik) verbunden ist.
Die Ausgabe: Das System generiert eine neue, plausible mathematische Behauptung (ein „zukünftiges Theorem"), die in die aktuelle Diskussion passt und die logischen Regeln einhält.

Die Analogie: Der nächste Zug im Schach

Stellen Sie sich vor, Sie versuchen, den nächsten Zug in einem komplexen Schachspiel vorherzusagen.

Alte Methoden waren wie das Betrachten einer Liste beliebter Schacheröffnungen (die „soziale Karte"). Sie konnten erraten, dass Sie vielleicht ein „Königs-Gambit" spielen würden, aber sie wusnten nicht, ob dieser Zug tatsächlich legal war oder ob er Sie sofort mattsetzen würde.
COMPOSE ist wie ein Großmeister, der die Geschichte des Spiels betrachtet (wer was vorher gespielt hat) und die strengen Schachregeln (wie die Figuren ziehen). Es sagt einen Zug voraus, der nicht nur eine beliebte Strategie ist, sondern auch ein legaler, solider Zug, der zum aktuellen Brettzustand passt.

Wie sie es testeten

Die Forscher haben nicht einfach nur geraten; sie bauten einen massiven Testdatensatz.

Sie sammelten 108.000 Beispiele von Papers und ihren entsprechenden formalen Logikstrukturen.
Sie schufen einen „Zukunfts-Test" mit Papers, die Ende 2024 und 2025 veröffentlicht wurden (die das Modell noch nicht gesehen hatte).
Sie fragten das Modell: „Basierend auf diesem alten Paper, was wird das nächste Paper sagen?"

Die Ergebnisse:

Bessere Vorhersagen: COMPOSE war viel besser darin, das genaue Thema des zukünftigen Papers zu erraten als andere KI-Modelle.
Mehr Fundiertheit: Wenn menschliche Richter (und andere KIs) die Ausgabe überprüften, wurden die Vorhersagen von COMPOSE höher bewertet, weil sie mathematisch tiefgründiger, spezifischer und genauer waren.
Das Geheimnis: Als sie entweder die „soziale Karte" oder die „Logik-Karte" ausschalteten, wurde das System schlechter. Dies bewies, dass Sie wirklich beide benötigen, um eine gute Vorhersage zu treffen.

Eine Einschränkung (Der „blinde Fleck")

Die Arbeit gibt eine Schwäche zu: Das System ist auf die „Logik-Karte" (Mathlib) angewiesen, um zu funktionieren. Wenn ein mathematisches Thema sehr neu oder nischig ist und noch nicht in der formalen Bibliothek niedergeschrieben wurde, könnte das System verwirrt werden und versuchen, das neue Thema in eine alte, nicht verwandte Kategorie zu zwingen (wie der Versuch, eine neue Musikart mit den Regeln eines anderen Instruments zu erklären).

Zusammenfassung

COMPOSE ist ein Werkzeug, das hilft, die Zukunft der Mathematik vorherzusagen, indem es das, worüber Mathematiker sprechen, mit der Funktionsweise ihrer Logik kombiniert. Es stellt sicher, dass zukünftige Vorhersagen nicht nur fließend klingender Unsinn sind, sondern sowohl in der Geschichte des Fachgebiets als auch in den strengen Regeln der Mathematik fundiert sind.

Technische Zusammenfassung: COMPOSE – Das Komponieren zukünftiger Theoreme aus Zitaten und formaler Struktur

Problemdefinition

Die Arbeit adressiert die Herausforderung der fundierten zukünftigen mathematischen Generierung: die Aufgabe, eine plausible zukünftige mathematische Behauptung (eine theoremaähnliche Aussage) für ein gegebenes „Anker"-Paper vorherzusagen. Die Autoren argumentieren, dass eine valide Vorhersage zwei gleichzeitige Einschränkungen erfüllen muss:

Wissenschaftliche Trajektorie: Sie muss die durch den wissenschaftlichen Zitationsgraphen und die Evolution von Ideen in der Literatur angezeigte Forschungsrichtung erweitern.
Formale Fundierung: Sie muss den logischen Abhängigkeiten innewohnender formaler Mathematik Rechnung tragen und sicherstellen, dass die Behauptung gültig aus bestehenden Definitionen, Lemmata und Theoremen ableitbar ist.

Bestehende Ansätze modellieren typischerweise nur eine dieser Quellen. Modelle, die ausschließlich auf wissenschaftlichen Texten trainiert wurden, können zwar fließende, aber logisch nicht fundierte Behauptungen generieren, während Theorembeweiser-Systeme über formale Strukturen reasoning betreiben, aber den wissenschaftlichen Kontext fehlt, um vielversprechende Forschungsrichtungen zu identifizieren. Die Arbeit postuliert, dass die Kombination dieser komplementären Quellen aufgrund der fundamentalen Unterschiede darin, wie wissenschaftliche Papers und formale Bibliotheken (wie Mathlib) Wissen organisieren, nicht trivial ist.

Methodik: Das COMPOSE-Framework

Die Autoren schlagen COMPOSE vor, ein Dual-Graph-Framework, das ein Sprachmodell sowohl auf wissenschaftlichen Zitationskontext als auch auf formale Theoremstruktur konditioniert. Der Ansatz besteht aus drei Hauptkomponenten:

1. Datenkonstruktion

Die Autoren konstruierten einen Datensatz von 108.000 gepaarten wissenschaftlich-formalen Graphbeispielen, abgeleitet aus arXiv-Mathematik-Papers (2000–2023) und der Lean Mathlib-Bibliothek.

Wissenschaftlicher Graph ( $G_s$ ): Erstellt aus einem Anker-Paper und seinem Zitationskontext (bis zu zwei Hops). Er enthält Knoten für Abstracts von Papers und aus dem Text extrahierte Theoremknoten. Kanten repräsentieren Zitationslinks und interne Paper-Abhängigkeiten.
Formaler Graph ( $G_f$ ): Durch Ausrichtung extrahierter informaler Theoreme auf entsprechende Theoreme in Mathlib konstruiert. Diese Ausrichtung verwendet FrenzyMath (ein Korpus menschlich verfasster informaler Beschreibungen für Mathlib-Theoreme), um eine informal-zu-informal-Abruf durchzuführen und so das Rauschen einer direkten Autoformalisierung zu vermeiden. Der formale Graph erweitert sich vom übereinstimmenden Theorem-Wurzelknoten aus, wobei über LeanDojo extrahierte Abhängigkeitskanten verwendet werden.
Benchmark: Ein zeitlich zurückgehaltener Testset von 47.000 zukünftigen Papers aus dem späten 2024 und 2025, verwendet zur Evaluierung der Fähigkeit des Modells, tatsächliche veröffentlichte Ergebnisse vorherzusagen.

2. Modellarchitektur

COMPOSE verwendet eine Dual-Encoder-Architektur, gefolgt von einem graph-konditionierten Decoder:

Dual Encoder: Zwei dedizierte Graph-Neuronale Netze (GNNs) verarbeiten $G_s$ $G_{s}$ und $G_f$ $G_{f}$ separat.
- $G_s$ -Knoten werden mit E5-Embeddings (wissenschaftlicher Text) initialisiert.
- $G_f$ -Knoten werden mit DeepSeek-Math-Embeddings (formale Signaturen) initialisiert.
- Beide verwenden gerichteten, kantentyp-spezifischen Message Passing mit gated residualen Verbindungen.
Fusionsmodul: Die Repräsentationen beider Graphen werden in einen gemeinsamen latenten Raum projiziert und über einen bidirektionalen Cross-Attention-Mechanismus fusioniert. Dies ermöglicht dem Modell, die wissenschaftliche Richtung mit formalen Einschränkungen zu integrieren.
Decoder: Ein vortrainiertes, mathematikspezifisches LLM (DeepSeek-Math-7B oder Mistral-7B), angepasst mit LoRA. Cross-Attention-Schichten werden in den Decoder eingefügt, um die Generierung auf die fusionierten Graph-Embeddings zu konditionieren, wodurch das Modell während der Token-Generierung die gesamte Graphstruktur beachten kann.

3. Zwei-Stufen-Training

Stufe 1 (Repräsentationslernen): Die Graph-Encoder und das Fusionsmodul werden ohne Decoder mit drei Zielfunktionen trainiert:
- Link Prediction: Um sicherzustellen, dass Encoder die Graphstruktur erfassen.
- Kontrastives Alignment: Um die fusionierte Graphrepräsentation mit dem Abstract und der Hauptbehauptung des Ziel-Papers auszurichten.
- Cross-Alignment: Um informale Theoremknoten explizit mit ihren übereinstimmenden formalen Gegenstücken auszurichten.
Stufe 2 (Generierung): Der Decoder wird hinzugefügt und mit folgenden Mitteln feinabgestimmt:
- Autoregressiver Verlust: Standard-Vorhersage des nächsten Tokens.
- Graph-Margin-Verlust: Ein Regularisierungsterm, der das Modell bestraft, wenn es denselben Text für ein nicht übereinstimmendes Graphpaar generiert, und es zwingt, sich auf den spezifischen Graphkontext zu verlassen.

Wichtige Ergebnisse

Experimente wurden auf dem 47K-zukünftige-Papers-Benchmark durchgeführt, wobei COMPOSE mit starken Baselines (einschließlich GIANTS, FutureGen, GoAI und verschiedenen rein textbasierten oder rein promptbasierten Varianten) verglichen wurde.

Abrufleistung: COMPOSE erreichte die höchste Gap (0,240), definiert als die Differenz der Kosinus-Ähnlichkeit zwischen dem generierten Text und dem wahren zukünftigen Paper im Vergleich zu nicht verwandten Papers. Es übertraf die Baselines signifikant in H@10 (50,8 %) und H@100 (80,8 %), was darauf hindeutet, dass seine generierten Behauptungen viel wahrscheinlicher das richtige zukünftige Paper aus dem Pool abrufen.
Vorhersage neuer mathematischer Behauptungen (NMCP): COMPOSE führte bei Precision (0,560) und Match (0,730), was zeigt, dass seine Ausgaben auf formaler und informaler Ebene mit zukünftigen Theoremen übereinstimmen, nicht nur thematisch.
LLM-Richter-Evaluierung: Ein LLM-Richter (GPT-4.0) bewertete die Ausgaben hinsichtlich Inhalt, Tiefe, Neuheit, Präzision und Spezifität. COMPOSE erzielte die höchste Gesamtpunktzahl (3,36/5), insbesondere bei technischer Tiefe (3,52) und Spezifität (3,52), und produzierte konkretere und mathematisch reichhaltigere Ausgaben als Baselines, die oft vage Zusammenfassungen generierten.
Ablationsstudien: Das Entfernen entweder des wissenschaftlichen oder des formalen Graph-Encoders führte zu signifikanten Leistungseinbußen, was bestätigt, dass beide Modalitäten komplementäre Signale liefern. Der formale Graph war entscheidend für die Fundierung, während der wissenschaftliche Graph unerlässlich für die Identifizierung der richtigen Forschungsrichtung war.

Bedeutung und Behauptungen

Die Arbeit behauptet, dass die zukünftige mathematische Generierung von der Kombination wissenschaftlichen Kontexts mit formaler Struktur profitiert.

Fundierte Generierung: Die Autoren zeigen, dass die alleinige reliance auf wissenschaftlichen Text zu Behauptungen führt, die thematisch relevant, aber logisch nicht fundiert sind, während die alleinige reliance auf formale Struktur das Modell auf bekannte Theoreme beschränkt, ohne neue Richtungen vorherzusehen. COMPOSE überbrückt diese Lücke erfolgreich.
Datenbeitrag: Die Konstruktion des 108K-gepaarten Datensatzes und des 47K-zukünftige-Papers-Benchmarks stellt eine neue Ressource zur Evaluierung fundierter mathematischer Generierung dar und adressiert den Mangel an zeitlichen Benchmarks in diesem Bereich.
Methodischer Fortschritt: Das Dual-Graph-Framework mit Cross-Attention-Fusion bietet einen neuartigen Ansatz zur Integration heterogener Wissensquellen (informale Literatur vs. formale Logik) für generative Aufgaben.

Die Autoren weisen auf Einschränkungen hin, insbesondere dass die Methode auf einer approximativen informal-formalen Ausrichtung beruht (was in Bereichen mit spärlicher Mathlib-Abdeckung Rauschen einführen kann) und dass generierte Behauptungen nicht von einem Beweisassistenten verifiziert werden, sondern stattdessen auf Abruf und LLM-basierter Evaluierung als Proxy-Signale angewiesen sind. Sie schlagen vor, dass zukünftige Arbeiten proof-bewusste Verifikation einbeziehen könnten, um die formale Korrektheit generierter Behauptungen direkt zu überprüfen.