SorryDB: Can AI Provers Complete Real-World Lean Theorems?

Il paper presenta SorryDB, un benchmark dinamico di 1000 compiti reali in Lean estratti da progetti GitHub, dimostrando che gli approcci attuali (modelli linguistici, agenti e provatori simbolici) sono complementari e che un approccio basato su agenti con Gemini Flash, sebbene il più performante, non supera sistematicamente gli altri metodi.

L'essenziale

Immagina di dover costruire una cattedrale gigantesca, pietra dopo pietra. Ogni mattoncino è una dimostrazione matematica. Per secoli, i matematici hanno scritto queste dimostrazioni su carta, ma oggi stanno usando un "architetto digitale" chiamato Lean per costruire questa cattedrale in modo che un computer possa verificare che ogni singolo mattone sia perfetto.

Il problema? La cattedrale è così grande che nessuno riesce a finire tutto. Ci sono ancora centinaia di buchi nei muri, spazi vuoti dove i matematici hanno scritto: "Ehi, qui manca la dimostrazione, la farò più tardi". In gergo tecnico, questi spazi vuoti si chiamano "sorry" (che in inglese significa "scusa", come a dire: "Scusa, non l'ho ancora fatto").

Ecco dove entra in gioco questo articolo scientifico, che presenta SorryDB.

1. Il Problema: I Giochi da Tavolo vs. La Vita Reale

Fino a poco tempo fa, per vedere se un'intelligenza artificiale (AI) fosse brava a fare matematica, le si facevano risolvere problemi da olimpiadi (tipo i Giochi della Gioventù Matematica).

• L'analogia: È come allenare un calciatore facendogli fare solo esercizi di tiro in porta in un campo vuoto, senza avversari, senza vento e senza pubblico.
• La realtà: Nella vita reale, un matematico non deve solo tirare in porta. Deve capire il vento, vedere dove sono gli altri giocatori, usare le regole specifiche del suo team e risolvere problemi che nessuno ha mai visto prima. I vecchi test (come miniF2F o PutnamBench) erano diventati "saturi": le AI le avevano già imparate a memoria, quindi non dicevano più quanto fossero davvero intelligenti.

2. La Soluzione: SorryDB (Il "Cantiere Aperto")

Gli autori hanno creato SorryDB, un nuovo banco di prova. Invece di usare vecchi problemi da libro di testo, hanno guardato direttamente su GitHub (il sito dove gli sviluppatori salvano il codice) a 78 progetti reali di matematica che sono ancora in costruzione.

Hanno raccolto tutti i "sorry", ovvero tutti i buchi lasciati aperti dai matematici umani.

• L'analogia: Invece di dare all'AI un puzzle già stampato su un foglio, gli hanno detto: "Ecco il cantiere della cattedrale. Ecco 1000 buchi nei muri che i muratori umani hanno lasciato aperti. Tu prova a riempirli usando i mattoni che abbiamo già in magazzino."

Questo è geniale perché:

1. È sempre nuovo: Appena un matematico umano riempie un buco, ne crea un altro. Il test si aggiorna da solo.
2. È difficile: Non sono solo esercizi di scuola, ma problemi complessi che dipendono da migliaia di altre regole scritte da altri.
3. È onesto: Nessuna AI ha mai visto questi problemi specifici prima, quindi non può barare imparate a memoria.

3. La Gara: Chi è il Migliore?

Hanno messo alla prova diverse "AI matematiche" su questi 1000 buchi.

• I "Semplici": Programmi vecchi che usano regole fisse (come un calcolatore).
• I "Cervelloni": Modelli linguistici enormi (come GPT, Claude, Gemini) che parlano fluentemente ma non sono specializzati.
• Gli "Esperti": AI addestrate specificamente per la matematica.
• Gli "Agenti": AI che non si limitano a rispondere, ma agiscono: provano una soluzione, se sbaglia, leggono l'errore, pensano di nuovo e riprovano.

Cosa è successo?

• Nessuno ha vinto da solo: Anche il modello più potente (Gemini Flash) non è riuscito a risolvere tutto.
• L'errore è il migliore insegnante: Le AI che potevano "ripensarci" (gli agenti che provavano, sbagliavano, leggevano l'errore e riprovavano) sono andate molto meglio di quelle che davano una sola risposta al volo. È come se avessero detto: "Ops, questo mattone non entra, proviamo a tagliarlo diversamente".
• Ognuno ha i suoi punti di forza: Un'AI era brava a risolvere i buchi nei progetti di scuola, un'altra nei progetti di ricerca avanzata. Se le metti insieme, riescono a risolvere il 35% dei buchi. Da sole, nessuna arriva al 100%.

4. La Morale della Favola

Il messaggio principale è che l'AI non è ancora un "super-matematico" che risolve tutto da sola.
Tuttavia, se usata come un assistente intelligente che può provare, sbagliare, correggersi e imparare dagli errori in tempo reale, diventa uno strumento potentissimo per aiutare i matematici umani a finire la cattedrale.

In sintesi:

• SorryDB è come un cantiere edile in tempo reale, non un libro di esercizi.
• Le AI attuali sono come operai molto veloci ma a volte distratti: hanno bisogno di qualcuno che controlli il lavoro e dica "Riprova, qui non va bene".
• Il futuro non è un'AI che sostituisce il matematico, ma un'AI che lavora con il matematico, riempiendo i buchi "scusa" uno alla volta, fino a completare la cattedrale.

Sommario tecnico

Titolo: SORRYDB: Possono i provatori AI completare teoremi Lean del mondo reale?

1. Il Problema

Il campo della dimostrazione automatica di teoremi (ATP) si è concentrato storicamente su dataset competitivi statici (come IMO, PutnamBench o miniF2F). Tuttavia, questi benchmark presentano diverse limitazioni critiche per lo sviluppo di strumenti pratici:

• Saturazione e Contaminazione: Molti di questi dataset sono saturi; le soluzioni potrebbero essere state memorizzate dai modelli durante l'addestramento, rendendo difficile distinguere tra ragionamento generale e semplice richiamo.
• Disallineamento con la Realtà: I problemi competitivi mancano del contesto reale dei progetti di formalizzazione, come le dipendenze da definizioni specifiche del progetto, la gestione di un codice base condiviso e la necessità di integrare soluzioni in un ecosistema complesso.
• Mancanza di Dinamicità: I benchmark statici non riflettono l'evoluzione continua della matematica formale e non misurano la capacità di un agente di contribuire a progetti nuovi e in sviluppo.

2. Metodologia: Il Dataset SorryDB

Gli autori introducono SorryDB, un benchmark dinamico e in continua evoluzione estratto da progetti reali su GitHub.

• Fonte dei Dati: Il dataset è costruito estraendo le istanze della parola chiave sorry (un segnaposto per una dimostrazione mancante) da 78 repository GitHub attivi e mantenuti, registrati nel "Reservoir" (il registro dei pacchetti Lean).
• Criteri di Selezione: Vengono inclusi solo progetti con licenze OSI approvate, aggiornati negli ultimi tre mesi, che coprono diverse categorie: pedagogico, strumentazione, benchmark, librerie e progetti di formalizzazione di teoremi specifici (es. Teorema di Fermat, Teorema di Carleson).
• Definizione del Task: Il compito è "fill-in-the-sorry": fornire il codice Lean necessario per sostituire un sorry specifico in un teorema esistente, completando l'obbligo di prova senza necessariamente dimostrare l'intero teorema se contiene più sorry.
• Pipeline di Validazione:
  1. Estrazione: Identificazione dei sorry sui rami principali e di lavoro.
  2. Filtraggio: Rimozione dei duplicati e selezione delle istanze più recenti.
  3. Verifica: Un pipeline automatizzata clona il repository, sostituisce il sorry con la soluzione proposta e verifica che il progetto compili con successo e che il sorry sia stato effettivamente rimosso (non solo sostituito da un altro placeholder). Questo evita la necessità di etichette curate manuali.

3. Contributi Chiave

1. Dataset SorryDB: Un dataset dinamico che allinea i benchmark alle esigenze pratiche della comunità di formalizzazione, mitigando il rischio di contaminazione dei dati di test.
2. Framework di Benchmarking: Un meccanismo di validazione automatizzata che permette di valutare l'accuratezza delle soluzioni in un ambiente di sviluppo reale.
3. Valutazione Comparativa: Un'analisi su uno snapshot statico di 1000 task (cutoff gennaio 2026) che confronta diversi approcci: tactic deterministiche, LLM generici, modelli specializzati e approcci agenziali.

4. Risultati Sperimentali

Sull'insieme di 1000 task, sono stati valutati diversi approcci:

• Approcci Deterministici (Tactic): Tactic come trivial, ring, linarith e grind hanno risolto una piccola percentuale di task (circa l'8,4% per TACTICS in totale), dimostrando efficacia solo su problemi semplici o ben strutturati.
• LLM Generici (Pass@1 vs Pass@32):
  • I modelli generici (GPT-5.2, Claude Opus 4.5, Gemini Flash 3, Qwen 3) mostrano prestazioni moderate in un singolo tentativo (Pass@1: 5-11%).
  • La performance migliora significativamente con il campionamento multiplo (Pass@32), raggiungendo il 20,5% per Gemini Flash 3.
• Modelli Specializzati: Modelli come Kimina Prover e Goedel Prover V2, addestrati su matematica competitiva, hanno ottenuto risultati inferiori rispetto agli LLM generici su questo dataset (es. Goedel Prover V2: 2,7% Pass@1). Questo suggerisce una difficoltà nel generalizzare a contesti non competitivi e una possibile incompatibilità con le versioni recenti di Lean.
• Approcci Iterativi e Agenziali (Il risultato principale):
  • Gli approcci che utilizzano feedback iterativo (Self-Correcting e Agentic) hanno superato di gran lunga tutti gli altri metodi.
  • Gemini Flash 3 (Agentic) ha raggiunto il 30,3% di successo.
  • Gemini Flash 3 (Self-Correcting) ha raggiunto il 27,9%.
  • Claude Opus 4.5 (Self-Correcting) ha raggiunto il 27,1%.
  • Conclusione: L'accesso all'ambiente di compilazione e il feedback sugli errori di build sono fattori dominanti per la performance, molto più importanti di un budget di ragionamento esteso o del fine-tuning su dataset specifici.
• Complementarità: Nessun singolo modello risolve tutti i problemi. La combinazione di tutti i provatori ha risolto il 35,7% dei task, dimostrando che diversi approcci sono complementari e risolvono sottoinsiemi diversi di problemi.

5. Significato e Implicazioni

• Validità Pratica: SorryDB dimostra che i benchmark basati su progetti reali sono essenziali per valutare l'utilità pratica degli strumenti ATP. I modelli specializzati su olimpiadi matematiche faticano a generalizzare a progetti di formalizzazione complessi e "sporchi".
• Importanza del Feedback: L'iterazione basata sugli errori di compilazione è cruciale. Gli agenti che possono provare, fallire, leggere l'errore e correggere il codice sono significativamente più efficaci dei modelli "one-shot".
• Benchmark Evolutivo: A differenza dei dataset statici, SorryDB è progettato per evolvere. Man mano che gli strumenti migliorano e risolvono i sorry attuali, i nuovi task rimasti diventeranno intrinsecamente più difficili, mantenendo il benchmark rilevante e non saturabile.
• Sfide Future: Il lavoro evidenzia la necessità di migliorare la capacità dei modelli di navigare nelle librerie esistenti (Mathlib) e di gestire il contesto locale dei progetti, oltre a gestire le differenze di versione di Lean.

In sintesi, il paper stabilisce che per avanzare nell'AI per la dimostrazione di teoremi, è necessario spostare l'attenzione dai problemi isolati e competitivi a task integrati in flussi di lavoro reali, dove l'interazione iterativa con l'ambiente di sviluppo è la chiave del successo.