ExecVerify: White-Box RL with Verifiable Stepwise Rewards for Code Execution Reasoning

1. Il Problema

I Large Language Models (LLM) per il codice, specialmente quelli di dimensioni ridotte (es. 7B), faticano a ragionare correttamente sul processo di esecuzione dei programmi. Le limitazioni attuali derivano da due fattori principali:

• Dipendenza dalla SFT (Supervised Fine-Tuning): I metodi esistenti si basano su spiegazioni generate da un "insegnante" (teacher-generated explanations) sotto forma di catene di ragionamento input-output o descrizioni in linguaggio naturale delle tracce di esecuzione. Tuttavia, durante l'addestramento SFT, i passaggi intermedi dell'esecuzione non vengono verificati esplicitamente. Il modello tende a imitare il testo del teacher senza comprendere realmente la semantica dell'esecuzione, portando a errori di logica e allucinazioni.
• Mancanza di controllo sulla difficoltà: I dati di addestramento sono spesso raccolti passivamente o generati senza un controllo strutturato sulla difficoltà, risultando in un mix di esempi banali o irrisolvibili, privi di un curriculum di apprendimento progressivo.

2. Metodologia: ExecVerify

Il paper introduce ExecVerify, un framework che supera la semplice imitazione testuale combinando Sintesi di Dati Basata su Vincoli e Reinforcement Learning (RL) a "Scatola Bianca" (White-Box).

A. Sintesi di Dati Basata su Vincoli (Constraint-Based Data Synthesis)

Per creare un dataset di alta qualità e strutturato, gli autori sintetizzano programmi Python seguendo un approccio curriculare:

1. Vincoli Strutturali: I modelli generano codice iterando su tipi e metodi built-in di Python, applicando vincoli espliciti come chiamate a metodi annidati e strutture di controllo (if/for/while) con profondità crescente.
2. Sintesi degli Input: Vengono generati input diversificati (inclusi input mutati) per testare il comportamento del programma.
3. Filtraggio per Difficoltà: I campioni vengono eseguiti e filtrati. Vengono mantenuti solo gli esempi che sono "non banali ma risolvibili" per modelli di piccole dimensioni (valutati tramite un modello teacher di 7B), scartando quelli troppo facili o impossibili.

B. Due Fasi di Post-Training

Il framework adotta una pipeline di addestramento in due stadi:

• Fase 1: RL a Scatola Bianca per il Ragionamento (White-Box RL for Code Reasoning)

  • Obiettivo: Rafforzare la capacità di tracciare lo stato di esecuzione (control flow e variabili).
  • Meccanismo: Invece di valutare solo l'output finale, il sistema esegue il codice in una sandbox e genera domande "white-box" verificabili basate sulla traccia di esecuzione reale. Queste domande chiedono al modello di prevedere:
    • La prossima istruzione eseguita (Control-flow).
    • Il valore e il tipo delle variabili dopo un'istruzione specifica (Data-flow).
  • Funzione di Ricompensa: Viene definita una ricompensa ibrida che combina la correttezza Input-Output ($R_{I/O}$) con l'accuratezza delle previsioni sugli stati intermedi ($R_{white}$). Questo sposta l'obiettivo da una semplice imitazione testuale alla comprensione semantica passo-passo.

• Fase 2: RL per la Generazione di Codice (RL for Code Generation)

  • Obiettivo: Trasferire le capacità di ragionamento acquisite alla generazione di codice funzionale.
  • Meccanismo: Il modello viene ulteriormente addestrato utilizzando ricompense basate sui test unitari (Unit-Test), guidandolo a generare codice che passi i test di validazione.

3. Contributi Chiave

1. Ricompense Verificabili Step-by-Step: A differenza dei metodi precedenti che usano spiegazioni testuali non verificabili, ExecVerify utilizza tracce di esecuzione reali per fornire segnali di ricompensa densi e verificabili su ogni passaggio intermedio.
2. Dataset Curriculare Sintetico: Creazione di un dataset sintetico con livelli di difficoltà controllati e diversità strutturale, superando i limiti dei dati raccolti passivamente.
3. Pipeline a Due Stadi: Dimostrazione che il potenziamento del ragionamento di esecuzione (Fase 1) precede e migliora significativamente le prestazioni nella generazione di codice (Fase 2).
4. Efficienza dei Dati: Il metodo dimostra che dati sintetici di alta qualità e difficoltà controllata sono più efficaci di grandi quantità di dati grezzi o di dataset esistenti (come SEMCODER o CODEI/O).

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un modello base Qwen2.5-Coder-7B-Instruct.

• Ragionamento sul Codice (Code Reasoning):
  • Il modello addestrato con ExecVerify ottiene risultati paragonabili a modelli molto più grandi (es. Qwen2.5-Coder-32B) su benchmark come CRUXEval, LiveCodeBench-Exec e REval.
  • Miglioramento medio del punteggio da 60.8 a 80.8 (+20 punti) rispetto al modello base, superando di gran lunga le varianti SFT o RL basate solo su Input-Output.
• Generazione di Codice (Code Generation):
  • Dopo la Fase 2, il modello supera i baseline di post-training forti su benchmark come EvalPlus, LiveCodeBench e BigCodeBench.
  • Si registra un miglioramento di pass@1 fino al 5.9% rispetto a baseline potenti.
• Generalizzazione:
  • I miglioramenti si trasferiscono efficacemente ad altre architetture (Llama3-8B) e dimensioni (3B).
  • Il modello mostra capacità di generalizzazione cross-linguistica (Java, C++, Go, ecc.) e su codice che utilizza librerie esterne.

5. Significato e Impatto

Il lavoro di ExecVerify segna un cambiamento di paradigma nell'addestramento di LLM per il codice:

• Dal Testo alla Semantica: Sposta il focus dall'imitazione di spiegazioni testuali (che possono essere superficiali) alla verifica rigorosa della logica di esecuzione interna.
• Scalabilità: Dimostra che modelli più piccoli (7B), se addestrati con segnali di ricompensa "white-box" e dati curati, possono competere con modelli molto più grandi (32B+) in compiti di ragionamento complesso.
• Fondamento per l'Affidabilità: Fornisce un approccio per ridurre le allucinazioni di codice, assicurando che il modello comprenda non solo cosa produce il codice, ma come viene eseguito, un passo cruciale per applicazioni di riparazione automatica e generazione di codice sicuro.

In sintesi, ExecVerify dimostra che l'integrazione di segnali di esecuzione verificabili nel ciclo di apprendimento per rinforzo è fondamentale per sviluppare modelli di codice capaci di un ragionamento profondo e affidabile.