Benchmark Vero de Berkeley: en el mejor de los casos, solo 27 de 43 proyectos resueltos

El laboratorio RDI de la Universidad de California en Berkeley publicó un benchmark llamado Vero. Exige que los agentes de IA hagan, a escala de todo un repositorio, dos cosas a la vez: implementar cada API requerida y demostrar que cada especificación dada es válida, manteniendo siempre coherentes el código, la prueba y la compilación. Los benchmarks anteriores de verificación formal básicamente se quedaban en el nivel de un solo teorema o función; este es el primero a nivel de repositorio.

El enunciado consiste en 43 proyectos Lean 4 multimódulo, portados desde código existente en Python, Dafny, Verus y Coq, que cubren en total 743 API y 2.705 especificaciones formales. La evaluación se ejecuta en dos modos: en el modo solo prueba se entrega una implementación de referencia y el agente solo debe probarla; en el modo código y prueba, el agente debe escribir su propia implementación y luego demostrar que satisface la especificación.

Tabla de puntuación

Número de instancias resueltas por completo (de un total de 43) con un presupuesto de 90 minutos:

Vale la pena fijarse en la brecha entre la primera y la tercera fila: con el mismo GPT-5.5 y el mismo Codex, solo con subir el nivel de razonamiento de medium a xhigh, la puntuación en el modo código y prueba salta de 2 a 27. En este tipo de tareas, el rendimiento marginal del presupuesto de razonamiento está lejos de saturarse.

Lo difícil no está en probar una especificación aislada

La fila superior aporta otro conjunto de cifras. GPT-5.5 (xhigh) aprueba el 87,3% de las especificaciones individuales en el modo código y prueba, y el 85,8% en el modo solo prueba, pero, según el criterio de 'instancia totalmente resuelta', solo quedan 27/43 y 25/43. El juicio de los investigadores es claro: demostrar cada especificación aislada ya no es el punto difícil; lo difícil es mantener coherente todo el repositorio de pruebas.

La diferencia entre estas dos cifras tiene implicaciones de ingeniería reales. Una tasa de acierto del 87% por especificación, extrapolada a un proyecto con decenas de especificaciones, significa que casi todos los proyectos se quedarán atascados en algunas de ellas. Y la verificación formal es de todo o nada: si queda una sola especificación sin demostrar, todo el repositorio no compila, y las partes ya demostradas correctamente no reciben ningún crédito parcial. Esto es completamente distinto de un proyecto que, con un 87% de pruebas unitarias superadas, aún puede salir a producción.

Otro detalle está en la composición del código de prueba. En las ejecuciones resueltas por completo, los lemas auxiliares representan una mediana del 73,6% del código de prueba. Es decir, tres cuartas partes de lo que escriben los agentes es andamiaje levantado sobre la marcha para sostener la prueba principal. Esta proporción sugiere que los modelos actuales siguen una vía de amplitud, apilando lemas a la fuerza en lugar de encontrar una estructura de prueba concisa.

Elegir el propio algoritmo: ayudó 5 veces, perjudicó 17

El modo código y prueba le da al agente un grado de libertad: como puede escribir la implementación por sí mismo, también puede elegir un algoritmo más fácil de probar. Los investigadores midieron el efecto neto de esta libertad y, en comparaciones pareadas, 5 casos tuvieron éxito gracias al cambio de algoritmo, mientras que 17 fracasaron por esa misma razón.

Ese 5 contra 17 dice bastante. En teoría, poder elegir la propia implementación solo debería ayudar; en el peor de los casos, bastaría con copiar la implementación de referencia. En la práctica, el modelo a menudo elige una versión que considera 'ingeniosa' pero que resulta más difícil de probar, y termina atascado dentro de los 90 minutos. Saber escribir código y saber qué código es fácil de probar son dos capacidades distintas, y los agentes actuales solo dominan la primera.

El ranking deja además una nota: de las 43 instancias, 10 nunca fueron resueltas por ninguna configuración, en ninguno de los dos modos. Este conjunto constituye el techo rígido actual del método y también el punto en el que más debería concentrarse la siguiente ronda de trabajo.

Para quienes construyen herramientas de programación con IA, el valor de referencia de Vero no está en el ranking, sino en que convierte la 'coherencia a nivel de repositorio' —algo que antes solo se percibía por experiencia— en una métrica medible. Los benchmarks del tipo SWE-bench evalúan si se puede corregir correctamente un único error; Vero evalúa si se puede soportar el conjunto completo de restricciones de un proyecto de ingeniería. Ambas dificultades no están en el mismo nivel.

Fuentes: blog público del laboratorio RDI de Berkeley, CocoLoop; el tamaño del benchmark, el número de instancias resueltas por completo en ambos modos, la tasa de acierto por especificación, la proporción de lemas auxiliares y las estadísticas de comparación pareada se verificaron conforme al informe público.