💻 computer science

COMPOSE: Composing Future Theorems from Citations and Formal Structure

Het artikel introduceert COMPOSE, een dual-graph framework dat plausibele toekomstige wiskundige stellingen genereert door wetenschappelijke citatiecontexten en formele stelling-afhankelijkheden gezamenlijk te benutten, waarbij het superieure prestaties aantoont via een nieuw geconstrueerd dataset en benchmark.

Oorspronkelijke auteurs: David Busbib, Michael Werman

Gepubliceerd 2026-05-29

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: David Busbib, Michael Werman

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je probeert de volgende grote doorbraak op een specifiek gebied van de wiskunde te voorspellen. Je wilt raden wat een toekomstig artikel zal zeggen, maar je wilt niet zomaar willekeurige wiskundewoorden verzinnen. Je wilt dat je gok plausibel is—dat wil zeggen, dat het past bij het huidige gesprek en voldoet aan de strenge regels van logica die de wiskunde vereist.

Dit artikel introduceert een nieuw systeem genaamd COMPOSE (Composing Future Theorems from Citations and Formal Structure), ontworpen om precies dat te doen.

Hier is hoe het werkt, opgesplitst in eenvoudige concepten:

Het Probleem: Twee Verschillende Kaarten

Om de toekomst van de wiskunde te voorspellen, heb je meestal twee dingen nodig, maar bestaande tools kijken slechts naar één:

De "Sociale" Kaart (Citaties): Dit is als kijken naar wie met wie praat op een feestje. Als Artikel A Artikel B citeert, hebben ze een gesprek. Dit vertelt je welke onderwerpen populair zijn en waar het onderzoek naartoe gaat.
De "Logica"-Kaart (Formele Structuur): Dit is als het reglement van een spel. In de wiskunde kun je niet zomaar iets zeggen; je moet het bewijzen met behulp van eerdere stappen. Deze kaart toont de strikte afhankelijkheden: "Je kunt Stelling X alleen bewijzen als je Lemma Y al kent."

Het Probleem:

Als je alleen kijkt naar de Sociale Kaart, kun je een onderwerp raden dat populair is maar logisch onmogelijk (zoals proberen een huis te bouwen zonder fundering).
Als je alleen kijkt naar de Logica-kaart, kun je een logisch perfect bewijs vinden, maar het kan gaan over een onderwerp waar niemand meer om geeft, of het mist misschien het "grote plaatje" van waar het vakgebied naartoe gaat.

De Oplossing: COMPOSE

De auteurs hebben een systeem gebouwd dat werkt als een tweetalige vertaler die ook een detective is. Het kijkt tegelijkertijd naar beide kaarten.

De Invoer: Je geeft het systeem een "Ankerartikel" (een huidig wiskundig artikel).
De Dubbele Grafiek:
- Het bouwt een Wetenschappelijke Grafiek: Het kijkt naar het Ankerartikel en de artikelen die het citeert, en creëert een web van ideeën en gesprekken.
- Het bouwt een Formele Grafiek: Het neemt de wiskundige stellingen uit die artikelen en zoekt hun "officiële" versies in een gigantische digitale bibliotheek genaamd Mathlib (wat vergelijkbaar is met een geverifieerde encyclopedie van wiskundebewijzen). Het traceert vervolgens de logische afhankelijkheden tussen die officiële versies.
De Fusie: Het systeem gebruikt een speciaal "neuronaal netwerk" (een type AI) om deze twee kaarten te samenvoegen. Het leert hoe het gesprek (citaties) verbonden is met de regels (formele logica).
De Uitvoer: Het systeem genereert een nieuwe, plausibele wiskundige bewering (een "toekomstige stelling") die past bij het huidige gesprek en de logische regels naleeft.

De Analogie: De Volgende Zet in Schaken Voorspellen

Stel je voor dat je probeert de volgende zet in een complex schaakspel te voorspellen.

Oude methoden waren als kijken naar een lijst van populaire schaakopeningen (de "Sociale Kaart"). Ze konden raden dat je misschien een "Kings Gambit" zou spelen, maar ze wisten niet of die zet eigenlijk legaal was of dat het je direct schaakmat zou zetten.
COMPOSE is als een grootmeester die kijkt naar de geschiedenis van het spel (wie wat eerder speelde) en de strenge regels van schaken (hoe de stukken bewegen). Het voorspelt een zet die niet alleen een populaire strategie is, maar ook een legale, degelijke zet die past bij de huidige bordtoestand.

Hoe Ze Het Testten

De onderzoekers gokten niet zomaar; ze bouwden een enorme testset.

Ze verzamelden 108.000 voorbeelden van artikelen en hun overeenkomstige formele logische structuren.
Ze creëerden een "toekomsttest" met artikelen gepubliceerd in eind 2024 en 2025 (die het model nog niet had gezien).
Ze vroegen het model: "Op basis van dit oude artikel, wat zal het volgende artikel zeggen?"

De Resultaten:

Bessere Gokken: COMPOSE was veel beter in het raden van het exacte onderwerp van het toekomstige artikel dan andere AI-modellen.
Meer Verankerd: Toen menselijke beoordelaars (en andere AI's) de output beoordeelden, scoorden de gokken van COMPOSE hoger omdat ze wiskundig diepgaander, specifieker en accurater waren.
Het Geheime Ingrediënt: Toen ze de "Sociale Kaart" of de "Logica-kaart" uitschakelden, werd het systeem slechter. Dit bewees dat je echt beide nodig hebt om een goede voorspelling te doen.

Een Beperking (Het "Blind Vlek")

Het artikel erkent één zwakte: het systeem is afhankelijk van de "Formele Kaart" (Mathlib) om te werken. Als een wiskundig onderwerp heel nieuw of niche is en nog niet in de formele bibliotheek is opgeschreven, kan het systeem in de war raken en proberen het nieuwe onderwerp in een oude, niet-gerelateerde categorie te forceren (zoals proberen een nieuw type muziek uit te leggen met de regels van een ander instrument).

Samenvatting

COMPOSE is een hulpmiddel dat helpt de toekomst van de wiskunde te voorspellen door te combineren waarover wiskundigen praten met hoe hun logica eigenlijk werkt. Het zorgt ervoor dat toekomstige voorspellingen niet zomaar vloeiend klinkende onzin zijn, maar verankerd zijn in zowel de geschiedenis van het vakgebied als de strenge regels van de wiskunde.

Technische Samenvatting: COMPOSE – Het Samenstellen van Toekomstige Stellingen uit Citaten en Formele Structuur

Probleemdefinitie

Het artikel adresseert de uitdaging van gegronde toekomstige wiskundige generatie: de taak om een plausibele toekomstige wiskundige claim (een stelling-achtige uitspraak) te voorspellen voor een gegeven "anker"-artikel. De auteurs betogen dat een geldige voorspelling moet voldoen aan twee gelijktijdige beperkingen:

Wetenschappelijke Traject: Het moet de onderzoeksrichting uitbreiden die wordt aangegeven door het wetenschappelijke citatienetwerk en de evolutie van ideeën in de literatuur.
Formele Gronding: Het moet de logische afhankelijkheden inherent aan formele wiskunde respecteren, zodat de claim geldig afleidbaar is uit bestaande definities, lemma's en stellingen.

Bestaande benaderingen modelleren doorgaans slechts één van deze bronnen. Modellen die uitsluitend op wetenschappelijke tekst zijn getraind, kunnen vloeiende maar logisch ongegronde claims genereren, terwijl stellingbewijssystemen redeneren over formele structuren maar de wetenschappelijke context missen om veelbelovende onderzoeksrichtingen te identificeren. Het artikel postuleert dat het combineren van deze complementaire bronnen niet triviaal is vanwege de fundamentele verschillen in hoe wetenschappelijke artikelen en formele bibliotheken (zoals Mathlib) kennis organiseren.

Methodologie: Het COMPOSE-kader

De auteurs stellen COMPOSE voor, een dubbel-grafiek kader dat een taalmodel conditioneert op zowel de wetenschappelijke citatiecontext als de formele stellingstructuur. De aanpak bestaat uit drie hoofdcomponenten:

1. Dataconstructie

De auteurs construeerden een dataset van 108.000 gekoppelde wetenschappelijk-formele grafiekvoorbeelden afgeleid van arXiv wiskunde-artikelen (2000–2023) en de Lean Mathlib-bibliotheek.

Wetenschappelijke Grafiek ( $G_s$ ): Opgebouwd uit een ankerartikel en zijn citatiecontext (tot twee sprongen). Het bevat abstracte knopen voor artikelen en stellingknopen die uit de tekst zijn geëxtraheerd. Randen vertegenwoordigen citatielinks en interne artikelafhankelijkheden.
Formele Grafiek ( $G_f$ ): Geconstrueerd door geëxtraheerde informele stellingen af te stemmen op overeenkomstige stellingen in Mathlib. Deze afstemming maakt gebruik van FrenzyMath (een corpus van handgeschreven informele beschrijvingen voor Mathlib-stellingen) om informeel-naar-informeel retrieval uit te voeren, waardoor de ruis van directe autoformalisatie wordt vermeden. De formele grafiek breidt zich uit vanuit de gematchte stellingwortel met behulp van afhankelijkheidsranden die via LeanDojo zijn geëxtraheerd.
Benchmarks: Een tijdelijk terughoudende testset van 47.000 toekomstige artikelen van eind 2024 en 2025, gebruikt om het vermogen van het model om daadwerkelijke gepubliceerde resultaten te voorspellen, te evalueren.

2. Modelarchitectuur

COMPOSE maakt gebruik van een dubbele-encoder architectuur gevolgd door een grafiek-geconditioneerde decoder:

Dubbele Encoders: Twee toegewijde Graph Neural Networks (GNN's) verwerken $G_s$ $G_{s}$ en $G_f$ $G_{f}$ afzonderlijk.
- $G_s$ -knopen worden geïnitieerd met E5-embeddings (wetenschappelijke tekst).
- $G_f$ -knopen worden geïnitieerd met DeepSeek-Math-embeddings (formele handtekeningen).
- Beide maken gebruik van gerichte, randtype-specifieke berichtoverdracht met afgesloten residuale verbindingen.
Fusiemodule: De representaties van beide grafieken worden geprojecteerd in een gedeelde latente ruimte en gefuseerd via een bidirectionele cross-attention mechanisme. Dit stelt het model in staat de wetenschappelijke richting te integreren met formele beperkingen.
Decoder: Een vooraf getrainde wiskunde-specialistische LLM (DeepSeek-Math-7B of Mistral-7B) aangepast met LoRA. Cross-attention lagen worden in de decoder ingevoegd om de generatie te conditioneren op de gefuseerde grafiek-embeddings, waardoor het model tijdens de token-generatie naar de volledige grafiekstructuur kan attenderen.

3. Tweestaps Training

Fase 1 (Representatieleren): De grafiek-encoders en fusiemodule worden getraind zonder de decoder met drie doelen:
- Link Prediction: Om ervoor te zorgen dat encoders de grafiekstructuur vastleggen.
- Contrastieve Afstemming: Om de gefuseerde grafiekrepresentatie af te stemmen op het abstract en de hoofdclaim van het doelartikel.
- Cross-Afstemming: Om informele stellingknopen expliciet af te stemmen op hun gematchte formele tegenhangers.
Fase 2 (Generatie): De decoder wordt toegevoegd en fijngefineerd met behulp van:
- Autoregressieve Verlies: Standaard volgende-token voorspelling.
- Grafiek Margin Verlies: Een regularisatieterm die het model straft als het dezelfde tekst genereert voor een niet-gematchte grafiekkoppel, waardoor het wordt gedwongen zich te verlaten op de specifieke grafiekcontext.

Belangrijkste Resultaten

Experimenten werden uitgevoerd op de 47K toekomstige artikel-benchmark, waarbij COMPOSE werd vergeleken met sterke baselines (waaronder GIANTS, FutureGen, GoAI, en diverse alleen-tekst of alleen-prompt varianten).

Retrieval Performance: COMPOSE behaalde de hoogste Gap (0,240), gedefinieerd als het verschil in cosinus-similariteit tussen de gegenereerde tekst en het ware toekomstige artikel versus niet-gerelateerde artikelen. Het presteerde aanzienlijk beter dan baselines in H@10 (50,8%) en H@100 (80,8%), wat aangeeft dat de gegenereerde claims veel waarschijnlijker het juiste toekomstige artikel uit de pool halen.
Voorspelling van Nieuwe Wiskundige Claims (NMCP): COMPOSE leidde in Precisie (0,560) en Match (0,730), wat aantoont dat de outputs overeenkomen met toekomstige stellingen op zowel formeel als informeel niveau, niet alleen thematisch.
LLM-Judge Evaluatie: Een LLM-judge (GPT-4.0) evalueerde outputs op Inhoud, Diepgang, Originaliteit, Precisie en Specificiteit. COMPOSE behaalde de hoogste totaalscore (3,36/5), met name in Technische Diepgang (3,52) en Specificiteit (3,52), en produceerde concretere en wiskundig rijkere outputs dan baselines die vaak vage samenvattingen genereerden.
Ablatie Studies: Het verwijderen van ofwel de wetenschappelijke ofwel de formele grafiek-encoder veroorzaakte significante prestatiedalingen, wat bevestigt dat beide modaliteiten complementaire signalen bieden. De formele grafiek was cruciaal voor gronding, terwijl de wetenschappelijke grafiek essentieel was voor het identificeren van de juiste onderzoeksrichting.

Betekenis en Claims

Het artikel beweert dat toekomstige wiskundige generatie profiteert van het combineren van wetenschappelijke context met formele structuur.

Gegronde Generatie: De auteurs tonen aan dat het uitsluitend vertrouwen op wetenschappelijke tekst leidt tot claims die thematisch relevant zijn maar logisch ongegronden, terwijl het uitsluitend vertrouwen op formele structuur het model beperkt tot bekende stellingen zonder nieuwe richtingen te anticiperen. COMPOSE slaagt erin deze kloof te overbruggen.
Data Bijdrage: De constructie van de 108K gekoppelde dataset en de 47K toekomstige artikel-benchmark biedt een nieuwe resource voor het evalueren van gegronde wiskundige generatie, en adresseert het gebrek aan tijdelijke benchmarks in dit veld.
Methodologische Vooruitgang: Het dubbel-grafiek kader met cross-attention fusie biedt een nieuwe aanpak voor het integreren van heterogene kennisbronnen (informele literatuur versus formele logica) voor generatieve taken.

De auteurs merken beperkingen op, specifiek dat de methode afhankelijk is van benaderende informeel-formele afstemming (wat ruis kan introduceren in gebieden met schaarse Mathlib-dekking) en dat gegenereerde claims niet worden geverifieerd door een bewijshulp, maar in plaats daarvan vertrouwen op retrieval en LLM-gebaseerde evaluatie als proxy-signalen. Zij suggereren dat toekomstig werk bewijs-bewuste verificatie kan incorporeren om de formele correctheid van gegenereerde claims direct te controleren.