Scalare la dimostrazione di teoremi in Lean per la verifica del codice nel mondo reale

Abstract degli autori

Presentiamo EasyProver, un sistema per dimostrare teoremi in Lean basato su agenti ricorsivi con contesti isolati, ricerca asincrona, esplorazione parallela di tattiche e un servizio di elaborazione con capacità elastica. Usando un modello di frontiera pronto all’uso, senza addestramento aggiuntivo, dimostra 669/672 problemi di PutnamBench e tutte e sei le formalizzazioni IMO 2026, e risolve 597/600 condizioni di verifica NTP4VC e tutti i 189 compiti VERINA mediante dimostrazione o confutazione. Poiché questi benchmark sono prossimi alla saturazione, introduciamo anche Aegis, che trasforma problemi di programmazione competitiva in compiti di verifica molto più difficili, basati su implementazioni reali. La pipeline scrive soluzioni in Rust sicuro, le traduce in Lean con Aeneas, genera specifiche ed etichetta ogni enunciato fissato con una dimostrazione o una confutazione verificata dal kernel. Produce 2.045 coppie di programmi Rust-Lean convalidate tramite verifica differenziale e 11.533 specifiche candidate. A differenza dei benchmark scritti a mano, questi compiti comportano obblighi a livello di implementazione legati all’aritmetica a larghezza fissa, al fallimento esplicito, ai cicli generati, alle conversioni di tipo e alla mutazione resa funzionale. Su un campione stratificato di 2.000 enunciati, EasyProver ne dimostra 1.054 (il 52,7%) entro un budget di 30 minuti per enunciato. Gli stessi compiti possono anche essere usati per valutare altri dimostratori e come ricompense per l’apprendimento per rinforzo.