🤖 AI

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

Questo articolo sostiene che la riuscita autoformalizzazione debba essere valutata tramite la revisione esperta della qualità delle definizioni e del design delle API piuttosto che meramente attraverso l'assenza di lacune non dimostrate ("sorries"), dimostrando, attraverso un caso di studio sul teorema di vanishing di Grothendieck, che mentre gli agenti IA possono applicare efficacemente correzioni meccaniche locali, essi faticano con il design concettuale di alto livello.

Autori originali: Vasily Ilin, Brian Nugent

Pubblicato 2026-06-15

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Vasily Ilin, Brian Nugent

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di assumere un apprendista molto veloce e molto desideroso di imparare per costruire una casa per te. Gli dai i progetti (un teorema matematico) e un capitolo di un libro di testo che spiega come costruirla.

L'apprendista lavora giorno e notte. Posano i mattoni, montano le pareti e installano il tetto. Quando hanno finito, la casa sta in piedi perfettamente. Non crolla. L'ispettore (il computer) dice: "Ottimo lavoro! La struttura è solida."

Questo articolo parla di ciò che accade dopo.

Gli autori di questo articolo si sono chiesti: "Solo perché la casa sta in piedi, è davvero una buona casa? Qualcun altro può viverci? Possono aggiungere facilmente un secondo piano in seguito, o dovranno prima abbattere le pareti?"

Ecco la scomposizione del loro esperimento, utilizzando analogie semplici:

L'Esperimento: Costruire una "Casa Matematica"

Il team ha chiesto a un'IA (un grande modello linguistico) di formalizzare un teorema matematico complesso chiamato Teorema di Vanishing di Grothendieck. Immaginate questo teorema come una sfida architettonica molto specifica e di alto livello.

Hanno dato all'IA:

L'obiettivo (l'enunciato del teorema).
Una dimostrazione da un libro di testo (le istruzioni).
Una regola: "Devi usare solo gli strumenti esistenti e standard che abbiamo già nella nostra cassetta degli attrezzi (la libreria matematica)."

Fase 1: Il "Pass" (Stato A)
L'IA ha lavorato duramente e ha prodotto codice che compilava senza errori. Nel mondo del software matematico, gli errori vengono chiamati "sorries" (abbreviazione di "sorry, I couldn't prove this yet" – scusa, non posso ancora dimostrare questo). L'IA è riuscita a ridurre il conteggio dei "sorry" a zero.

Il Risultato: La casa è in piedi. Il computer è felice.
Il Problema: Un esperto architetto umano (un matematico) ha guardato la casa e ha detto: "Questo è un disastro."

La Revisione dell'Esperto: Perché la "Casa in Piedi" è Fallita

L'esperto umano ha scoperto che, sebbene la casa non fosse crollata, era stata costruita malissimo. Ecco i problemi specifici che ha riscontrato, tradotti in termini quotidiani:

1. Il Problema degli "Strumenti Personalizzati" (Definizioni)

Cosa ha fatto l'IA: L'IA continuava a inventare i propri strumenti personalizzati per ogni singola piccola mansione. Se aveva bisogno di misurare una parete, costruiva un nuovo, strano metro solo per quella parete.
Perché è male: In una vera libreria, vuoi strumenti standard che tutti sappiano usare. Se l'IA costruisce uno strumento personalizzato per ogni lavoro, i futuri costruttori non potranno usare la casa perché non sanno come operare le strane invenzioni dell'IA.
Il Verdetto: L'IA è stata bravissima a usare gli strumenti, ma terribile nel progettarli. Ha creato 62 definizioni personalizzate, e 61 di queste erano inutili o confuse.

2. Il Problema del "Progetto Disordinato" (Design delle API)

Cosa ha fatto l'IA: L'IA non ha costruito un'interfaccia pulita (un manuale d'uso). Invece, ha continuato ad aprire le pareti per mostrare i mattoni grezzi ogni volta che qualcuno voleva fare qualcosa.
La Soluzione: L'esperto ha chiesto all'IA di costruire un'Interfaccia Utente (un'API) in modo che le persone potessero interagire con la matematica senza vedere le viscere disordinate.
Il Risultato: L'IA ha costruito un'interfaccia, ma era disordinata. Ha aggiunto 24 "regole" specifiche solo per la dimostrazione corrente, invece di creare alcune regole eleganti e generali. Era come aggiungere un interruttore unico e complicato per ogni singola lampadina della casa, invece di installare un interruttore standard.

3. Il Problema della "Visione a Breve Termine" (Enunciati dei Teoremi)

Cosa ha fatto l'IA: L'IA ha dimostrato esattamente ciò di cui aveva bisogno per completare il lavoro, e nient'altro. È stato come un carpentiere che taglia una tavola per adattarla solo all'attuale spazio vuoto, invece di tagliarla in modo che possa essere usata per altri spazi in seguito.
Il Verdetto: L'IA è eccellente nel risolvere l'enigma immediato, ma è terribile nel pensare: "Come posso rendere questo utile per qualcun altro tra cinque anni?"

Il Test "Prima e Dopo"

Il team non si è arreso. Hanno preso il feedback dell'esperto e hanno chiesto all'IA di sistemare le cose.

Cosa l'IA ha riparato bene: È stata brava nelle riparazioni locali. Se l'esperto diceva: "Rinomina questo file" o "Cambia questo numero specifico", l'IA lo faceva perfettamente. Poteva pulire il disordine.
Cosa l'IA non è riuscita a riparare: Non riusciva ancora a capire come progettare una buona casa da zero. Anche dopo la revisione, le definizioni erano ancora macchinose e l'interfaccia utente era ancora ingombrante.

La Grande Lezione

L'articolo si conclude con un'idea semplice e potente:

"Chiudere i gap" (far sì che il codice compili) è la parte facile.

La parte difficile è il design.

L'IA è come un brillante muratore: Può posare i mattoni perfettamente se le dici esattamente dove metterli.
L'IA NON è un architetto: Non può decidere che aspetto debba avere la casa, come debbano fluire le stanze o di quali strumenti avranno bisogno i futuri residenti.

Il Messaggio Chiave:
Non dovremmo solo chiedere: "L'IA ha risolto il problema matematico?" Dobbiamo chiederci: "L'IA ha costruito qualcosa che altri esseri umani possano effettivamente usare?"

Attualmente, l'IA può risolvere l'enigma, ma non può costruire la libreria. Per ottenere un risultato veramente utile, un esperto umano deve ancora intervenire per svolgere il lavoro pesante di progettazione e organizzazione. La "parte difficile" non è dimostrare il teorema; è assicurarsi che la dimostrazione sia un dono per il futuro, non un peso.

Sintesi Tecnica: I "Sorries" Non Sono la Parte Difficile

Problema

La narrativa prevalente nella formalizzazione semi-autonoma si concentra sulla completamento della prova: la capacità di un agente di generare codice che un assistente alla dimostrazione (ad esempio, Lean) accetti come teorema verificato. Tuttavia, gli autori sostengono che un teorema verificato è distinto da un contributo a una libreria riutilizzabile. La matematica moderna si basa su librerie interconnesse dove le definizioni devono combinarsi, gli enunciati dei teoremi devono possedere la giusta generalità e le API devono facilitare il ragionamento futuro senza costringere gli utenti a svelare le implementazioni.

Il problema centrale identificato è che, sebbene i Large Language Models (LLM) siano sempre più capaci di colmare lacune locali nelle prove (rimuovendo i "sorries"), essi faticano con le decisioni di design globale necessarie per produrre formalizzazioni di alta qualità e manutenibili. Nello specifico, gli agenti spesso falliscono nel scegliere definizioni appropriate, nel progettare enunciati di teoremi generalizzabili o nel costruire API pulite, producendo codice che passa il controllo del kernel ma fallisce la revisione esperta come contributo a una libreria.

Metodologia

Il documento presenta un caso di studio dettagliato di una formalizzazione semi-autonoma del teorema di sparizione di Grothendieck (Hartshorne, 1977, Cap. III, Thm. 2.7) in Lean 4. Il teorema afferma che per uno spazio topologico noetheriano $X$ e un intero $n$ maggiore della dimensione di Krull topologica di $X$ , la $n$ -esima coomologia di sheaf di qualsiasi sheaf di gruppi abeliani su $X$ è nulla.

Lo studio segue un disegno sperimentale prima-e-dopo:

Stato A (Formalizzazione Iniziale): Un agente (Claude Code), guidato da un enunciato del teorema fornito da un umano e da un estratto PDF della dimostrazione di Hartshorne, ha generato una formalizzazione che compilava con zero "sorries" (obiettivi non provati).
Revisione Esperta: Un esperto di Lean/mathlib ha revisionato lo Stato A, identificando problemi nelle definizioni, nella generalità dei teoremi, nell'organizzazione dei file e nel design delle API.
Stato B (Formalizzazione Rifattorizzata): L'agente è stato incaricato di affrontare la checklist dell'esperto. Ciò ha comportato un "refactoring guidato dalla revisione" e una successiva fase di "compressione e lucidatura" per allinearsi alle convenzioni di mathlib.
Seconda Revisione: Lo stesso esperto ha revisionato lo Stato B.

L'analisi confronta i due stati attraverso quattro dimensioni: definizioni, enunciati dei teoremi, prove e struttura di file/API. La cronologia del progetto, l'uso di token e le interazioni con gli strumenti sono stati ricostruiti dai log dei commit e dalla telemetria per comprendere i modelli di comportamento dell'agente.

Risultati Chiave e Conclusioni

1. Definizioni: Il Punto di Fallimento Primario

Le definizioni sono state identificate come la componente più debole e l'area in cui l'agente ha mostrato il minor miglioramento tra lo Stato A e lo Stato B.

Stato A: L'agente ha generato 62 definizioni personalizzate. Solo una (TopCat.closedIncl) è stata ritenuta corretta e riutilizzabile. Le altre erano "ad hoc", spesso avvolgendo costruzioni della libreria standard con nomi specifici al contesto della prova corrente (ad esempio, sheafH_filtered_colimit_h1_sectionsFunctor invece di usare sheafSections esistenti).
Conseguenze: Queste definizioni hanno creato "costi di trasporto futuri", costringendo gli utenti successivi a dimostrare equivalenze banali per utilizzare gli oggetti. Hanno inoltre ostacolato le prestazioni dei tattici (ad esempio, simp) oscurando la sintassi sottostante.
Stato B: L'agente non è riuscito a migliorare significativamente la sua capacità di creare definizioni generali e riutilizzabili. Ha continuato a creare oggetti specifici e non necessari invece di progettare costruzioni generali con specializzazioni convenienti.

2. Design delle API: Miglioramento Parziale

Stato A: L'agente non ha costruito un'API per la coomologia di sheaf (Sheaf.H), ma ha ripetutamente svelato la definizione nei file a valle.
Stato B: L'agente ha creato un file API dedicato, che ha pulito le prove a valle. Tuttavia, l'API stessa era "rumorosa e gonfia", contenente circa 800 righe e 24 lemmi altamente specifici invece di un'interfaccia distillata e principesca.
Contrasto: L'agente si è comportato meglio con l'API per topologicalKrullDim (una definizione più semplice), suggerendo che può progettare buone API quando viene sollecitato con compiti specifici e limitati, ma fatica con il design aperto.

3. Enunciati dei Teoremi: Locale vs Globale

Stato A: L'agente ha dimostrato esattamente ciò che era necessario per la prova immediata, usando spesso ipotesi eccessivamente specifiche (ad esempio, richiedendo una "presentazione iniettiva" quando una sequenza esatta breve sarebbe bastata).
Stato B: L'agente è riuscito a generalizzare gli enunciati dei teoremi quando esplicitamente richiesto nella checklist di revisione. Tuttavia, non è stato in grado di identificare le generalizzazioni necessarie autonomamente. L'agente eccelle nelle correzioni sintattiche locali ma manca del giudizio globale per anticipare i futuri bisogni di riutilizzo.

4. Prove: Miglioramento Disomogeneo

Stato A: Le prove contenevano "muri di istruzioni have", uso frequente errato dell'uguaglianza definizionale e svelamento diretto delle definizioni.
Stato B: Le prove sono migliorate, in particolare nei file che utilizzano oggetti esistenti di mathlib. L'agente ha adottato sotto-lemmi nominati per decomporre prove complesse, un pattern rinforzato dai vincoli di "battito cardiaco" (performance).
Limite: Le prove che dipendevano dalle proprie scarse definizioni (ad esempio, nei file di colimit filtrati) rimanevano difficili da leggere e mantenere.

5. Dinamiche del Processo

Adattamento al Feedback: L'agente si è adattato bene al feedback con predicati di completamento netti (ad esempio, "rinomina questo file", "generalizza questa ipotesi"). Ha faticato con il feedback che richiedeva un giudizio controfattuale (ad esempio, "progetta un'API che sarà utile in futuro").
Vie di Fuga: Gli agenti tendevano a dichiarare i compiti "bloccati" o a incolpare l'infrastruttura (ad esempio, "gap di mathlib") di fronte a difficili decisioni di design. Sono stati necessari prompt espliciti che vietassero queste frasi per forzare la decomposizione.
Metriche: "Chiudere i sorries" è una metrica insufficiente per la qualità. Il progetto è continuato ad evolversi significativamente (in termini di righe di codice e struttura) molto tempo dopo che il conteggio dei sorries è arrivato a zero.

Significato e Rivendicazioni

Il documento sostiene che la valutazione dell'autoformalizzazione deve estendersi oltre il semplice completamento binario della prova. Gli autori affermano che:

L'accettazione del kernel è incompleta: Un teorema può essere verificato dal kernel pur costringendo gli utenti futuri attraverso coercizioni goffe, definizioni duplicate e API ingestibili.
Il "Gap di Riutilizzabilità": Esiste una netta separazione tra la capacità di un agente di chiudere obiettivi locali e la sua capacità di scegliere definizioni e progettare API. Questa seconda parte richiede un giudizio sul riutilizzo futuro che gli attuali LLM non possiedono.
Standard di Valutazione: Gli autori propongono che i sistemi di AI-per-la-matematica debbano essere valutati in base al fatto che la formalizzazione risultante superi la revisione esperta. Nello specifico, dopo che una prova è passata il controllo, un esperto dovrebbe revisionare le definizioni pubbliche, gli enunciati dei teoremi, gli spazi di nomi e le superfici API per misurare la capacità del sistema di rispondere al feedback di design.

Lo studio conclude che, senza un sofisticato apparato per il design globale, gli LLM sono capaci di produrre "artefatti verificati" ma non ancora "contributi a una libreria riutilizzabili". La strada da seguire prevede l'uso di esperti umani per definire le specifiche di qualità (definizioni, interfacce) e di agenti per gestire i refactoring più stretti e meccanicamente verificabili.