FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

Il paper presenta FormalProofBench, un benchmark privato che valuta la capacità dei modelli AI di generare prove matematiche di livello universitario avanzato formalmente verificate in Lean 4, rivelando che i modelli più performanti raggiungono una precisione del 33,5%.

L'essenziale

🧠 Il Grande Esame di Matematica per le Intelligenze Artificiali

Immagina di dover insegnare a un robot come risolvere un problema di matematica. Fino a poco tempo fa, gli chiedevamo: "Ehi, qual è la soluzione?" e il robot rispondeva con un testo lungo e convincente. Ma c'era un problema: il robot poteva inventare cose, saltare passaggi logici o usare regole che non esistono, e noi umani (o altri robot) faticavamo a notare l'errore perché il testo sembrava giusto.

Gli autori di questo studio hanno pensato: "Basta con le chiacchiere. Facciamo un esame dove la risposta deve essere verificata da un computer infallibile."

Ecco come funziona il loro nuovo banco di prova, chiamato FormalProofBench.

1. La Sfida: Costruire un Ponte Perfetto 🌉

Immagina che la matematica sia la costruzione di un ponte.

• I vecchi test (come MATH): Chiedevano al robot di descrivere a parole come costruire il ponte. Se il robot diceva "ho usato cemento forte", anche se in realtà aveva usato sabbia, il test umano poteva accettarlo.
• FormalProofBench: Qui, il robot non può parlare. Deve scrivere il codice esatto per costruire il ponte usando un linguaggio speciale chiamato Lean 4. Questo linguaggio è come un architetto robotico che non tollera errori: se anche un solo mattone è messo male, il computer dice "NO, il ponte crollerà" e il test fallisce. Non ci sono "quasi giusti". O funziona, o non funziona.

2. Il Laboratorio: Un Robot con un Assistente 🛠️

Per risolvere questi problemi (che sono di livello universitario avanzato, tipo esami per laureati), i ricercatori non hanno lasciato i robot soli. Li hanno messi in una "gabbia" speciale con degli strumenti:

• Un dizionario magico (Lean Loogle): Per cercare le regole matematiche già esistenti.
• Un banco di prova (Lean Executor): Per provare a scrivere un pezzo di codice, vedere se funziona e, se c'è un errore, correggerlo subito.

I robot hanno a disposizione 40 tentativi (o "turni") per ogni problema. Possono cercare, provare, sbagliare, correggere e riprovare. È come se avessero 40 ore di laboratorio per risolvere un singolo esercizio.

3. Chi ha passato l'esame? 🏆

I ricercatori hanno messo alla prova i "super-robot" più potenti del mondo (come Claude, GPT-5, Gemini, ecc.).
Il risultato è stato sorprendente e un po' preoccupante:

• Il robot migliore, Claude Opus 4.5, è riuscito a risolvere correttamente solo il 33,5% dei problemi.
• Gli altri sono andati peggio, scendendo fino al 3% o 4%.

Cosa significa? Significa che anche i robot più intelligenti del 2026 faticano enormemente a fare matematica "seria" e verificabile. Sono bravissimi a scrivere saggi o a fare calcoli semplici, ma quando devono costruire una prova logica complessa che non ammette errori, si perdono facilmente.

4. Il Segreto del Successo: "Provare e Riprovare" 🔄

L'analisi più interessante riguarda come i robot hanno lavorato.

• I robot che fallivano: Passavano tutto il tempo a consultare il "dizionario magico" (cercando regole che non esistevano o che non servivano), come uno studente che legge tutto il libro di testo senza mai fare un esercizio.
• I robot che vincevano: Usavano il "banco di prova". Scrivevano un pezzo di codice, vedevano l'errore, lo correggevano e riprovavano. Più volte provavano a eseguire il codice, più avevano successo.
  • Metafora: È la differenza tra chi studia la teoria della guida in auto e chi sale in auto, prova a sterzare, sbatte contro il muro, impara e riprova.

5. Perché è importante? 🚀

Questo studio ci dice due cose fondamentali:

1. Siamo ancora lontani: Le Intelligenze Artificiali non sono ancora pronte a sostituire i matematici umani per la ricerca avanzata. C'è ancora un "muro" logico da abbattere.
2. Il futuro è promettente: Anche se il 33% sembra poco, è un enorme passo avanti rispetto al passato. Se continuiamo a migliorare, presto potremo avere assistenti che non solo scrivono formule, ma le verificano istantaneamente, accelerando la scoperta scientifica.

In sintesi

FormalProofBench è come un esame di guida per le IA, ma invece di guidare un'auto, devono guidare la logica matematica. Finora, solo un pilota su tre è riuscito a parcheggiare senza graffiare l'auto, e quelli che ci sono riusciti sono stati quelli che hanno avuto il coraggio di fare molti tentativi pratici, non solo quelli che hanno letto il manuale.

Sommario tecnico

Titolo: FormalProofBench: I modelli possono scrivere prove matematiche di livello universitario che sono formalmente verificate?

1. Il Problema e il Contesto

Nonostante i significativi progressi dei Large Language Models (LLM) nel ragionamento matematico su benchmark informali (come MATH o AIME), esiste un divario critico tra la capacità di generare argomentazioni plausibili in linguaggio naturale e quella di produrre dimostrazioni matematiche rigorose e verificabili.

• Limiti dei benchmark attuali: Le soluzioni in linguaggio naturale possono nascondere errori logici sottili, omissioni di casi critici o invocazioni di lemmi inesistenti, errori che spesso sfuggono anche a valutatori umani o basati su LLM.
• La necessità di verifica formale: La comunità matematica sta adottando sempre più i dimostratori di teoremi interattivi (come Lean 4 e la sua libreria Mathlib). Tuttavia, mancano benchmark rigorosi che valutino se i modelli AI possano generare prove che superino il controllo del kernel di Lean (type-checking), garantendo che la dimostrazione sia matematicamente corretta e non solo semanticamente plausibile.

2. Metodologia: FormalProofBench

Il paper introduce FormalProofBench, un benchmark privato progettato per valutare le capacità di dimostrazione di teoremi formali a livello avanzato (triennio universitario e dottorato).

• Struttura del Task: Ogni compito presenta una coppia composta da:
  1. Una dichiarazione del problema in linguaggio naturale.
  2. La corrispondente dichiarazione formale in Lean 4.
     Il modello deve generare un termine di prova (proof term) in Lean che venga accettato dal kernel di Lean 4.
• Dataset:
  • Volume: 200 problemi selezionati da esami di qualificazione e testi universitari standard.
  • Dominii: Analisi reale e funzionale, teoria della misura, algebra, geometria algebrica, teoria dei numeri, probabilità, logica e teoria dei modelli.
  • Qualità: I problemi sono stati formalizzati da esperti (dottorandi e specialisti di Lean) e sottoposti a una revisione secondaria umana per evitare errori di formalizzazione (misformalization).
• Ambiente di Valutazione (Agentic Harness):
  • I modelli non generano la prova in un singolo passaggio (forward pass), ma operano in un ciclo di agenti con un massimo di 40 turni per problema.
  • Strumenti a disposizione:
    • lean_loogle: Per cercare teoremi e definizioni in Mathlib.
    • lean_run_code: Per eseguire codice Lean, ottenere feedback sugli errori, sui goal irrisolti e sui mismatch di tipo.
    • submit_proof: Per inviare la prova finale.
  • Criterio di Successo: Binario e automatizzato. Una prova è corretta solo se compila con successo nel kernel Lean 4 (nessun "sorry", nessun assioma locale).

3. Contributi Chiave

1. Nuovo Benchmark Deterministico: Presentazione di un benchmark non contaminato (i dati sono privati per prevenire l'inquinamento dei dati di training), realistico e con valutazione deterministica basata sul compilatore Lean.
2. Valutazione di Livello Graduate: Analisi dettagliata di modelli frontier su problemi di livello universitario avanzato, un passo oltre i benchmark olimpici o di scuola superiore.
3. Analisi Agente e Costi: Valutazione delle prestazioni in un ambiente multi-turno con accesso a strumenti di ricerca ed esecuzione codice, includendo analisi di latenza e costi computazionali.
4. Analisi dei Modelli di Utilizzo degli Strumenti: Identificazione di pattern comportamentali critici tra modelli di successo e fallimento.

4. Risultati Sperimentali

I risultati mostrano che, sebbene ci siano progressi, la capacità di dimostrare teoremi formali complessi rimane una sfida significativa per i modelli attuali.

• Prestazioni Generali:
  • Il modello migliore, Claude Opus 4.5 (Thinking), ha raggiunto un'accuratezza del 33,5%.
  • C'è un calo rapido delle prestazioni per i modelli successivi: Gemini 3 Pro (18,5%), Claude Sonnet 4.5 (18,0%), GPT 5 (17,0%).
  • I modelli open-source o meno avanzati (es. DeepSeek V3.2, Grok) hanno mostrato prestazioni inferiori al 10%.
• Analisi dell'Utilizzo degli Strumenti (Tool-Use):
  • Correlazione con l'Esecuzione Codice: I modelli di successo tendono a utilizzare frequentemente lean_run_code per iterare rapidamente sulla soluzione, ottenendo feedback immediati dagli errori di compilazione.
  • Trappola della Ricerca: Un fallimento comune è l'eccessivo uso di lean_loogle (ricerca) senza esecuzione di codice, portando i modelli a cercare lemmi inesistenti o a "spirale" di ricerca senza progresso.
  • Ottimizzazione: I modelli migliori usano la ricerca solo per colmare lacune specifiche dopo aver tentato di costruire la prova, mentre i modelli meno performanti si affidano ciecamente alla ricerca.
• Costi e Latenza:
  • La latenza media per test è elevata (spesso oltre un'ora per modello, inclusi i tentativi di iterazione).
  • Il costo per test varia da circa 10 centesimi a oltre 1 dollaro, a seconda del modello e del numero di token utilizzati.

5. Significato e Implicazioni

• Bottleneck della Formalizzazione: Il paper evidenzia che, sebbene l'AI stia migliorando, la formalizzazione matematica rimane un collo di bottiglia. La capacità di tradurre idee matematiche in sintassi formale corretta è ancora un ostacolo maggiore della logica stessa.
• Verso l'Assistente Matematico: Il rapido miglioramento osservato suggerisce che stiamo avvicinandoci a una soglia in cui i sistemi AI potrebbero diventare strumenti pratici per i matematici, accelerando la formalizzazione della ricerca e democratizzando l'accesso ai metodi formali.
• Direzioni Future: Il lavoro suggerisce l'esplorazione di configurazioni di strumenti alternative (es. ricerca semantica, grep su codice locale), l'ablazione delle dichiarazioni in linguaggio naturale per testare la capacità di traduzione, e l'espansione verso teoremi di ricerca pura man mano che Mathlib cresce.

In sintesi, FormalProofBench stabilisce un nuovo standard per la valutazione dell'IA matematica, spostando il focus dalla "plausibilità" alla "verificabilità formale", e dimostra che, sebbene i modelli migliori stiano iniziando a superare la soglia del 30% di successo, c'è ancora molta strada da fare per raggiungere l'affidabilità necessaria per l'uso nella ricerca matematica avanzata.