“El desarrollo de las matemáticas hacia una mayor precisión ha llevado, como es bien sabido, a la formalización de grandes extensiones de ellas, de modo que uno puede demostrar cualquier teorema utilizando nada más que unas pocas reglas mecánicas”.
— K. Gödel
En la Parte 1, construimos un verificador de pruebas y desarrollamos un modelo mental de por qué deberíamos confiar en las pruebas que surgen de un LLM: siempre que tengamos un razonamiento formalizado y un verificador sólido, todo lo que necesitamos es unas “algunas reglas mecánicas”. Entonces, ¿cómo capacitamos a un LLM para que genere pruebas válidas?
Como lo demostró maravillosamente DeepSeek, la misma intuición detrás de la IA que aprende el juego de Go funciona para que la IA aprenda a razonar, siempre que se pueda verificar el razonamiento (y ahora sabemos que se puede). En esta segunda parte, le damos un buen uso a nuestro verificador y creamos un bucle de entrenamiento de RL de extremo a extremo para ajustar un modelo de código abierto para producir pruebas en el lenguaje que presentamos en la parte 1: de un vistazo, la siguiente figura muestra los ingredientes básicos del flujo.
TL; DR: después de una colaboración entre máquinas y humanos para generar un conjunto de datos (aprovechando nuestro verificador como una verificación de cordura en ejemplos generados por LLM), ejecutamos en Tinker un bucle RL para realizar ajustes finos al estilo LoRA de modelos de código abierto. Le indicamos al modelo (1) cómo funciona nuestro lenguaje, (2) cómo aplicar reglas para crear pruebas y (3) cómo formatear las respuestas para que sean fáciles de analizar. Luego, cada prueba se ejecuta a través del verificador de pruebas y la recompensa se propaga hacia atrás para mejorar las capacidades del modelo: idealmente, el modelo comenzará con intentos de prueba en su mayoría fallidos y luego mejorará progresivamente a medida que avanza el entrenamiento.
Tenga en cuenta que, si bien la serie se centra específicamente en el razonamiento matemático, las pruebas verificables son fundamentales para generar confianza en los sistemas de software distribuido. Como argumentaron algunos expertos, la IA bien puede ser el ingrediente que falta para demostrar la corrección del software a escala.
Abróchese el cinturón, clone el repositorio y codifique. Si te saltaste la primera parte, ¡puedes leerla aquí!
Generación de conjuntos de datos
“La gente piensa que las matemáticas son complicadas. Las matemáticas son la parte simple. Son las cosas que podemos entender. Son los gatos los que son complicados”. — J. Conway
Para obtener una recompensa por mejorar nuestro modelo, necesitamos ejemplos de pruebas en primer lugar: idealmente, nos gustaría una combinación de pruebas fáciles y concretas, escritas en nuestro propio lenguaje de razonamiento. ¡No podemos simplemente generar cadenas aleatorias en nuestro alfabeto porque nos gustaría que el modelo intente probar cosas que sabemos que son demostrables en primer lugar! ¿Cómo iniciamos el proceso?
Nuestra combinación de entrenamiento es una combinación de tres fuentes:
Una traducción manual de ejercicios (premisas->conclusión) tomados de forallx, que asumimos que son pruebas solucionables; Una traducción manual de ejercicios (premisas->conclusión) tomados de Lenguaje, Prueba y Lógica, que asumimos que son pruebas solucionables; Un corpus de pruebas generado por un potente LLM (Sonnet by Anthropic). Dado que no podemos asumir que las tuplas de premisas->conclusión generadas por el LLM sean correctas, solicitamos al LLM que genere una prueba completa, que (¡lo adivinaste!) es verificada por nuestro verificador de pruebas antes de agregarla al conjunto de capacitación.
Una sola observación en el conjunto de datos se parece al siguiente objeto:
{“instalaciones”: [“P”, “Q”]”conclusión”: “P y Q”, “num_steps”: 1}
es decir, un conjunto de premisas, una conclusión y cuántos pasos tomó Sonnet para generar una prueba válida: las premisas y la conclusión terminarán en el mensaje durante RL (ya que le pediremos al modelo que encuentre una prueba de la conclusión a partir de las premisas), y num_steps es un valor conveniente para imprimir algunas estadísticas sobre la dificultad percibida del conjunto de entrenamiento (asumiendo por simplicidad que la duración de una prueba se correlaciona vagamente con su dificultad).
Aprendizaje por refuerzo en Tinker
“La mejor manera de tener una buena idea es tener muchas ideas”.
– atribuido a L. “
Ahora estamos listos para obtener nuestro propio LLM, más pequeño y de código abierto, para Vibe Proving. Hay muchas recetas y servicios en línea para realizar RL en modelos de código abierto, pero elegimos a Tinker porque promete abstraer la infraestructura y la mayor parte del texto estándar requerido (también es el nuevo chico de la cuadra, por lo que es una oportunidad para probarlo).
El ciclo de entrenamiento en sí no tiene muchas sorpresas:
Ejemplo: dada la indicación y una tupla (premisas->conclusión), le pedimos al modelo que genere múltiples intentos de prueba. Verificar: pasamos cada intento por el verificador de pruebas. Recompensa: las pruebas válidas (es decir, pruebas que son completamente analizables y lógicamente correctas) obtienen una recompensa 1, todos los demás resultados obtienen 0 (“Hacer o no hacer”, de hecho). Tenga en cuenta que también verificamos que la prueba generada tenga la misma (premisas->conclusión) que nuestra solicitud, para evitar que el LLM engañe fácilmente al sistema al producir siempre una prueba trivialmente correcta. Actualización: ajustamos los pesos del modelo para que las pruebas exitosas sean más probables.
Siguiendo las propias pautas de Tinker, elegimos experimentar con modelos de razonamiento MoE en algunos tamaños: gpt-oss-20b, gpt-oss-120b y Qwen3-30B-A3B-Instruct-2507. Durante la capacitación, los registros y las pruebas se almacenan en la carpeta Training_logs: al final, nuestra aplicación (¡codificada con vibración!) se puede utilizar para visualizar las tendencias métricas e inspeccionar las pruebas generadas.
Si está utilizando un asistente de inteligencia artificial para monitorear el entrenamiento (con el que experimenté por primera vez en este proyecto), una porción de datos interesante para rastrear son las pruebas de los libros de texto, ya que están diseñadas para ser complicadas. Como ejemplo, la siguiente es una actualización de estado de Claude Code:
¿Qué tan buena está demostrando nuestra vibra?
Después de algunas ejecuciones y un poco de retoque con los parámetros, siempre terminamos con modelos que pueden probar la mayoría de los ejemplos generados, pero tienen dificultades en algunas pruebas de libros de texto. Es instructivo y un poco divertido inspeccionar las pruebas generadas.
Desde el punto de vista del éxito, se trata de un intento de demostrar la ley de DeMorgan, es decir, mostrar cómo pasar de [‘not A or not B’] no (A y B), suponiendo primero A y B y demostrando una contradicción:
ni A ni B (premisa) | A y B (subprueba) | Un (2) | B (2) || no A (subprueba anidada, de 1) || ~ (3,5) || no B (subprueba anidada) || ~ (4,7) | (1, 5-6, 7-8) QED
En el lado del fracaso, ningún modelo demostró con éxito desde ‘A o B’, ‘no A o C’, ‘no B o D’ que C o D , luchando por gestionar adecuadamente las subpruebas anidadas y aplicar la regla de explosión, como se muestra en este rastro:
A o B (premisa) no A o C (premisa) no B o D (premisa) | A (subprueba) || no A (subprueba anidada) || ~ (4,5) | C (5-6) ← ERROR….
¿Qué tan fácil fue Tinker?
Nuestra pequeña prueba de concepto no es una prueba de estrés para un servicio de capacitación a escala, pero fue suficiente para obtener algunas impresiones fundamentadas del sistema.
La combinación de buenos ejemplos públicos, documentación compatible con Claude y abstracción de hardware dio como resultado una introducción agradable y suave a RL, a un costo razonable (todos los experimentos para la publicación del blog costaron aproximadamente $60, incluidas las ejecuciones iniciales que, en retrospectiva, ¡fueron obviamente una pérdida de tiempo y dinero!).
Cuando lo dominas y comienzas a ejecutar algunos trabajos en paralelo, la falta de monitoreo y observabilidad se convierte en un problema: a veces mis ejecuciones se ralentizaron significativamente (obtuve respuestas try_again durante mucho tiempo, como si el sistema estuviera sobrecargado), y algunos trabajos fallaron en algún momento por razones poco claras (pero, efectivamente, puedes reiniciar desde un punto de control anterior). Teniendo en cuenta el precio razonable y la naturaleza prototipo de mis cargas de trabajo, ninguno de estos problemas superó a los profesionales, y me fui con una experiencia Tinker lo suficientemente positiva como para que definitivamente la usaría nuevamente para un proyecto futuro.
¡Nos vemos, vaqueros de RL!
“Hacemos estas cosas no porque sean fáciles, sino porque pensamos que iban a ser fáciles”. – Anónimo
Si bien Tinker hace que el proceso de capacitación (en su mayor parte) sea fluido, el diablo todavía está en los detalles (RL): apenas hemos arañado la superficie hasta ahora, ya que nuestro objetivo era pasar de cero a una pila de Vibe Proving, sin optimizar RL per se.
La buena noticia es que el flujo es bastante modular, por lo que todos los componentes se pueden mejorar y modificar (más o menos) de forma independiente:
elección de modelo: tipo de modelo, tamaño de modelo, proveedor… parámetros de entrenamiento: elegir tasa de aprendizaje, tamaño de lote, rango LoRA… abstracciones de código: reescribir el código con RL Envs… optimización rápida: mejores instrucciones, formato más fácil, ejemplos útiles en contexto,… optimización de conjuntos de datos: ejemplos más diversos, aprendizaje del plan de estudios (no solo variando la dificultad de la prueba, sino por ejemplo comenzando con pruebas que se realizan excepto por un paso faltante, luego pruebas con dos pasos faltantes, etc. hasta que el modelo necesita completar toda la prueba)…
Del mismo modo, nuestro propio lenguaje de prueba personalizado definitivamente no es suficiente para obtener resultados interesantes: podríamos mejorarlo, pero llegar a algo utilizable en realidad requeriría una asombrosa cantidad de trabajo. Por estas razones, es mejor migrar a un lenguaje diseñado específicamente, como Lean: lo que es más importante, ahora que conoce las pruebas como razonamiento formalizado, el mismo modelo mental se traslada a un lenguaje que es (mucho) más expresivo. Además, Lean tiene prácticamente el mismo estilo para escribir pruebas, es decir, reglas para introducir y eliminar operadores lógicos.
En otras palabras, una vez que logramos entender las matemáticas detrás de Vibe Proving y construimos un arnés RL inicial, lo que queda es buena ingeniería.
Expresiones de gratitud
Gracias a Patrick John Chia, Federico Bianchi, Ethan Rosenthal, Ryan Vilim y Davis Treybig por sus valiosos comentarios sobre versiones anteriores de este borrador.
Si le gusta la intersección de genAI, el razonamiento sobre sistemas distribuidos y la verificación, también puede consultar nuestra investigación en Bauplan.
Se utilizaron asistentes de codificación de IA para escribir el repositorio complementario, pero no se utilizó ningún asistente para escribir el texto (a menos que fuera para la revisión y la corrección de errores tipográficos).