FVSpec: Real-World Property-Based Tests as Lean Challenges

Riepilogo Tecnico: FVSpec

Problema

Il documento affronta il divario critico nella verifica formale (FV) assistita dall'IA per il software del mondo reale. Mentre le proposte di sicurezza dell'IA si affidano sempre più ad agenti autonomi per verificare formalmente il codice generato dall'IA, i benchmark attuali non riescono a supportare questo obiettivo. I benchmark esistenti (ad es., Minif2f, PutnamBench) si concentrano su problemi di olimpiadi matematiche o codice per dimostratori di teoremi scritto da esperti, che differisce significativamente dal "normale" panorama dell'ingegneria del software. Il software del mondo reale coinvolge complessi alberi di dipendenze, API esterne "black-box" e componenti scritti in linguaggi diversi, il che lo rende intrinsecamente più difficile da verificare rispetto ai sistemi monolitici e chiusi. Inoltre, vi è una mancanza di dataset di alta qualità e su larga scala derivati da codice scritto da ingegneri senza intento di verifica formale, necessari per addestrare agenti che possano operare "fuori distribuzione" (out-of-distribution) rispetto ai loro dati di addestramento.

Metodologia

Gli autori introducono FVSpec, una pipeline di generazione di benchmark che trasforma i Property-Based Tests (PBT) del mondo reale in sfide di verifica formale in Lean 4. Il processo prevede tre fasi principali:

1. Raccolta Dati (FVSpec:PBT):

   • Il team ha estratto 11.039 PBT unici da 333 repository Python open-source utilizzando il framework Hypothesis.
   • I repository sono stati filtrati per licenze permissive e i duplicati (inclusi i fork) sono stati rimossi per garantire la diversità.
   • Il corpus risultante rappresenta l'ingegneria del software "ordinaria", con test che variano da asserzioni banali a test multi-strategia complessi.

2. Traspilazione Agente-centrica (FVSpec:FV):

   • Una pipeline di LLM a tre agenti traduce i PBT Python e il relativo codice in Lean 4.
   • Scoperta delle Funzioni: Utilizza tree-sitter per estrarre la Funzione Sotto Test (FUT) e la sua chiusura transitiva di dipendenze locali.
   • Traduzione: Un agente di formalizzazione genera due file: Impl.lean (una versione computabile della funzione) e Spec.lean (enunciati di teoremi corrispondenti alle asserzioni dei PBT, con le prove lasciate come segnaposto sorry).
   • Riparazione Iterativa: La pipeline impiega un ciclo LSP (Language Server Protocol). Se il codice Lean generato non compila (tramite lake build), i diagnostici del compilatore vengono rimandati all'agente per la revisione. Questo ciclo può eseguire fino a 16 iterazioni.
   • Gestione degli Effetti: Per il codice che coinvolge effetti collaterali (ad es., Redis, I/O di file), l'agente axiomatizza questi sistemi esterni come interfacce non interpretate. I teoremi sono enunciati su questi assiomi, garantendo che l'obbligo di prova rimanga significativo rispetto alla logica del codice, anche se i dettagli concreti dell'implementazione vengono astratti.

3. Post-Produzione e Filtraggio:

   • I campioni generati sono sottoposti a una rigorosa validazione. I fallimenti sono categorizzati (ad es., timeout, discrepanze di tipo, identificatori sconosciuti).
   • Viene calcolato un punteggio di "fedeltà strutturale" basato su cinque sotto-metriche: copertura dei parametri, corrispondenza dei tipi, copertura delle strategie, copertura delle asserzioni e copertura delle dipendenze.
   • I campioni sono valutati per difficoltà (Facile/Difficile) utilizzando un giudice LLM calibrato (claude-haiku-4-5).
   • Il dataset finale mantiene diverse formalizzazioni per ogni PBT se nessun singolo tentativo domina sui parametri di qualità, risultando in 9.415 sfide derivate da 2.772 PBT unici.

Contributi Chiave

1. FVSpec:PBT: Un corpus di 11.039 PBT Python de-duplicati estratti da repository open-source, che rappresenta il primo dataset su larga scala e con licenza pulita di PBT provenienti dallo sviluppo software ordinario (escludendo la programmazione competitiva o codice ITP curato).
2. FVSpec:FV: Un dataset di 9.415 sfide di verifica formale in Lean 4. Ogni sfida include il codice Python originale, il PBT originale, un'implementazione in Lean e un teorema in Lean con obblighi di prova. Il dataset presenta una fedeltà strutturale mediana di 0,65, con il 62% delle sfide classificato come "difficile".
3. Valutazioni Baseline: Metriche di performance per modelli di frontiera (Claude Sonnet 4.6, Claude Opus 4.7 e GPT-5.4). I modelli hanno raggiunto un tasso di successo medio del 70% sui problemi "facili" e del 49% su quelli "difficili", indicando che il benchmark non è ancora saturo.
4. Rilascio Open Source: L'intera pipeline (scraper, estrattore di dipendenze, agente di formalizzazione e script) e i dataset sono rilasciati sotto una doppia licenza MIT/Apache.

Risultati

• Resa della Pipeline: La pipeline di traspilazione ha convertito con successo il 25% degli iniziali 11.039 PBT in sfide Lean valide (9.415 campioni).
• Metriche di Qualità: Il punteggio di fedeltà strutturale mediana è 0,65. La corrispondenza dei tipi (1,00) e la copertura delle asserzioni (0,97) sono alte, mentre la copertura dei parametri (0,24) e la copertura delle dipendenze (0,48) sono più basse, indicando aree in cui la fedeltà della traduzione varia.
• Performance dei Modelli: I modelli baseline hanno risolto il 70% dei campioni facili e il 49% di quelli difficili. I tassi di rifiuto sono stati bassi (4–8% per i facili, 3–25% per i difficili), suggerendo che i modelli tentano generalmente di eseguire i compiti.
• Complessità: Il campione mediano contiene 6 teoremi. Il dataset include una vasta gamma di complessità, dagli algoritmi di ordinamento semplici a complessi scheduler di job di workflow che coinvolgono timeout e transizioni di stato.

Significato e Rivendicazioni

Il documento afferma che FVSpec fornisce una base necessaria per far avanzare la verifica formale assistita dall'IA del software del mondo reale. A differenza dei benchmark precedenti che si affidano a prove scritte da esperti o problemi matematici, FVSpec deriva le specifiche da ingegneri che non avevano alcun intento di verifica formale. Ciò garantisce che i problemi siano "fuori distribuzione" rispetto ai dati di addestramento standard dei modelli, offrendo un test più rigoroso della capacità di generalizzazione di un agente.

Gli autori pongono questo lavoro come un passo verso la "IA sicura garantita" e la "Supervisione Formale Scalabile", dove gli agenti autonomi devono verificare il software con la stessa velocità ed efficacia con cui lo scrivono. Fornendo un benchmark su larga scala e realistico, FVSpec mira a guidare il progresso nell'addestramento di agenti capaci di gestire le complessità degli ecosistemi software moderni, incluse le dipendenze esterne e gli effetti collaterali, che vengono spesso ignorati nei benchmark sintetici. Il documento riconosce modestamente i limiti, come il potenziale dell'assiomatizzazione di mancare specifiche semantiche degli effetti collaterali e la mancanza di baseline di esperti umani per la calibrazione della difficoltà.