Riassunto Tecnico: Visored: Un Prover di Linguaggio Naturale Controllato per la Matematica Generata da LLM

Problematica

I Large Language Models (LLM) hanno dimostrato una capacità crescente nel ragionamento matematico, tuttavia rimangono soggetti a allucinazioni. Di conseguenza, le dimostrazioni generate dall'IA sono affidabili solo quanto il processo di verifica. Sebbene i dimostratori automatici di teoremi (ATP) e i modelli di intera dimostrazione (ad esempio, quelli che prendono di mira Lean o Rocq) abbiano raggiunto alti tassi di successo su benchmark come miniF2F, essi richiedono tipicamente una dichiarazione già formalizzata come input. Il collo di bottiglia critico risiede nell'autoformalizzazione: la traduzione della prosa matematica informale in una forma verificabile dalla macchina.

Questa traduzione è non banale perché la matematica informale si basa su un background condiviso, condizioni laterali implicite (ad esempio, $x \neq 0$) e abusi di notazione che i lettori colmano automaticamente. Una traduzione diretta in un linguaggio formale richiede di impegnarsi verso specifici lemmi di libreria, sottotipi, convenzioni per i casi limite e coercizioni (ad esempio, $\mathbb{N}$ vs. $\mathbb{Z}$ vs. $\mathbb{R}$) che non lasciano traccia nel testo sorgente. Gli errori in queste decisioni raramente si manifestano come errori del compilatore, ma piuttosto come "deriva semantica silenziosa", dove un'affermazione compila ma non riflette più l'intento originale.

Metodologia

Visored è un prototipo di ricerca progettato per colmare il divario tra la scrittura matematica informale e la verifica formale, introducendo una rappresentazione intermedia (IR) a tipi dipendenti che si colloca tra LaTeX e i linguaggi a basso livello come Lean.

Architettura Core

Il sistema opera attraverso una pipeline (Figura 2 nel paper) composta dalle seguenti fasi:

1. Input in Linguaggio Naturale Controllato (CNL): Visored accetta un sottoinsieme controllato di inglese matematico incorporato in LaTeX. Il vocabolario (template di frasi come "Let...", "Assume...", "Then..." e comandi LaTeX) è definito da file di specifica esterni .lpcsv, consentendo di estendere il linguaggio superficiale senza modificare il parser.
2. Sintassi e Semantica: L'input viene analizzato in un albero sintattico e poi elaborato in un AST tipizzato (sem AST). Questa fase risolve i nomi, assegna tipi e classi, ed impone la ben-definizione al momento del controllo dei tipi. Seguendo la tradizione di PVS, le funzioni parziali (ad esempio, $1/x$, $\sqrt{x}$, $\log x$) portano argomenti di ipotesi impliciti (ad esempio, $x \neq 0$, $x \ge 0$) che devono essere soddisfatti prima che l'espressione sia accettata.
3. IR di Medio Livello (MIR): L'AST tipizzato viene abbassato a Visored MIR, il substrato per il solver.
4. Solver con Limite di Costo: Il solver soddisfa le obbligazioni "Then..." e le condizioni di ben-definizione utilizzando un motore guidato da regole e con limiti di costo (chiamato "Miracle"). Esso impiega un database di regole backward e forward (ispirato a ProofGrader) e tattiche specializzate (ad esempio, normalizzatori algebrici, solver a catena) per chiudere i passaggi di routine che i matematici tipicamente omettono.
5. Emissione Opzionale in Lean: Le dimostrazioni accettate possono essere trasposte in Lean 4. Il processo di trasposizione prevede la riproduzione della cronologia di normalizzazione e la gestione delle testimonianze di coercizione tra sistemi numerici.

Filosofia di Design

Visored è costruito su due osservazioni primarie:

1. Fluidità degli LLM: Gli LLM sono addestrati prevalentemente sulla matematica informale. Un CNL superficiale rimane vicino al dominio in cui gli LLM sono già fluidi, evitando la necessità per il modello di apprendere da zero la sintassi dei low-level prover (tattiche, nomi di lemmi di libreria).
2. Trattabilità: Colmare il divario tra ragionamento naturale e formale è più trattabile rispetto al teorema automatico completo. Avendo l'LLM che fornisce lo schema della dimostrazione in CNL, il solver deve solo chiudere piccoli passaggi ovvi, un compito ben entro la portata dell'ingegneria agentica moderna.

Il sistema tratta il parsing semantico "verso l'alto" (LaTeX $\to$ Visored) come il problema difficile, gestito dall'LLM, mentre la proiezione "verso il basso" (Visored $\to$ Lean) è un processo deterministico e meccanico.

Contributi Chiave

• IR a Tipi Dipendenti per l'Autoformalizzazione: Visored introduce un IR semanticamente ricco dove ogni decisione priva di traccia superficiale in LaTeX (sottotipi, lemmi di libreria, convenzioni per i casi limite, cast) è resa esplicita.
• Estensibilità Guidata da Specifiche: La superficie CNL è definita da file di configurazione esterni piuttosto che da parser codificati, permettendo di sintonizzare il vocabolario su specifiche convenzioni matematiche (testuali, di competizione, di ricerca) senza ricompilare il sistema.
• Diagnostica Localizzata: A differenza dei sistemi che forniscono un unico verdetto di accettazione/rifiuto dopo una completa compilazione in Lean, Visored fornisce diagnostiche localizzate durante la fase di elaborazione o risoluzione. Ciò consente un ciclo di "verifica e revisione" in cui un LLM può individuare e correggere errori specifici.
• Enforcement della Ben-Definizione: Il sistema impone la ben-definizione (ad esempio, assicurando che $x \neq 0$ prima di $1/x$) tramite argomenti di ipotesi impliciti soddisfatti dal solver, piuttosto che affidarsi alle convenzioni di totalizzazione del target prover.
• Integrazione di Scuole Esistenti: Visored sintetizza elementi di Mizar/Naproche (superficie CNL), PVS (ben-definizione al tempo di controllo dei tipi), Lean/Rocq (tipi dipendenti) e ProofGrader (risoluzione guidata da regole con budget di costo) in una singola pipeline rivolta agli LLM.

Risultati Sperimentali

Gli autori riportano uno studio di copertura sul split miniF2F-valid (244 problemi), che ha servito sia come set di sviluppo che di valutazione.

• Performance: Un agente di codifica LLM (Claude), guidato da un documento di competenze che descrive la superficie CNL, ha prodotto dimostrazioni verificate da Visored per 222 problemi su 244 (91%).
• Suddivisione:
  • Induzione: 100% (8/8)
  • Algebra: 98% (86/88)
  • Teoria dei Numeri: 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (Olimpiadi): 35% (7/20)
• Analisi dei Fallimenti: I problemi non risolti sono stati attribuiti a lacune nel database di regole di Visored (ad esempio, mancanza della disuguaglianza AM-GM, assenza di tipi di campi finiti, identità trigonometriche) o regressioni nel prototipo, piuttosto che all'incapacità dell'LLM di trovare la strategia di dimostrazione. Gli autori dichiarano esplicitamente che l'agente ha fallito nel risolverli perché la necessaria "macchina" non era ancora stata implementata nel sistema.
• Costo di Trasposizione: L'attuale schema di emissione sparsa risulta in un output Lean altamente verboso, con un rapporto mediano del numero di righe di $\approx 250\times$ rispetto alle dimostrazioni Lean scritte a mano, con una coda che raggiunge $\approx 25.000\times$. Ciò è dovuto alla riproduzione dei passaggi di normalizzazione e delle testimonianze di coercizione.

Significato e Rivendicazioni

Il paper posiziona Visored non come un competitore per l'automated theorem proving, ma come una prova di concetto per una nuova infrastruttura per controllare e organizzare la matematica informale prodotta dall'IA.

• Rivendicazioni Modeste: Gli autori dichiarano esplicitamente di non rivendicare un automated theorem proving competitivo, né di estrapolare i risultati a split di test non visti. Il 91% di copertura è presentato come un limite inferiore di ciò che il design può esprimere, non come un tasso di successo ottimizzato.
• Spostamento del Collo di Bottiglia: Il lavoro sostiene la visione secondo cui il vincolo principale nella matematica IA si sta spostando dalla "generazione di idee" alla "verifica e organizzazione delle stesse su scala".
• Modalità di Utilità: Visored è progettato per funzionare in quattro modalità:
  1. Verificatore al tempo di inferenza: Un controllore in tempo reale per gli output degli LLM.
  2. Ciclo di autoformalizzazione: Un meccanismo per permettere agli LLM di riscrivere le dimostrazioni basandosi su diagnostiche localizzate.
  3. Segnale di ricompensa denso: Fornire feedback per singolo step per il Reinforcement Learning (RL).
  4. Generatore di dati CNL: Creare un corpus rinnovabile di dimostrazioni che leggono naturalmente e sono formalmente verificate.

Il paper conclude che la combinazione di una superficie CNL, un IR a tipi dipendenti e un solver guidato da regole crea una pipeline in cui i fallimenti sono localizzati e azionabili, offrendo una via più affidabile dalla prosa informale alle dimostrazioni verificate dal kernel rispetto agli attuali approcci di autoformalizzazione diretta. I problemi non risolti rappresentano un arretrato di regole e macchine mancanti, non un limite fondamentale del design.