Sintesi Tecnica: Scalare l'Agentic Verifier per la Programmazione Competitiva

Definizione del Problema

Sebbene i Large Language Models (LLM) abbiano dimostrato forti capacità nella sintesi di programmi, essi incontrano spesso difficoltà nel risolvere correttamente problemi di programmazione competitiva in un unico tentativo. Una strategia comune per migliorare l'accuratezza è lo scaling al tempo di test (test-time scaling), dove vengono campionate molteplici soluzioni candidate e un verificatore seleziona la migliore.

I metodi di verifica esistenti affrontano limitazioni significative nel contesto della programmazione competitiva:

1. Generazione di Casi di Test Completi: Generare casi di test completi (input + output di verità fondamentale/ground-truth) è spesso difficile quanto risolvere il problema originale, rendendo il processo computazionalmente costoso e inaffidabile.
2. Esecuzione Basata Solo su Input: Approcci recenti generano solo input validi e selezionano le soluzioni basandosi sull'accordo degli output (voto). Tuttavia, questi metodi si affidano tipicamente al campionamento casuale di input.
3. Inefficienza del Campionamento Casuale: Lo spazio degli input validi nella programmazione competitiva è vastissimo, ma solo una piccola frazione è "discriminante" (ovvero, capace di esporre differenze comportamentali tra soluzioni corrette e errate). Gli esperimenti preliminari del paper dimostrano che scalare il numero di input casuali produce rendimenti decrescenti e non riesce a colmare il divario di prestazioni rispetto ai casi di test di verità fondamentale.

Metodologia: Agentic Verifier

Gli autori propongono l'Agentic Verifier, un agente basato su LLM progettato per ragionare attivamente sulle esecuzioni dei programmi e cercare input di test altamente discriminanti che espongano le discrepanze tra i candidati.

Meccanismo Core

Invece del campionamento casuale cieco, il verificatore intraprende un'interazione multi-turno con un ambiente di esecuzione del codice:

1. Formulazione del Task: Dato un problema $Q$ e una coppia di soluzioni candidate $(C_a, C_b)$, l'obiettivo dell'agente è generare un programma generatore di input $G$ che produca un input valido $x$ tale che $Exec(C_a, x) \neq Exec(C_b, x)$.
2. Ciclo di Interazione: L'agente propone iterativamente input, esegue le soluzioni candidate, ispeziona il feedback (errori di runtime, output) e affina le proprie ipotesi per scoprire controesempi.
3. Strategia di Selezione: Al tempo di inferenza, il verificatore addestrato genera input di test mirati per coppie di soluzioni candidate. Questi input vengono utilizzati in una strategia di voto basata sull'esecuzione per selezionare la soluzione finale.

Pipeline di Addestramento

Il verificatore viene addestrato tramite una pipeline scalabile in tre fasi:

1. Sintesi di Dati su Larga Scala: Gli autori costruiscono un dataset di problemi di programmazione competitiva con soluzioni etichettate. Per i problemi privi di casi di test di verità fondamentale, sintetizzano suite di test di alta qualità utilizzando un meccanismo di voto a maggioranza basato sul consenso tra più soluzioni di riferimento per garantirne l'affidabilità.
2. Rejection Fine-Tuning: Utilizzando un modello insegnante forte (Qwen3-235B), raccolgono traiettorie di interazione multi-turno di successo in cui l'agente riesce a generare input discriminanti. Il modello base viene sottoposto a fine-tuning su queste traiettorie di alta qualità, mascherando i prompt iniziali e il feedback per apprendere pattern di interazione efficaci.
3. Reinforcement Learning (RL) Agente-centrico: Il verificatore è ulteriormente ottimizzato tramite GRPO (Group Relative Policy Optimization). La funzione di ricompensa è sparsa e basata sull'esito:
   • $+1$: Input valido che distingue le due soluzioni.
   • $0$: Input valido che non distingue (le soluzioni concordano).
   • $-1$: Input non valido o generatore vuoto.
     Il curriculum di addestramento privilegia le coppie di "hard negative" dove gli input discriminanti sono rari, incoraggiando l'agente a imparare comportamenti di generazione mirati.

Contributi Chiave

1. Analisi Empirica: Il paper dimostra empiricamente che la generazione casuale di input è altamente inefficiente per la verifica basata sull'esecuzione di soli input, rivelando un sostanziale divario di prestazioni rispetto agli input di test discriminanti.
2. Agentic Verifier: Introduzione di un agente che genera attivamente input di test altamente discriminanti attraverso l'interazione multi-turno, andando oltre il campionamento statico o casuale.
3. Pipeline di Addestramento Scalabile: Una nuova pipeline che combina sintesi di dati, rejection fine-tuning e reinforcement learning agente-centrico per addestrare il verificatore.
4. Scaling al Tempo di Test: Dimostrazione che il metodo proposto beneficia continuamente dell'aumento del calcolo al tempo di test, scalando efficacemente sia con il numero di soluzioni candidate che con il numero di input generati.

Risultati Sperimentali

L'approccio è stato valutato su cinque benchmark di programmazione competitiva (USACO, LiveCodeBench, OJBench, ICPC-Eval e un nuovo benchmark CodeForces) utilizzando due modelli di policy (Qwen3-30B e Qwen3-235B).

• Guadagni di Performance: L'Agentic Verifier ha superato costantemente i baseline forti, inclusa la generazione casuale di input, la generazione di casi di test tramite modello (CodeT, CodeRM) e la selezione basata su reward-model.
  • Ha ottenuto guadagni assoluti di +10–15% nella precisione Best@k rispetto ai forti baseline basati sull'esecuzione.
  • Sul subset "Hard" di OJBench, il verificatore addestrato da 30B ha migliorato le prestazioni di +34.1% rispetto al baseline, superando significativamente un modello zero-shot da 235B.
• Comportamento di Scaling: A differenza dei baseline che mostravano una saturazione precoce, l'Agentic Verifier ha mostrato un chiaro comportamento di scaling al tempo di test, con le prestazioni che migliorano costantemente all'aumentare del numero di input di test.
• Zero-Shot vs. Addestrato: I modelli LLM zero-shot hanno fornito un certo miglioramento, ma il verificatore addestrato specificamente sul task ha superato significativamente i modelli zero-shot, anche quando il modello addestrato era 7 volte più piccolo del corrispondente zero-shot.

Significato e Rivendicazioni

Il paper sostiene che l'efficacia della votazione basata sull'esecuzione è determinata principalmente dalla qualità discriminante degli input di test piuttosto che sulla loro mera quantità.

Oltre a migliorare la selezione Best-of-N, gli autori evidenziano un'implicazione più ampia: le suite di test dei benchmark sono verificatori imperfetti. Le suite di test fissi coprono solo una parte limitata dello spazio degli input validi, portando a falsi positivi in cui soluzioni errate superano tutti i test del benchmark. L'Agentic Verifier può esporre attivamente questi fallimenti scoprendo controesempi mirati. Pertanto, gli autori posizionano il verificatore non solo come uno strumento di reranking, ma come un meccanismo complementare di controllo della correttezza in grado di espandere la copertura degli input e mitigare il rumore indotto dai benchmark nella valutazione del codice su larga scala.