💻 computer science

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

Lean Refactor è un framework agentico di retrieval-augmented che ottimizza le prove Lean per molteplici obiettivi, tra cui compressione dei token, velocità di compilazione e compatibilità delle versioni, selezionando dinamicamente strategie di refactoring curate senza richiedere il riaddestramento del modello.

Autori originali: Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

Pubblicato 2026-05-21

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

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

Il Problema: La Prova "Sovra-ingegnerizzata"

Immagina un architetto brillante ma eccessivamente entusiasta (l'IA) che ha appena costruito una casa (una prova matematica). La casa è strutturalmente solida: non crollerà e supera tutti i controlli di sicurezza. Tuttavia, l'architetto ha utilizzato 500 mattoni per costruire un muro che ne richiedeva solo 50. Ha usato un martello pneumatico per schiacciare una noce.

Nel mondo di Lean (un linguaggio utilizzato per scrivere prove matematiche verificabili dai computer), i modelli di IA spesso producono prove che sono corrette ma incredibilmente lunghe, disordinate e lente da compilare.

Troppo lunghe: La prova è difficile da leggere per gli umani.
Troppo lente: Poiché la prova è gonfia di passaggi non necessari, il computer impiega molto tempo per verificare se è valida.
Fragili: Il linguaggio Lean cambia frequentemente (come gli aggiornamenti software). Una prova scritta per la "Versione 1.0" potrebbe rompersi completamente quando il computer si aggiorna alla "Versione 2.0", anche se la matematica è ancora corretta.

Gli strumenti esistenti hanno cercato di risolvere il problema riaddestrando l'IA (cosa costosa e lenta) o semplicemente chiedendole di "essere più breve" (cosa che spesso rende la prova più lenta da eseguire).

La Soluzione: Il Sistema "Bibliotecario Intelligente"

Gli autori hanno creato Lean Refactor. Invece di tentare di riaddestrare l'IA, hanno costruito un sistema "plug-and-play" che agisce come un bibliotecario super-intelligente per l'IA.

Ecco come funziona, usando una metafora:

1. La Banca delle Strategie (La Biblioteca)

Immagina una biblioteca enorme piena di "Carte del Refactoring". Ogni carta descrive un trucco specifico per accorciare una prova.

Il Trucco: "Invece di elencare ogni numero uno per uno, usa questa singola formula magica."
I Metadati: Crucialmente, ogni carta ha un'etichetta. Dice:
- Quanto tempo risparmia? (es. "Risparmia il 30% del tempo di compilazione").
- Su quale versione del linguaggio funziona? (es. "Funziona su Lean v4.16 e v4.22").
- Di quanto accorcia la prova?

Il documento afferma di aver costruito la più grande biblioteca di queste carte mai realizzata, contenente oltre 9.000 strategie uniche distillate da centinaia di migliaia di esempi di prove.

2. L'Agente (L'Architetto + Il Bibliotecario)

Quando l'IA deve correggere una prova, non indovina. Segue un ciclo:

Il Pianificatore: L'IA esamina la prova disordinata e dice: "Questa sezione sembra aver bisogno di un trucco 'Formula Magica'".
Il Bibliotecario (Recupero): Il sistema va alla biblioteca e estrae le carte specifiche che corrispondono a quella sezione.
- Se vuoi la prova più breve: Estrae le carte che promettono la maggiore riduzione delle dimensioni.
- Se vuoi la compilazione più veloce: Estrae le carte che promettono il maggiore aumento di velocità.
- Se stai usando una vecchia versione di Lean: Filtra tutte le carte che non funzionano sulla tua versione.
Il Refactorer: L'IA applica il trucco dalla carta per riscrivere la prova.
Il Debugger: Il computer verifica la nuova prova. Se si rompe, l'IA cerca di correggere l'errore localmente senza annullare l'intero miglioramento.

Perché Questo è Speciale (Le Affermazioni del Documento)

1. Bilancia obiettivi in competizione (La Magia "Multi-Obiettivo")
Di solito, devi scegliere: "Voglio che la prova sia breve, o voglio che compili velocemente?"

Vecchio Metodo: Ne scegli uno e l'altro ne risente.
Lean Refactor: Puoi dire al sistema: "Voglio che sia breve, ma anche veloce". Il sistema guarda le carte della biblioteca, vede quali offrono entrambe le cose e sceglie il miglior equilibrio.
Risultato: Su problemi matematici da competizione, hanno ridotto le prove di oltre il 70% e tagliato il tempo di compilazione di oltre il 60%.

2. Sopravvive agli aggiornamenti software (La "Robustezza della Versione")
Poiché le carte della biblioteca sono etichettate con le specifiche versioni software su cui funzionano, il sistema può filtrare istantaneamente i trucchi "obsoleti".

Risultato: Se chiedi una prova per "Lean v4.16", il sistema usa solo carte che funzionano per la v4.16. Questo impedisce all'IA di allucinare (inventare) strumenti che non esistono in quella versione.

3. Funziona con qualsiasi IA (La Funzione "Model Agnostic")
Non è necessario addestrare una nuova IA per questo. Il sistema funziona con qualsiasi modello di IA "congelato" (pre-addestrato), sia che provenga da Google (Gemini), Anthropic (Claude) o OpenAI (GPT). L'"intelligenza" deriva dalla biblioteca di strategie, non dal cervello dell'IA.

Risultato: L'hanno testato su diversi modelli di IA e ha migliorato le prestazioni di tutti, battendo persino un agente di codifica specializzato chiamato "Claude Code".

La Conclusione

Lean Refactor è come fornire a una squadra di costruttori un set di progetti e una scatola di attrezzi con scorciatoie pre-testate ed etichettate. Invece di indovinare come costruire una casa, guardano il modo migliore per costruire un muro specifico in base agli strumenti che hanno e alla versione del codice edilizio che stanno utilizzando.

Il documento afferma che questo approccio:

Riduce le prove del 70%+ nelle competizioni matematiche.
Le rende 60% più veloci da compilare.
Le mantiene funzionanti anche quando il linguaggio software si aggiorna.
Fa tutto questo senza bisogno di riaddestrare i modelli di IA.

Riepilogo Tecnico: Lean Refactor

Enunciato del Problema

I Modelli Linguistici di Grandi Dimensioni (LLM) addestrati con apprendimento per rinforzo (RL) per la dimostrazione di teoremi formali in Lean generano spesso dimostrazioni che sono corrette ma notoriamente verbose, fragili e computazionalmente costose. Sebbene esistano sforzi di rifattorizzazione esistenti, questi incontrano tre limitazioni fondamentali quando applicati all'ecosistema Lean:

Tensione Multi-Obiettivo: La rifattorizzazione in Lean è intrinsecamente multi-obiettivo. L'ottimizzazione della lunghezza della dimostrazione spesso entra in conflitto con la minimizzazione del costo di compilazione (ad esempio, dimostrazioni più brevi possono invocare tattiche pesanti che aumentano i tempi di compilazione), e i metodi esistenti mancano di meccanismi principiali per bilanciare questi compromessi o adattarsi a obiettivi utente non visti al momento dell'inferenza.
Fragilità delle Versioni: Lean e la sua libreria standard, Mathlib, evolvono su base quasi settimanale con frequenti cambiamenti dell'API e rinominazioni dei lemmi. Gli LLM all'avanguardia hanno cutoff di conoscenza statici, portando a allucinazioni di tattiche obsolete e incompatibilità con le attuali catene di strumenti.
Scarsità di Dati: A differenza dei linguaggi di programmazione mainstream, Lean manca di dataset accoppiati su larga scala (coppie codice rumoroso-pulito) necessari per le pipeline di rifattorizzazione basate sull'addestramento. Inoltre, gli approcci basati sull'addestramento richiedono un fine-tuning ripetuto per ogni nuova release di LLM, fallendo nel scalare con il turnover dei modelli o con il ciclo di release di Lean.

Metodologia: Lean Refactor

Gli autori propongono Lean Refactor, un framework agenziale di recupero-aumentato plug-and-play progettato per rifattorizzare le dimostrazioni in Lean senza eseguire il fine-tuning dell'LLM sottostante. Il sistema disaccoppia la logica di rifattorizzazione dal modello esternalizzando la conoscenza in un database strutturato e densamente annotato.

1. Banca di Strategie Densamente Annotata

Il cuore del framework è un database curato di 9.237 strategie di rifattorizzazione uniche distillate da oltre 200.000 coppie di dimostrazioni lunghe-brevi.

Struttura: Ogni strategia include un titolo, una descrizione, una precondizione ("quando applicare"), una guida passo-passo per l'applicazione ed esempi astratti prima/dopo.
Metadati: Crucialmente, ogni strategia è annotata con metadati che l'LLM non può inferire dai dati di addestramento:
- Riduzione del Tempo di Compilazione: Il speedup relativo mediano osservato quando si applica la strategia.
- Compatibilità delle Versioni: Un insieme di catene di strumenti Lean/Mathlib validate (ad esempio, v4.14.0, v4.16.0, v4.22.0) sotto le quali la dimostrazione rifattorizzata compila con successo. Ciò è determinato ricompilando le dimostrazioni accorciate su più versioni.

2. Recupero e Rianordino Multi-Obiettivo

All'inferenza, il framework impiega una pipeline di recupero che si adatta agli obiettivi specificati dall'utente senza riaddestramento del modello:

Dimostrazione più Breve: Recupera strategie basandosi puramente sulla similarità semantica (similarità del coseno) al segmento della dimostrazione.
Consapevole del Tempo di Compilazione: Recupera un ampio pool di candidati semanticamente simili e poi rianordina questi ultimi basandosi sui metadati annotati di riduzione del costo di compilazione.
Specifico per la Versione: Filtra il pool dei candidati per includere solo strategie i cui metadati di compatibilità includono la versione Lean target dell'utente.

3. Ciclo Agenziale

Il framework incapsula questi componenti in un ciclo agenziale agnostico rispetto al modello costituito da:

Pianificatore: Decompone il compito di rifattorizzazione in passaggi specifici basati sulle strategie recuperate.
Rifattorizzatore: Esegue il piano per generare una dimostrazione più breve.
Debugger: Utilizza il feedback del compilatore per riparare gli errori in un ciclo chiuso (fino a $D$ round).
Agnosticismo del Modello Sottostante: Il pianificatore, il rifattorizzatore e il debugger possono essere istanziati da qualsiasi LLM all'avanguardia congelato (ad esempio, serie Gemini, Claude, GPT), permettendo al sistema di trasferirsi tra modelli senza riaddestramento.

Contributi Chiave

Rilascio del Dataset: Gli autori rilasciano il più grande dataset di rifattorizzazione Lean a oggi, comprendente oltre 200K coppie di dimostrazioni lunghe-brevi e 9K strategie di rifattorizzazione, ciascuna annotata con costo di compilazione e compatibilità delle versioni.
Prestazioni: Lean Refactor ottiene una compressione a livello di token >70% sui benchmark di competizione (miniF2F, PutnamBench) e >20% sui repository di ricerca (Analysis, FLT, PhysLean). Riduce inoltre il tempo di compilazione fino al 60% sui benchmark di competizione.
Controllabilità e Robustezza: Il sistema supporta il controllo multi-obiettivo (lunghezza vs velocità vs compatibilità) tramite regole di recupero piuttosto che pesi del modello. Le dimostrazioni rifattorizzate mostrano un trasferimento zero-shot più forte verso future release di Lean rispetto alle controparti non rifattorizzate e ai precedenti metodi di ottimizzazione.
Agnosticismo del Modello: Il framework migliora le prestazioni su diversi backbones LLM (Gemini 3 Flash, Claude Haiku 4.5) e supera agenti di codifica generici come Claude Code, anche quando quest'ultimo ha accesso allo stesso strumento di recupero delle strategie.

Risultati Sperimentali

Riduzione della Lunghezza: Sui benchmark di competizione, Lean Refactor supera lo stato dell'arte precedente, ProofOptimizer, ottenendo una riduzione dell'88,40% su miniF2F e del 70,38% su PutnamBench (contro il 57,20% di ProofOptimizer). Sulle dimostrazioni a livello di ricerca, ottiene una riduzione media del 20–33%, superando significativamente le baseline di ablazione.
Tempo di Compilazione: Rianordando le strategie basandosi sui metadati del costo di compilazione, il framework ottiene una riduzione relativa del 42,62% del tempo di compilazione su PutnamBench, rispetto al 37,11% dell'approccio di recupero standard.
Compatibilità delle Versioni: Quando si mirano a versioni specifiche di Lean (ad esempio, v4.16.0), il recupero filtrato per versione produce costantemente una migliore riduzione della lunghezza rispetto al recupero non filtrato. Le dimostrazioni rifattorizzate mantengono la capacità di controllo dei tipi su più future release di Lean (fino a v4.29.0) rispetto a quelle prodotte da ProofOptimizer o dalle dimostrazioni verbose originali.
Riduzione delle Dipendenze: Le dimostrazioni rifattorizzate riducono le dipendenze esterne e intra-progetto nel 42–67% dei casi, indicando una genuina semplificazione logica piuttosto che un semplice scarico su lemmi pesanti della libreria.

Significato

Il documento sostiene che Lean Refactor affronta i colli di bottiglia critici nel mantenimento delle librerie matematiche formali: la tensione tra concisione della dimostrazione ed efficienza di compilazione, e la fragilità del codice attraverso catene di strumenti in rapida evoluzione. Esternalizzando la conoscenza di rifattorizzazione in una banca di strategie ricca di metadati, il framework abilita un'ottimizzazione multi-obiettivo controllabile senza la necessità di costosi fine-tuning del modello. Questo approccio permette al sistema di rimanere robusto contro la deriva delle versioni di Lean/Mathlib e adattabile immediatamente a nuovi backbones LLM, gettando le basi per dimostrazioni formali più mantenibili e resilienti alle versioni.