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

Resumo Técnico: ExecVerify

1. O Problema

Os Grandes Modelos de Linguagem (LLMs) focados em código ainda enfrentam dificuldades significativas no raciocínio sobre a execução de código, especialmente em modelos de menor porte (ex: 7B parâmetros). As limitações principais identificadas são:

• Falha na Compreensão Semântica: Os modelos tendem a memorizar padrões de texto em vez de simular a execução real do programa.
• Limitações do SFT (Fine-tuning Supervisionado): Métodos existentes dependem de SFT com explicações geradas por um "professor" (teacher). Isso cria um objetivo de treinamento que se resume a imitar o texto do professor, sem verificar explicitamente se os passos intermediários de execução (como valores de variáveis ou fluxo de controle) estão corretos.
• Falta de Controle na Dificuldade dos Dados: Os dados de treinamento são frequentemente coletados passivamente, resultando em exemplos triviais ou insolúveis, sem um currículo estruturado de aprendizado.

2. Metodologia: ExecVerify

O ExecVerify é um framework de pós-treinamento que combina Síntese de Dados Baseada em Restrições e Aprendizado por Reforço (RL) de Caixa Branca (White-Box). O objetivo é alinhar o treinamento com a correção semântica em cada etapa da execução, e não apenas na saída final.

O processo divide-se em três componentes principais:

A. Síntese de Dados Baseada em Restrições (Constraint-Based Data Synthesis)
Para criar um conjunto de dados de alta qualidade e com níveis variados de dificuldade:

• Restrições Estruturais: O sistema itera sobre tipos e métodos nativos do Python, gerando código que deve conter chamadas aninhadas e padrões específicos de fluxo de controle (loops for, while, condicionais if).
• Síntese de Entradas: Gera múltiplas entradas válidas para cada snippet de código, incluindo mutações baseadas em tipos para testar robustez.
• Filtragem por Dificuldade: Executa os programas sintetizados e filtra os dados. Mantém apenas instâncias que são não triviais (modelos pequenos falham frequentemente) mas solúveis (modelos fortes conseguem resolver), criando um "currículo" de aprendizado.

B. Treinamento em Duas Etapas (Two-Stage Post-Training)

1. Etapa I: RL de Caixa Branca para Raciocínio de Código

   • Warm-up SFT: Um breve ajuste supervisionado com cadeias de raciocínio I/O (Input-Output) para injetar padrões básicos.
   • Recompensas de Caixa Branca (White-Box Rewards): Diferente do RL tradicional que recompensa apenas a saída final, o ExecVerify utiliza o trace (rastro) do interpretador para gerar perguntas verificáveis sobre:
     • Fluxo de Controle: Qual linha será executada a seguir?
     • Fluxo de Dados: Qual é o valor e o tipo de uma variável após uma linha específica?
   • Função de Recompensa: Combina a precisão da saída final (I/O) com a precisão das previsões dos passos intermediários. Se o modelo acertar o valor de uma variável ou o próximo comando, recebe uma recompensa explícita. Isso força o modelo a "simular" o código internamente.

2. Etapa II: RL para Geração de Código

   • Uma vez que o modelo adquiriu habilidades de raciocínio de execução, ele é adaptado para a tarefa de geração de código.
   • Utiliza recompensas baseadas em testes unitários (pass/fail) para garantir que o código gerado seja funcionalmente correto.
   • A premissa é que o raciocínio de execução refinado na Etapa I transfere-se para uma geração de código mais robusta.

3. Contribuições Principais

• Mudança de Paradigma de Treinamento: Transição da imitação de texto (SFT) para a verificação semântica passo a passo via RL de caixa branca.
• Dataset Curricular Sintético: Criação de um dataset com 119k+ exemplos sintetizados, filtrados por dificuldade e diversidade estrutural, superando a qualidade de dados passivos existentes.
• Recompensas Verificáveis: Introdução de um mecanismo onde o interpretador valida as previsões do modelo sobre o estado interno do programa (variáveis e controle), fornecendo sinais de recompensa densos e precisos.
• Pipeline de Transferência Eficiente: Demonstração de que melhorar o raciocínio de execução primeiro resulta em ganhos significativos na geração de código posterior.

4. Resultados Experimentais

Os experimentos foram conduzidos utilizando o modelo base Qwen2.5-Coder-7B-Instruct.

• Raciocínio de Código (Code Reasoning):

  • O modelo de 7B treinado com ExecVerify alcançou desempenho comparável a modelos muito maiores (ex: Qwen2.5-Coder-32B).
  • Em benchmarks como CRUXEval, LiveCodeBench-Exec e REval, o modelo obteve uma melhoria média de +20.0 pontos em relação à base, atingindo uma pontuação média de 80.8 (vs 77.9 do modelo de 32B).
  • Mostrou generalização multilingue (Java, C++, etc.) no benchmark CRUXEval-X.

• Geração de Código (Code Generation):

  • Após a Etapa II, o modelo superou as linhas de base de pós-treinamento em benchmarks padrão (HumanEval, MBPP, LiveCodeBench, BigCodeBench).
  • Houve uma melhoria de até 5.9% no métrico pass@1 em comparação com baselines fortes de RL puro.
  • A ablação mostrou que o conhecimento de execução de "caixa branca" é transferível e essencial para lidar com restrições lógicas sutis que modelos treinados apenas com I/O falham em capturar.

• Eficiência de Dados:

  • O dataset sintetizado pelo ExecVerify demonstrou superior eficiência de dados, superando conjuntos de dados existentes (como PYX-Sub e CodeI/O-Sub) mesmo com o mesmo volume de treinamento (15k exemplos).

5. Significado e Impacto

O trabalho ExecVerify demonstra que a capacidade de raciocínio de execução em LLMs de código não precisa depender exclusivamente do aumento do tamanho do modelo (scaling laws), mas pode ser drasticamente melhorada através de:

1. Dados Sintéticos de Alta Qualidade: Com controle rigoroso sobre a estrutura e dificuldade.
2. Feedback Semântico Direto: Utilizando o interpretador como "verificador de verdade" para recompensar a compreensão interna do programa, não apenas a saída final.

Isso sugere um caminho viável para tornar modelos menores (7B-14B) altamente competitivos em tarefas complexas de engenharia de software, reduzindo a dependência de modelos massivos e caros para tarefas que exigem lógica de execução precisa. O código, dados e modelos foram disponibilizados publicamente.