Quanto restano valide le dimostrazioni generate dagli LLM dopo il refactoring di un programma? Uno stress test per la generazione di codice verificabile

Abstract degli autori

I benchmark per la generazione di codice verificabile di solito mettono alla prova una dimostrazione rispetto a un’unica implementazione fissa. Ci chiediamo se la stessa dimostrazione resti valida dopo un refactoring del programma che ne preserva il comportamento. Presentiamo RefactorProof, che ricava 458 varianti certificate da Lean dai 185 task di VERINA che vengono compilati nell’ambiente da noi fissato, mantenendo identici, byte per byte, la specifica e la dimostrazione valutata. VERINA fornisce dimostrazioni di riferimento per 46 task, tutti appartenenti alla sua partizione basic; i confronti principali tra modelli e riferimenti si svolgono inoltre su insiemi corrispondenti di 21-25 task brevi e non ricorsivi. I refactoring strutturali rivelano una notevole fragilità nelle dimostrazioni di diversa provenienza: il PSR strutturale normalizzato per task è del 4,3% per le dimostrazioni di riferimento fornite e del 13,3-26,8% per i dimostratori specializzati. Nei task corrispondenti, tuttavia, le dimostrazioni dei dimostratori specializzati restano complessivamente valide senza modifiche più spesso delle dimostrazioni di riferimento fornite: +15,6 punti per DeepSeek-Prover-V2-7B, +18,8 per Goedel-Prover-V2-32B e +20,3 per Goedel-Prover-V2-8B; tutti e tre gli intervalli di confidenza al 95% escludono lo zero. Questo ordine si mantiene anche escludendo le varianti T1 per le quali tutte le dimostrazioni restano valide, con un’aggregazione bilanciata per famiglia e applicando criteri alternativi di selezione delle dimostrazioni valide utilizzabili. Il fatto che una dimostrazione non resti valida senza modifiche, però, non implica un costo di riparazione elevato: modifiche predefinite a un solo identificatore riparano 51/54 dei casi idonei in cui falliscono strutturalmente le dimostrazioni di riferimento e 58/85 dei casi idonei in cui falliscono quelle dei dimostratori. RefactorProof misura quindi la stabilità delle dimostrazioni senza modifiche a fronte del refactoring del programma, non il costo di manutenzione di una dimostrazione dopo che ha smesso di essere valida.