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

Resumen Técnico: ExecVerify

1. El Problema

Los Grandes Modelos de Lenguaje (LLMs) para código, especialmente los modelos de tamaño pequeño (ej. 7B), enfrentan dificultades significativas para realizar razonamiento sobre la ejecución de código. Aunque existen métodos previos que utilizan Fine-Tuning Supervisado (SFT) con explicaciones generadas por un "maestro" (en forma de cadenas de entrada-salida o descripciones de trazas de ejecución en lenguaje natural), estos enfoques tienen limitaciones críticas:

• Falta de verificación explícita: Durante el SFT, los pasos intermedios de ejecución no se verifican explícitamente. El objetivo de entrenamiento se reduce a imitar el texto del maestro, lo que puede llevar a que el modelo memorice explicaciones sin comprender realmente la lógica de ejecución (alucinando pasos que no ocurren).
• Datos no controlados: Los datos de entrenamiento suelen recopilarse pasivamente o generarse sin control sobre la dificultad, resultando en ejemplos triviales o irresolubles, careciendo de un currículo de aprendizaje estructurado.
• Generalización limitada: Los modelos entrenados solo con SFT muestran poca capacidad de generalización a tareas complejas de generación de código.

2. Metodología: El Framework ExecVerify

Los autores proponen ExecVerify, un marco de post-entrenamiento que combina Síntesis de Datos Basada en Restricciones y Aprendizaje por Refuerzo (RL) de Caja Blanca (White-Box). El enfoque consta de dos componentes principales:

A. Síntesis de Datos Basada en Restricciones
Para superar la falta de control en los datos existentes, los autores construyen un dataset curricular con múltiples niveles de dificultad:

1. Restricciones Estructurales: Se iteran sobre tipos y métodos integrados de Python. Se aplican restricciones estrictas para generar código que requiera llamadas anidadas a métodos y estructuras de control complejas (bucles for/while, condicionales if anidados).
2. Síntesis de Entradas: Se generan entradas diversas para cada fragmento de código mediante mutaciones conscientes de los tipos.
3. Filtrado por Dificultad: Se ejecutan los programas sintetizados y se filtran los ejemplos. Se retienen únicamente aquellos que son no triviales pero resolubles para modelos pequeños (evaluados mediante un modelo de 7B), descartando los demasiado fáciles o imposibles. Esto crea un dataset de ~119k ejemplos de alta calidad.

B. Entrenamiento en Dos Etapas con RL de Caja Blanca
El proceso de entrenamiento se divide en dos etapas secuenciales:

• Etapa I: RL de Caja Blanca para Razonamiento de Código

  • Objetivo: Mejorar la capacidad de razonamiento sobre el estado intermedio de la ejecución.
  • Mecanismo: En lugar de solo predecir la salida final, el modelo debe responder preguntas verificables derivadas de la traza de ejecución real (obtenida mediante un intérprete).
  • Tipos de Preguntas (Recompensas):
    1. Control de Flujo: ¿Qué línea de código se ejecutará a continuación?
    2. Flujo de Datos: ¿Cuál es el valor y el tipo de una variable específica después de ejecutar una línea?
  • Función de Recompensa: Se combina la corrección de la entrada-salida final ($R_{I/O}$) con la precisión en las preguntas de caja blanca ($R_{white}$). La recompensa total es $R = 2 \cdot ((1-\alpha)R_{I/O} + \alpha R_{white})$. Esto obliga al modelo a entender la semántica paso a paso, no solo a imitar texto.

• Etapa II: RL para Generación de Código

  • Objetivo: Transferir las habilidades de razonamiento adquiridas a la generación de código funcional.
  • Mecanismo: Se utiliza RL con recompensas basadas en pruebas unitarias (pass@1 en benchmarks estándar). El modelo, ya fortalecido en razonamiento, aprende a generar código que pasa las pruebas funcionales.

3. Contribuciones Clave

1. Recompensas Verificables Paso a Paso: Introducen un paradigma de "Caja Blanca" donde las recompensas de RL se derivan directamente de la ejecución real del código (trazas), verificando explícitamente el control de flujo y los estados de las variables, a diferencia de los métodos anteriores que solo verifican la salida final o imitan explicaciones textuales.
2. Dataset Curricular Sintetizado: Desarrollan una pipeline de síntesis de datos activa con restricciones estructurales y filtrado por dificultad, asegurando un equilibrio óptimo entre complejidad y solvabilidad para modelos pequeños.
3. Pipeline de Post-Entrenamiento Eficaz: Demuestran que un enfoque de dos etapas (primero razonamiento con recompensas densas, luego generación con pruebas unitarias) supera significativamente a los métodos de SFT y RL tradicionales.

4. Resultados Experimentales

Los experimentos se realizaron principalmente con el modelo base Qwen2.5-Coder-7B-Instruct:

• Razonamiento de Código:
  • El modelo de 7B entrenado con ExecVerify alcanza un rendimiento comparable al modelo Qwen2.5-Coder-32B en benchmarks de razonamiento como CRUXEval, LiveCodeBench-Exec y REval.
  • Logra un aumento promedio de +20.0 puntos en comparación con el modelo base, superando a otros modelos de 7B entrenados con SFT o RL de entrada-salida (I/O).
• Generación de Código:
  • Tras la segunda etapa de entrenamiento, el modelo mejora el pass@1 en tareas de generación (EvalPlus, LiveCodeBench, BigCodeBench) hasta en un 5.9% en comparación con baselines fuertes de post-entrenamiento.
  • La transferencia de conocimiento es clara: el razonamiento fino adquirido en la Etapa I mejora directamente la capacidad de generar código lógico y correcto.
• Generalización:
  • Multi-idioma: El modelo muestra mejoras consistentes en tareas de razonamiento en otros lenguajes (Java, C++, Go, etc.) en CRUXEval-X, a pesar de haber sido entrenado principalmente en Python.
  • Tamaño del Modelo: Las mejoras se observan también en arquitecturas más pequeñas (3B) y diferentes familias (Llama3), indicando que el método es robusto y escalable.
• Eficiencia de Datos: El dataset sintetizado por ExecVerify supera a datasets existentes (como PYX-Sub o CodeI/O-Sub) incluso cuando se utiliza el mismo volumen de datos de entrenamiento (15k ejemplos).

5. Significado e Impacto

El trabajo ExecVerify representa un avance significativo en la capacidad de los LLMs para entender la ejecución de programas:

• Cambio de Paradigma: Pasa de la "imitación de texto" (SFT) a la "comprensión semántica verificable" mediante RL de caja blanca.
• Superación de la Barrera de Tamaño: Demuestra que un modelo pequeño (7B) puede igualar el rendimiento de razonamiento de modelos mucho más grandes (32B) si se entrena con señales de recompensa densas y verificables sobre la ejecución real.
• Fundamento para la Generación: Establece que el razonamiento de ejecución profundo es un prerrequisito esencial para la generación de código robusta, resolviendo errores lógicos sutiles que los métodos superficiales no detectan.

En conclusión, ExecVerify ofrece una solución técnica sólida para mejorar la fiabilidad y la capacidad de razonamiento de los modelos de código, utilizando una combinación de síntesis de datos controlada y recompensas de RL basadas en la ejecución real.