s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

1. Il Problema

Nonostante i recenti successi degli approcci neuro-simbolici (che combinano Large Language Models - LLM - e metodi formali) su benchmark matematici orientati alle competizioni (come MiniF2F o PutnamBench), esiste un divario significativo: la capacità di risolvere problemi matematici astratti non garantisce la capacità di costruire prove formali per implementazioni reali di codice a basso livello.

I benchmark attuali mancano di scenari che richiedano:

• Ragionamento consapevole dell'architettura hardware (ISA - Instruction Set Architecture).
• Gestione dello stato della memoria, aliasing e endianness.
• Verifica di routine crittografiche assembly (x86/ARM) che hanno conseguenze dirette sulla sicurezza e affidabilità dei sistemi.

Il paper identifica la necessità di un benchmark che valuti la sintesi di prove verificabili dalla macchina per librerie crittografiche industriali, andando oltre la matematica da competizione.

2. Metodologia e Costruzione del Benchmark

Gli autori hanno sviluppato s2n-bignum-bench, un benchmark derivato dalla libreria crittografica s2n-bignum utilizzata da AWS. Questa libreria contiene routine assembly ottimizzate per la crittografia, la cui correttezza è stata già verificata formalmente utilizzando HOL Light (un dimostratore di teoremi interattivo basato su logica del primo ordine di ordine superiore).

Caratteristiche principali della costruzione:

• Origine dei Dati: I problemi sono estratti dal repository open-source di s2n-bignum. Il benchmark include 2.284 obblighi di prova (proof obligations) isolati.
• Formato del Task: Ogni problema è strutturato come una "query in contesto". Viene fornito un file di setup (setup.ml) che carica le definizioni, le costanti e i risultati precedentemente provati necessari per ricreare l'ambiente originale, ma il corpo della prova originale è sostituito da un segnaposto (CHEAT TAC).
• Identificatori Unici: Ogni problema ha un ID univoco (es. arm.bignum_montsqr_p256.lemma1.0) per gestire le occorrenze multiple dello stesso nome di teorema.
• Categorizzazione: I problemi sono divisi in quattro categorie basate su euristiche leggere:
  1. Bit-vector lemmas (311)
  2. Program-state lemmas (552)
  3. Functional correctness (859, divisi in 437 ARM e 422 x86)
  4. Generic (562, fatti ausiliari)
• Pipeline di Valutazione Offline: Il sistema permette valutazioni completamente offline utilizzando gli artefatti forniti, garantendo riproducibilità.

3. Contributi Chiave

Il paper presenta quattro contributi principali:

1. Dataset Industriale: La pacchettizzazione di 2.284 obblighi di prova da una libreria crittografica di produzione in task isolati con identificatori stabili.
2. Pipeline End-to-End: Fornitura di uno strumento completo per costruire il benchmark, recuperare problemi selezionati ed eseguire valutazioni offline.
3. Meccanismi di Integrità e Sicurezza:
   • Rilevamento di sottomissioni non valide o non corrette (es. uso di CHEAT TAC, introduzione di nuovi assiomi tramite new_axiom).
   • Validazione a livello di parser per evitare iniezioni sintattiche complesse.
   • Meccanismo di Mitigazione della Contaminazione: Offuscamento delle annotazioni di tipo per impedire che i modelli memorizzino le dichiarazioni dei teoremi.
4. Focus su Ragionamento Low-Level: Il benchmark misura la capacità di ragionamento bit-preciso e consapevole dell'ISA, più vicino ai flussi di lavoro di verifica reali rispetto alla matematica astratta.

4. Risultati Sperimentali

Gli autori hanno condotto esperimenti preliminari utilizzando GPT-5.3-Codex (accessibile tramite codex-cli) come baseline.

• Configurazione: Modalità "zero-shot" con prompt che richiede esclusivamente un'espressione di tattica HOL Light, senza spiegazioni naturali.
• Performance:
  • Modalità "Medium-effort": Tasso di successo del 4,4% (101 prove su 2.284).
  • Modalità "High-effort": Tasso di successo del 5,3% (121 prove su 2.284).
• Analisi per Categoria:
  • Le prestazioni migliori si sono registrate nelle categorie Generic (11-12%) e Bit-vector (8-9%).
  • Le prestazioni sono state nulle (0,0%) per le categorie di correttezza funzionale su assembly ARM e x86 (fc arm e fc x86), evidenziando la difficoltà estrema dei modelli attuali nel ragionare su codice assembly crittografico complesso.
• Gestione dei Timeout: È stato implementato un sistema di timeout dinamico basato su profilazione delle prove originali (da pochi secondi a diverse ore) per evitare penalizzazioni ingiuste o spreco di risorse computazionali.

5. Significato e Implicazioni

Il lavoro di s2n-bignum-bench rappresenta un passo avanti significativo nella valutazione dei LLM per la verifica formale:

• Superamento della Matematica da Competizione: Sposta il focus da problemi matematici astratti a scenari di ingegneria reale con impatti sulla sicurezza.
• Verifica di Codice Assembly: È il primo benchmark pubblico focalizzato sulla sintesi di prove verificabili per routine assembly crittografiche industriali in HOL Light.
• Testbed per il Futuro: Fornisce un ambiente riproducibile e sicuro per testare l'evoluzione delle capacità di ragionamento strutturato degli LLM.
• Sviluppi Futuri: Sebbene la versione attuale si concentri sulla correttezza funzionale, il framework è progettato per estendersi in futuro a proprietà relazionali (come la disciplina del tempo costante e l'equivalenza tra routine ottimizzate e di verifica).

In sintesi, il paper evidenzia che, sebbene gli LLM stiano facendo progressi nella matematica formale, c'è ancora una grande distanza da colmare per applicarli con successo alla verifica di sistemi critici a basso livello, e fornisce gli strumenti necessari per misurare e guidare questo progresso.