Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Questo articolo introduce il Ciclo Congettura-Dimostrazione (CPL), una pipeline che sfrutta l'apprendimento in contesto alimentando iterativamente un LLM con le proprie teoremi e dimostrazioni formalmente verificate in Lean 4 per migliorare significativamente il tasso di scoperta e il successo di congetture matematiche nuove e difficili da dimostrare.

L'essenziale

Immagina di dover insegnare a un robot molto intelligente, ma leggermente distratto, come risolvere enigmi matematici complessi. Il robot è un Modello Linguistico di Grande Dimensione (LLM), e gli enigmi sono dimostrazioni matematiche formali scritte in un linguaggio informatico rigoroso chiamato Lean.

Il documento introduce un nuovo modo per insegnare a questo robot, chiamato Ciclo Congettura-Dimostrazione (CPL). Ecco come funziona, spiegato attraverso semplici analogie:

Il Problema: La Trappola del "Indovina-e-Verifica"

Di solito, quando le persone cercano di far fare matematica all'IA, gli chiedono di indovinare un enigma e risolverlo tutto in una volta.

• L'Analogia: Immagina di chiedere a uno studente di "Scrivi un problema di matematica e risolvelo immediatamente".
• Il Problema: Lo studente diventa pigro. Scrive problemi facili (come "2 + 2 = 4") perché sono semplici da risolvere. Evita i problemi difficili perché sa che potrebbero fallire. L'IA finisce per generare migliaia di dimostrazioni facili e noiose, perdendosi quelle difficili e interessanti.

La Soluzione: La "Danza in Due Passi" (CPL)

Gli autori dividono il processo in due ruoli distinti: un Congetturatore (il Generatore di Idee) e un Dimostratore (il Risolutore).

1. Il Congetturatore (L'Architetto): Questa parte dell'IA esamina una libreria di regole matematiche esistenti e formula nuove idee (congetture). Non cerca ancora di risolverle; le scrive semplicemente.
2. Il Dimostratore (Il Costruttore): Questa parte prende le idee e cerca di costruire una dimostrazione per esse. Se fallisce, riprova. Continua a tentare fino a quando non riesce o non esaurisce i tentativi.
3. La Libreria (La Memoria): Ogni volta che il Dimostratore costruisce con successo una dimostrazione, questa viene aggiunta alla libreria.

L'Ingrediente Magico: Apprendimento in Contesto
Ecco la parte astuta: il Dimostratore non guarda solo le regole matematiche originali. Guarda la libreria di dimostrazioni che ha già costruito con successo durante la sessione corrente.

• L'Analogia: Immagina uno studente che sostiene un esame. Nel vecchio metodo, doveva affidarsi solo a ciò che aveva memorizzato prima dell'inizio dell'esame. In questo nuovo metodo, ogni volta che lo studente risolve correttamente un problema, gli è permesso leggere la propria soluzione prima di affrontare il problema successivo. Impara i "trucchi" e le "strategie" dai propri recenti successi.

Cosa Hanno Trovato

I ricercatori hanno testato questo approccio su alcuni concetti topologici ostici (un ramo della matematica che tratta forme e spazi) che l'IA non conosceva ancora bene.

• Quantità vs Qualità: Il vecchio metodo (indovinare e risolvere in una volta) ha generato più teoremi in totale, ma erano per lo più brevi e facili. Il nuovo metodo (CPL) ha generato meno teoremi in totale, ma erano molto più difficili e lunghi.
• Il Grande Vantaggio: Il nuovo metodo ha scoperto con successo un teorema specifico e difficile sugli "insiemi alfa-aperti" che il vecchio metodo non ha mai trovato, nemmeno dopo 20 tentativi.
• Imparare dal Successo: Quando all'IA è stata fornita la libreria delle sue precedenti dimostrazioni come "foglio di appunti" (contesto), è riuscita a dimostrare teoremi difficili che non avrebbe potuto risolvere senza quel contesto. Anche quando l'IA non è riuscita a dimostrare il teorema in inglese semplice, è riuscita a dimostrarlo nel codice Lean una volta aver visto dimostrazioni di successo simili.

Il Conclusione

Il documento afferma che separando la "generazione di idee" dalla "risoluzione delle dimostrazioni" e permettendo all'IA di imparare dai propri successi verificati in tempo reale, possiamo portarla a scoprire verità matematiche più difficili e complesse che altrimenti mancherebbe. È come dare all'IA una partenza avvantaggiata permettendole di studiare i propri compiti prima di sostenere l'esame finale.

Nota: Il documento si concentra rigorosamente su questo metodo per generare e verificare teoremi matematici. Non afferma che questo metodo funzioni per diagnosi mediche, previsioni finanziarie o altre applicazioni del mondo reale al di fuori della matematica formale.

Sommario tecnico

Riepilogo Tecnico: Scoperta di Nuovi Teoremi tramite LLM con Apprendimento della Dimostrazione in Contesto in Lean

Enunciato del Problema
I Modelli Linguistici di Grande Dimensione (LLM) hanno mostrato promesse nella dimostrazione formale di teoremi, ma affrontano sfide significative: possono allucinare e la generazione simultanea di una congettura matematica e della sua dimostrazione spesso porta a una convergenza su teoremi banali o semplici. Gli approcci esistenti si basano tipicamente sul Fine-Tuning Supervisionato (SFT) o sull'Apprendimento per Rinforzo con Ricompense Verificate (RLVR), che richiedono dati di addestramento estesi e sono difficili da applicare a modelli closed-source. Inoltre, i metodi attuali spesso faticano a scoprire teoremi "difficili da dimostrare" perché la probabilità di generare un teorema è fortemente pesata dal tasso di successo immediato nella sua dimostrazione, causando il collasso della ricerca in dimostrazioni semplici e brevi.

Metodologia: Il Ciclo Congettura-Dimostrazione (CPL)
Gli autori propongono il Ciclo Congettura-Dimostrazione (CPL), una pipeline progettata per generare automaticamente congetture matematiche e verificarle in Lean 4. Il framework separa la generazione delle congetture dalla generazione delle dimostrazioni, utilizzando una libreria di teoremi precedentemente verificati come contesto per entrambe le fasi.

La pipeline opera attraverso quattro componenti principali: un Congetturatore (agente LLM), un Dimostratore (agente LLM), un Server Lean e una Libreria (dati di codice Lean).

1. Fase di Congettura: Il Congetturatore genera nuovi enunciati matematici in formato Lean 4 basati sulla libreria corrente. Interroga il Server Lean per garantire la validità sintattica e la novità (verificando che l'enunciato non sia già dimostrabile dai teoremi esistenti in Mathlib4 o nella libreria corrente).
2. Fase di Dimostrazione: Per ogni congettura valida, il Dimostratore tenta di costruire una dimostrazione formale. Crucialmente, al Dimostratore viene fornita la libreria (contenente teoremi e dimostrazioni precedentemente verificati) come contesto. Ciò permette all'LLM di apprendere strategie di dimostrazione tramite apprendimento in contesto senza riaddestramento del modello. Il Dimostratore itera fino a un numero massimo di tentativi (impostato a 16 negli esperimenti), utilizzando i messaggi di errore dal Server Lean per affinare i suoi tentativi.
3. Iterazione: Le coppie verificate di congetture e dimostrazioni vengono aggiunte alla libreria, che funge quindi da contesto per le iterazioni successive.

Questa separazione permette al sistema di allocare le risorse di ricerca in base alla difficoltà della dimostrazione. A differenza di un ciclo semplice (SL) in cui un enunciato e una dimostrazione sono generati simultaneamente, il CPL tenta più dimostrazioni per un singolo enunciato prima di scartarlo. Ciò sposta la distribuzione dei teoremi generati verso quelli dimostrabili ma difficili, piuttosto che verso quelli meramente facili da dimostrare.

Contributi Chiave

1. Proposta di Pipeline: L'introduzione del CPL, un framework che disaccoppia la generazione delle congetture dalla generazione delle dimostrazioni, permettendo la scoperta di dimostrazioni più lunghe e complesse.
2. Apprendimento in Contesto per Modelli Closed-Source: La dimostrazione che gli LLM closed-source (in particolare ChatGPT-o3) possono migliorare le loro capacità dimostrative attraverso l'apprendimento in contesto dai loro stessi output precedentemente verificati, eliminando la necessità di aggiornamenti dei parametri o fine-tuning.
3. Validazione Teorica ed Empirica: Il paper fornisce un modello teorico che mostra come il CPL aumenti la probabilità di generare teoremi difficili da dimostrare rispetto ai framework di generazione simultanea. Sperimentalmente, verifica che il CPL ha riscoperto con successo un teorema specifico di livello di ricerca che il framework di base non è riuscito a trovare.

Risultati Sperimentali
Gli autori hanno valutato il CPL rispetto a una baseline di Ciclo Semplice (SL) utilizzando nozioni topologiche (semi-apertura, $\alpha$-apertura e pre-apertura) definite all'interno di Mathlib ma non ancora incluse nella libreria. L'obiettivo era il teorema che afferma che l'intersezione di due insiemi $\alpha$-aperti è $\alpha$-aperta.

• Tasso di Scoperta: In 20 esecuzioni sperimentali, il CPL ha scoperto il teorema target 5 volte. Al contrario, il framework SL, che ha generato significativamente più teoremi in media (328 contro 106), non è riuscito a generare il teorema target nemmeno una volta. Il test esatto di Fisher ha confermato che questa differenza è statisticamente significativa ($p = 0.024$).
• Lunghezza della Dimostrazione: Il CPL ha generato teoremi con lunghezze di dimostrazione significativamente maggiori (in numero di caratteri) rispetto a SL, supportando l'affermazione teorica che il framework sposta il focus verso dimostrazioni più difficili.
• Efficacia del Contesto:
  • Ridimostrazione: Quando si ridimostrano i teoremi generati, fornire la libreria come contesto ha aumentato il tasso di successo dal 91% al 99% ($p = 4 \times 10^{-35}$).
  • Teorema Target: Quando si è tentato di ridimostrare il teorema target sull'intersezione $\alpha$-aperta, il dimostratore è riuscito 7 volte su 80 tentativi quando gli è stata fornita la libreria generata come contesto. Senza la libreria, ha fallito il 100% delle volte.
  • Baseline in Linguaggio Naturale: Quando è stato chiesto di dimostrare il teorema in linguaggio naturale, ChatGPT-4o ha spesso giudicato il teorema falso o fornito dimostrazioni errate, e ChatGPT-o3 lo ha costantemente giudicato falso, indicando che il teorema era al di fuori delle conoscenze pre-addestrate dei modelli. Il successo in Lean 4 è stato attribuito all'apprendimento in contesto delle strategie dimostrative dalla libreria generata.

Significato e Affermazioni
Il paper afferma che il CPL affronta efficacemente la limitazione degli LLM nella scoperta di teoremi non banali sfruttando l'apprendimento in contesto da dimostrazioni verificate auto-generate. Gli autori sottolineano che questo approccio permette l'espansione automatica di librerie di matematica formale (come Mathlib) generando proposizioni su nozioni date che potrebbero non essere esplicitamente note all'LLM. Il lavoro suggerisce che separare le fasi di congettura e dimostrazione, combinata con l'arricchimento iterativo del contesto, è una strategia praticabile per la dimostrazione di teoremi neurale, in particolare per modelli closed-source dove i metodi di addestramento tradizionali non sono applicabili. Gli autori mantengono una posizione modesta, notando che, sebbene il framework abbia riscoperto con successo un teorema noto di livello di ricerca, sono necessari lavori futuri per affinare il processo di generazione per enunciati matematici più profondi e illuminanti.