Sintesi Tecnica: Oltre la Compilazione: Valutare la Formalizzazione Fedele di Enunciati da Linguaggio Naturale a Lean

1. Definizione del Probleamento

Il documento affronta il compito della formalizzazione di enunciati da linguaggio naturale a Lean: la traduzione automatica di enunciati matematici informali in dichiarazioni di teoremi valide in Lean 4. Questo compito è distinto dalla dimostrazione di teoremi. Nei benchmark di dimostrazione (es. MiniF2F, LeanDojo), l'enunciato formale è fisso e affidabile; l'obiettivo del sistema è generare una dimostrazione accettata dal verificatore. Nella formalizzazione degli enunciati, il sistema deve generare l'enunciato stesso.

La sfida centrale è che la compilazione è una condizione necessaria ma insufficiente per il successo. Una dichiarazione Lean può superare il controllo dei tipi (compilare) pur:

• Omettendo ipotesi critiche.
• Modificando il dominio del discorso.
• Rafforzando o indebolendo la tesi.
• Codificando una versione vacua del risultato.

I lavori precedenti si sono spesso basati sui tassi di compilazione o su metriche di equivalenza basate su riferimenti (es. BEq, back-translation). Questo articolo sostiene che la sola compilazione crei un "gap di compilazione riuscita" (compile-pass gap) in cui i sistemi appaiono efficaci ma falliscono nel preservare il significato matematico inteso. Gli autori definiscono il problema centrale come la valutazione della formalizzazione fedele dell'enunciato: generare dichiarazioni che compilino e preservino l'intento semantico dell'input in linguaggio naturale.

2. Metodologia

2.1 Costruzione del Benchmark

Gli autori hanno curato un benchmark di livello specialistico (graduate-level) composto da 400 enunciati in linguaggio naturale derivati da note di lezione e libri di testo LaTeX open-source. Il dataset è bilanciato tra quattro domini:

• Analisi Reale (100 voci)
• Analisi Complessa (100 voci)
• Topologia (100 voci)
• Algebra (100 voci)

Fondamentalmente, questi enunciati non hanno dichiarazioni Lean di riferimento (gold), garantendo che il compito rappresenti una vera traduzione piuttosto che un recupero di informazioni.

2.2 Protocollo di Valutazione

Il documento propone una metrica di Consenso LLM-as-Judge (LLM come giudice), calibrata da esperti umani, per valutare la fedeltà. Il protocollo prevede due fasi:

1. Verifica del Compilatore: Qualsiasi codice che non compila è immediatamente considerato non fedele.
2. Consenso Semantico: Per il codice che compila, due giudici LLM indipendenti (GPT-5.2 e Gemini-2.5-Pro) confrontano la dichiarazione Lean generata con l'enunciato originale in linguaggio naturale. Essi assegnano un punteggio di fedeltà (0–10).
   • Metrica di Successo: Una traduzione è considerata Fedele se e solo se compila E entrambi i giudici le assegnano un punteggio $\ge 9$.
   • Questo approccio di consenso rigoroso è progettato come un punto operativo conservativo per il confronto tra sistemi, non come una prova formale di equivalenza.

2.3 Calibrazione Umana

Per validare la metrica automatizzata, gli autori hanno condotto audit umani:

• Consenso-Positivo: Il 96,0% degli output etichettati come fedeli dal consenso rigoroso è stato confermato fedele dai revisori umani.
• Consenso-Negativo (Compile-Pass): L'82,4% degli output che sono compilati ma sono stati rifiutati dal consenso è stato confermato come un reale fallimento semantico dagli umani.
  Ciò conferma che la metrica è un filtro ad alta precisione e conservativo che identifica efficacemente la deriva semantica.

2.4 Setup Sperimentale: Design Fattoriale

Gli autori hanno valutato vari sistemi (LLM general-purpose, formalizzatori specializzati, modelli orientati alla dimostrazione e agenti potenziati da strumenti) utilizzando un design fattoriale $2^3$ per scomporre gli effetti di tre comuni interventi:

1. Drafting Esperto Parametrico (T): Utilizzo di un modello fine-tuned (Herald) per generare una bozza iniziale.
2. Ricerca della Conoscenza (S): Utilizzo di strumenti per interrogare Mathlib (ricerca simboli, risoluzione namespace) e per effettuare ricerche sul web per l'ancoraggio (grounding).
3. Feedback di Elaborazione Lean (F): Utilizzo di un REPL per compilare iterativamente il codice e ricevere messaggi di errore per la riparazione.

L'architettura dell'agente utilizza un orchestratore centrale (GPT-5.2) che mantiene lo stato e decide quali strumenti invocare in base alla configurazione.

3. Risultati Chiave

3.1 Il Gap di Compilazione Riuscita (Compile-Pass Gap)

Il risultato empirico più significativo è la divergenza tra i tassi di compilazione e la fedeltà semantica:

• Un agente completo potenziato da strumenti ha raggiunto un tasso di compilazione dell'89,5%.
• Tuttavia, sotto la metrica di consenso rigorosa, solo il 60,5% degli output è stato ritenuto fedele.
• Ciò lascia un gap di 29,0 punti in cui gli output compilano ma falliscono i controlli semantici. Gli audit umani hanno confermato che la maggior parte di questi casi "compilano ma sono negativi al consenso" sono reali fallimenti semantici (es. ipotesi mancanti, asserzioni vacue).

3.2 Performance dei Modelli

• Formalizzatori Specializzati e Modelli di Dimostrazione: I formalizzatori di enunciati dedicati (es. Herald, Kimina-Autoformalizer) e i modelli orientati alla dimostrazione (es. Goedel-Prover, Kimina-Prover) hanno ottenuto scarse prestazioni nella generazione di enunciati quando il target formale non veniva fornito. I loro tassi di fedeltà variavano tra il 4,0% e il 12,3%.
• LLM General-Purpose: Gli LLM general-purpose con approccio one-shot hanno raggiunto una fedeltà del 19,8–28,0%.
• Agenti Potenziati da Strumenti: Il framework dell'agente completo ha superato significativamente i baseline one-shot, raggiungendo una fedeltà del 60,5%. Tuttavia, diversi orchestratori (Sonnet 4.5, Gemini-2.5-Pro) hanno converguto verso livelli di performance simili (60–65%) nonostante i diversi baseline, suggerendo che i guadagni siano strutturali all'approccio potenziato da strumenti piuttosto che legati al modello orchestratore specifico.

3.3 Decomposizione Fattoriale degli Interventi

Lo studio ha isolato l'impatto dei tre strumenti:

• Feedback di Elaborazione (F): È stato il principale motore della validità (compilazione), aumentando significativamente il tasso di compilazione. Tuttavia, ha anche ampliato il contenitore "compila ma non è fedele", poiché ha permesso il passaggio di più dichiarazioni sintatticamente corrette ma semanticamente deviate.
• Ricerca (S): La ricerca ha migliorato principalmente l'ancoraggio (grounding) e la selettività. Ha ridotto il gap di compilazione riuscita (ovvero, ha aiutato a filtrare le dichiarazioni semanticamente errate che riuscivano a compilare) e ha migliorato l'efficienza riducendo il numero di iterazioni REPL necessarie. Il suo beneficio marginale era massimo in assenza di feedback.
• Drafting Esperto (T): Il prior di drafting fine-tuned era in gran parte sostituibile una volta disponibili feedback ed esplorazione. Infatti, con il feedback completo, il drafting prior ha leggermente danneggiato le performance, suggerendo che un orchestratore forte con feedback del compilatore può superare un draft specializzato in questo specifico stack di strumenti.

3.4 Variazioni Specifiche per Dominio

• Analisi Complessa ha mostrato i maggiori guadagni dal feedback del compilatore (+54,2 punti in fedeltà), probabilmente grazie alla maturità della copertura di Mathlib.
• Analisi Reale e Algebra hanno mostrato guadagni minori, indicando o un supporto limitato delle librerie o una maggiore difficoltà intrinseca di formalizzazione.
• Topologia ha presentato sfide specifiche con concetti avanzati (es. spazi di copertura), dove il feedback portava spesso a dichiarazioni valide ma semanticamente spostate.

4. Significato e Rivendicazioni

Il documento sostiene che la formalizzazione degli enunciati deve essere valutata come preservazione del significato, non semplicemente come accettazione da parte di Lean. I contributi primari sono:

1. Una Nuova Metrica: Una metrica basata sul consenso e calibrata dallamente dagli umani che espone il "gap di compilazione riuscita", rivelando che molti sistemi generano dichiarazioni sintatticamente valide ma semanticamente errate.
2. Decomposizione Diagnostica: Un'analisi fattoriale che mostra come gli strumenti non siano add-on monotoni. Mentre il feedback corregge la sintassi, può oscurare gli errori semantici; la ricerca migliora l'ancoraggio ma ha rendimenti decrescenti in presenza di feedback; e il drafting specializzato non è sempre necessario in un ciclo ricco di feedback.
3. Confronto tra Sistemi: L'evidenza che gli attuali modelli orientati alla dimostrazione e i formalizzatori specializzati non trasferiscono automaticamente le loro capacità di dimostrazione alla generazione di enunciati semanticamente fedeli senza un esplicito addestramento centrato sugli enunciati o protocolli potenziati da strumenti.

Gli autori concludono che i futi sistemi dovrebbero accoppiare un forte feedback di Lean con la valutazione semantica e politiche che decidano quando cercare, riparare o fermarsi, piuttosto che fare affidamento solo sui guadagni medi di accuratezza. Il documento evita esplicitamente di rivendicare che la propria metrica sia una prova formale di equivalenza, posizionandola invece come un confine decisionale conservativo e scalabile per il confronto tra sistemi.