Riepilogo Tecnico: COMPOSE – Comporre Teoremi Futuri da Citazioni e Struttura Formale

Definizione del Problema

Il documento affronta la sfida della generazione futura di matematica fondata: il compito di prevedere un'affermazione matematica futura plausibile (una dichiarazione simile a un teorema) per un dato articolo "ancora". Gli autori sostengono che una previsione valida deve soddisfare due vincoli simultanei:

1. Traiettoria Scientifica: Deve estendere la direzione di ricerca indicata dal grafo delle citazioni scientifiche e dall'evoluzione delle idee nella letteratura.
2. Fondamento Formale: Deve rispettare le dipendenze logiche intrinseche alla matematica formale, garantendo che l'affermazione sia validamente derivabile da definizioni, lemmi e teoremi esistenti.

Gli approcci esistenti modellano tipicamente solo una di queste fonti. I modelli addestrati esclusivamente su testo scientifico possono generare affermazioni fluide ma logicamente non fondate, mentre i sistemi di dimostrazione di teoremi ragionano su strutture formali ma mancano del contesto scientifico per identificare direzioni di ricerca promettenti. Il documento ipotizza che combinare queste fonti complementari non sia banale a causa delle differenze fondamentali nel modo in cui gli articoli scientifici e le librerie formali (come Mathlib) organizzano la conoscenza.

Metodologia: Il Framework COMPOSE

Gli autori propongono COMPOSE, un framework a doppio grafo che condiziona un modello linguistico sia sul contesto delle citazioni scientifiche sia sulla struttura dei teoremi formali. L'approccio consta di tre componenti principali:

1. Costruzione dei Dati

Gli autori hanno costruito un dataset di 108.000 esempi di grafi scientifici-formali accoppiati derivati da articoli di matematica su arXiv (2000–2023) e dalla libreria Lean Mathlib.

• Grafo Scientifico ($G_s$): Costruito a partire da un articolo ancora e dal suo contesto di citazione (fino a due salti). Include nodi astratti per gli articoli e nodi teorema estratti dal testo. Gli archi rappresentano i collegamenti di citazione e le dipendenze interne all'articolo.
• Grafo Formale ($G_f$): Costruito allineando i teoremi informali estratti ai corrispondenti teoremi in Mathlib. Questo allineamento utilizza FrenzyMath (un corpus di descrizioni informali scritte da umani per i teoremi Mathlib) per eseguire il recupero da informale a informale, evitando il rumore della formalizzazione automatica diretta. Il grafo formale si espande dal teorema radice corrispondente utilizzando archi di dipendenza estratti tramite LeanDojo.
• Benchmark: Un set di test temporaneamente tenuto da parte di 47.000 articoli futuri della fine del 2024 e del 2025, utilizzato per valutare la capacità del modello di prevedere risultati effettivamente pubblicati.

2. Architettura del Modello

COMPOSE impiega un'architettura a doppio encoder seguita da un decoder condizionato dal grafo:

• Doppi Encoder: Due Reti Neurali Grafiche (GNN) dedicate elaborano separatamente $G_s$ e $G_f$.
  • I nodi di $G_s$ sono inizializzati con embedding E5 (testo scientifico).
  • I nodi di $G_f$ sono inizializzati con embedding DeepSeek-Math (firme formali).
  • Entrambi utilizzano passaggio di messaggi diretti e specifici per tipo di arco con connessioni residue gateate.
• Modulo di Fusione: Le rappresentazioni da entrambi i grafi sono proiettate in uno spazio latente condiviso e fuse tramite un meccanismo di attenzione incrociata bidirezionale. Ciò permette al modello di integrare la direzione scientifica con i vincoli formali.
• Decoder: Un LLM specializzato in matematica preaddestrato (DeepSeek-Math-7B o Mistral-7B) adattato con LoRA. Sono inseriti strati di attenzione incrociata nel decoder per condizionare la generazione sugli embedding del grafo fusi, permettendo al modello di prestare attenzione all'intera struttura del grafo durante la generazione dei token.

3. Addestramento in Due Fasi

• Fase 1 (Apprendimento delle Rappresentazioni): Gli encoder del grafo e il modulo di fusione sono addestrati senza il decoder utilizzando tre obiettivi:
  • Previsione dei Collegamenti: Per garantire che gli encoder catturino la struttura del grafo.
  • Allineamento Contrastivo: Per allineare la rappresentazione del grafo fuso con l'abstract e l'affermazione principale dell'articolo target.
  • Allineamento Incrociato: Per allineare esplicitamente i nodi dei teoremi informali con le loro controparti formali corrispondenti.
• Fase 2 (Generazione): Il decoder viene aggiunto e fine-tunato utilizzando:
  • Perdita Autoregressiva: Previsione standard del token successivo.
  • Perdita di Margine del Grafo: Un termine di regolarizzazione che penalizza il modello se genera lo stesso testo per una coppia di grafi non corrispondenti, costringendolo a fare affidamento sul contesto specifico del grafo.

Risultati Chiave

Gli esperimenti sono stati condotti sul benchmark di 47K articoli futuri, confrontando COMPOSE con baselines robuste (inclusi GIANTS, FutureGen, GoAI e varie varianti solo testo o solo prompt).

• Prestazioni di Recupero: COMPOSE ha ottenuto il Gap più alto (0,240), definito come la differenza nella similarità coseno tra il testo generato e il vero articolo futuro rispetto ad articoli non correlati. Ha superato significativamente le baselines in H@10 (50,8%) e H@100 (80,8%), indicando che le sue affermazioni generate hanno molte più probabilità di recuperare l'articolo futuro corretto dal pool.
• Previsione di Affermazioni Matematiche Nuove (NMCP): COMPOSE ha guidato in Precisione (0,560) e Match (0,730), dimostrando che le sue uscite si allineano con i teoremi futuri sia a livello formale che informale, non solo a livello tematico.
• Valutazione tramite Giudice LLM: Un giudice LLM (GPT-4.0) ha valutato le uscite su Contenuto, Profondità, Novità, Precisione e Specificità. COMPOSE ha ottenuto il punteggio complessivo più alto (3,36/5), in particolare in Profondità Tecnica (3,52) e Specificità (3,52), producendo uscite più concrete e ricche matematicamente rispetto alle baselines che spesso generavano riassunti vaghi.
• Studi di Ablazione: La rimozione di uno qualsiasi degli encoder del grafo scientifico o formale ha causato cali significativi delle prestazioni, confermando che entrambe le modalità forniscono segnali complementari. Il grafo formale era cruciale per il fondamento, mentre il grafo scientifico era essenziale per identificare la corretta direzione di ricerca.

Significato e Affermazioni

Il documento afferma che la generazione futura di matematica trae beneficio dalla combinazione del contesto scientifico con la struttura formale.

• Generazione Fondata: Gli autori dimostrano che fare affidamento esclusivamente sul testo scientifico porta ad affermazioni tematicamente rilevanti ma logicamente non fondate, mentre fare affidamento esclusivamente sulla struttura formale limita il modello a teoremi noti senza anticipare nuove direzioni. COMPOSE colma con successo questo divario.
• Contributo ai Dati: La costruzione del dataset accoppiato da 108K elementi e del benchmark di 47K articoli futuri fornisce una nuova risorsa per valutare la generazione matematica fondata, affrontando la mancanza di benchmark temporali in questo campo.
• Avanzamento Metodologico: Il framework a doppio grafo con fusione tramite attenzione incrociata offre un approccio innovativo per integrare fonti di conoscenza eterogenee (letteratura informale vs. logica formale) per compiti generativi.

Gli autori notano le limitazioni, specificamente che il metodo si basa su un allineamento approssimativo informale-formale (che può introdurre rumore in aree con copertura scarsa di Mathlib) e che le affermazioni generate non sono verificate da un assistente di dimostrazione, affidandosi invece al recupero e alla valutazione basata su LLM come segnali proxy. Suggeriscono che un lavoro futuro potrebbe incorporare una verifica consapevole delle dimostrazioni per controllare direttamente la correttezza formale delle affermazioni generate.