“Lo que no puedo crear, no lo entiendo”
– atribuido a R. Feynman
Después de Vibe Coding, parece que hemos entrado en la era (muy especializada, pero mucho más genial) de Vibe Proving: DeepMind gana el oro en la Olimpiada Internacional de Matemáticas, Harmonic resuelve un problema no trivial en teoría de números y, por primera vez en la historia, los sistemas de IA parecen estar haciendo matemáticas serias.
Al mismo tiempo, se nos recuerda constantemente que los LLM alucinan: parece que tenemos una paradoja entre manos. Si los LLM pueden producir texto basura (incluidas las pruebas matemáticas) y razonamiento correcto (incluido el razonamiento matemático), ¿cómo podemos saber qué modelos completados son buenos y cuáles son alucinaciones?
La respuesta corta de LinkedIn es que utilizamos un LLM para generar razonamiento matemático y luego externalizamos nuestra confianza a un software especial que lo verifica. Pero esta breve respuesta plantea a su vez nuevas preguntas:
¿Cómo funciona este “software especial”? ¿Por qué confiamos en él? ¿Cómo capacitamos a un LLM para que lo utilice como pruebas?
Es tentador escribir artículos sobre grandes ideas como “LLM y matemáticas”, proporcionando respuestas intuitivas y no rigurosas en el entorno más general posible. A modo de ejemplo, así es como un nuevo libro intenta venderle toda la historia de “matemáticas y computadoras”:
El “oráculo de la verdad” que los pensadores han buscado durante siglos, una herramienta para verificar o refutar definitivamente cualquier afirmación matemática o lógica. (…) [El libro] ofrece una respuesta profunda a un misterio de larga data: ¿Pueden las computadoras revelar verdades universales?
Aquí haremos exactamente lo contrario. En lugar de palabras y analogías que suenen milagrosas, construiremos un sistema LLM para pruebas desde cero, con el objetivo de dar respuestas exactas para escenarios simples: ganamos en precisión, intercambiando algo de generalidad. En lugar de argumentos generales, nos esforzamos por crear guiones inspeccionables que funcionen con “pruebas” simples. Dividimos nuestra guía en dos partes, que también podrás disfrutar de forma independiente:
Parte 1 (ésta): comprender los verificadores y construir un modelo mental sólido de lo que hace que las matemáticas sean tan especiales (¿por qué no confiamos en los LLM que escriben leyes de la misma manera que lo hacemos con las pruebas?). Esto responderá las preguntas 1 y 2 anteriores; Parte 2 (próximamente): entrenar un LLM de código abierto para producir pruebas, utilizando nuestro verificador para proporcionar una señal de recompensa durante el aprendizaje por refuerzo. Esto responderá 3.
Por supuesto, uno podría reconstruir los conceptos básicos leyendo artículos en la frontera. Sin embargo, los informes de vanguardia suelen utilizar un lenguaje de propósito especial y están llenos de muchas otras consideraciones técnicas, lo que dificulta desenredar los componentes esenciales y construir un modelo mental inicial del espacio del problema.
Al crear un LLM para pruebas, obtenemos exposición directa a las ideas principales para que las exploraciones posteriores sean más fáciles: como no podemos responder todas las preguntas en línea, los seguimientos más avanzados se abordan en las preguntas frecuentes al final.
Ahora, abróchese el cinturón, clone el repositorio y codifique.
¿Qué significa que una prueba sea correcta?
“Arquímedes será recordado cuando Esquilo sea olvidado, porque las lenguas mueren y las ideas matemáticas no”
-GH Hardy
Los verificadores de pruebas son programas de software que toman como entrada el razonamiento matemático generado por un LLM y verifican que sea correcto. Esto es engañosamente simple: comprender qué significa "correcto" y cómo es posible establecer la corrección son la clave para construir un modelo mental preciso de cómo los estudiantes de maestría en maestría pueden tener tanto éxito en matemáticas.
Que las computadoras puedan verificar las matemáticas en general puede resultar sorprendente, pero todos estamos familiarizados con la aplicación mecánica de reglas matemáticas específicas. En la escuela secundaria aprendemos la regla para verificar que 2x es la derivada de x2 + 3; lo más importante es que es posible que no sepamos qué es una derivada, o qué significan esos símbolos, pero siempre que apliquemos la regla, podemos verificar la afirmación. En pocas palabras, lo que encontraremos hoy es que este fenómeno es mucho más general de lo que podríamos sospechar: el propio razonamiento matemático puede codificarse en símbolos y tratarse algorítmicamente.
Todo el mundo conoce el silogismo como un caso paradigmático de razonamiento correcto: “Todos los hombres son mortales; Sócrates es un hombre; luego Sócrates es mortal”. El estándar de corrección es la consecuencia lógica: un enunciado C es una consecuencia lógica de (necesariamente se deriva de) las premisas S₁, S₂… Sₖ si no es posible que S₁, S₂… Sₖ sean verdaderas y C sea falsa. En otras palabras, siempre que las premisas son verdaderas, la conclusión es necesariamente verdadera.
En casos simples, es fácil convencernos de que la conclusión se deriva de las premisas, pero ¿qué pasa con los más complejos? ¿Puedes “ver” inmediatamente que los números primos infinitos son una consecuencia lógica de la multiplicación y división básicas?
Las pruebas son una secuencia de enunciados, que comienzan con una o más premisas y terminan con una conclusión, de modo que cada enunciado se sigue necesariamente de las premisas y/o enunciados anteriores: el propósito de una prueba es mostrarnos exactamente cómo C se sigue de las premisas, procediendo paso a paso. Por ejemplo, podemos demostrar que hay infinitos números primos:
Supongamos, en aras de la contradicción, que sólo hay un número finito de números primos. Enumérelos todos: p₁, p₂,…, pₖ. Considere un nuevo número N = (p₁ × p₂ × … × pₖ) + 1. Entonces N es primo o compuesto; Si N es primo, entonces hemos encontrado un primo que no está en la lista original, contradiciendo la suposición de que p₁,…, pₖ eran todos primos. Si N es compuesto, debe tener un divisor primo q. Pero q no puede estar entre p₁,…, pₖ, porque al dividir N por cualquier p queda el resto 1. Así que nuevamente hemos encontrado un primo que no está en la lista original, q. En ambos casos contradecimos la suposición de que sólo había un número finito de números primos. Por tanto, debe haber infinitos números primos.
Siempre que se sienta cómodo con la aritmética básica y tenga una comprensión informal de la “negación” y la “contradicción”, podrá seguir esta cadena de deducciones. La idea crucial es que llegar a una prueba en primer lugar puede requerir mucha (a falta de una palabra mejor) creatividad, pero comprobar una es un procedimiento puramente mecánico: no tienes que confiar en mi palabra, puedes comprobar por ti mismo que mi prueba es correcta. De hecho, una prueba que no se puede verificar no es una prueba: como lo expresó Alonzo Church, si un auditor no puede verificar con “ciertos medios” una secuencia de fórmulas presentadas como prueba, puede exigir otra prueba, y “hasta que se proporcione la prueba complementaria, puede negarse a dejarse convencer” (y así sucesivamente, potencialmente para siempre).
Para resumir: una prueba es una forma comprobable paso a paso de demostrar que una conclusión se deriva de un conjunto de premisas. Dado que las pruebas se pueden verificar por diseño, podemos crear software que realice las verificaciones mecánicas a escala y usarlo para distinguir la basura de las pruebas correctas generadas por los LLM.
Como muestra la historia del software, los algoritmos funcionan bien en lenguajes definidos formalmente, como Python o Rust. En nuestro camino para construir nuestro propio pequeño verificador, debemos elegir una forma de representar las pruebas para que una computadora pueda verificarlas fácilmente.
Un lenguaje de programación para el razonamiento.
"La virtud de los textos formales es que sus manipulaciones, para ser legítimas, necesitan satisfacer sólo unas pocas reglas simples; son, si lo piensas bien, una herramienta sorprendentemente efectiva para descartar todo tipo de tonterías que, cuando usamos nuestras lenguas nativas, son casi imposibles de evitar".
—EW Dijkstra
Vibe Coding puede darnos la ilusión de que ahora “programamos en inglés”, pero al final las computadoras siempre ejecutan instrucciones en un lenguaje de programación. Si queremos que una computadora verifique las pruebas, necesitamos expresarlas en un lenguaje preciso: inequívoco de analizar, fácil de manipular.
Después de soñar con ello durante siglos, los matemáticos han descubierto cómo utilizar las matemáticas para modelar el razonamiento mismo, un lenguaje de programación especial, por así decirlo, para realizar demostraciones de forma rigurosa. Tomemos esta prueba trivial, que pretende demostrar que 12 es par y divisible por 3 partiendo de dos premisas evidentes:
S₁: 12 es mayor que 10 y 12 es par S2: 12 es divisible por 3 Por la línea 1, podemos ver que 12 es par Por la línea 2, podemos ver que 12 es divisible por 3 C, por la línea 3 y 4: por lo tanto, 12 es par y 12 es divisible por 3
Podemos usar variables y operaciones booleanas para representar oraciones en símbolos, de manera análoga a abstraer cadenas en constantes en Python: Q = “12 es mayor que 10”; R = “12 es par”; Z = “12 es divisible por 3”
Q Y R Z R (1) Z (2) R Y Z (3,4)
Con las dependencias entre líneas expresadas entre paréntesis, es fácil ver qué reglas mecánicas se pueden usar aquí: una regla (“eliminación AND”) establece que de alfa Y beta (donde alfa y beta son marcadores de posición) podemos eliminar Y y obtener uno de los dos; otra regla (“Y introducción”) dice introducir alfa Y beta siempre que alfa y beta aparezcan en algún paso previo. A diferencia de la prueba inglesa, esta traducción permite la manipulación mecánica: si se desea una analogía con la codificación, una prueba correcta es como un script que “se compila correctamente”, según lo establece automáticamente un algoritmo (el compilador/verificador).
En cálculo, cuando introducimos funciones trigonométricas, necesitamos nuevas reglas derivadas. De manera similar, cuando introducimos más operadores booleanos (NO, O), necesitamos nuevas reglas. El lector puede consultar los detalles en línea (o directamente en el repositorio), pero la esencia general permanece: una regla reorganizará una o más líneas en una nueva línea, ya sea eliminando operadores existentes o introduciéndolos.
Para resumir: podemos transformar una demostración en inglés en símbolos que puedan manipularse fácilmente, de manera similar a tratar una parábola como una ecuación para que podamos obtener la derivada mediante alguna “reorganización” de los términos. Verificar la prueba simbólica nos dice si el razonamiento es correcto y si se puede confiar en la conclusión matemática.
Sin embargo, hay infinitas cosas que podemos querer probar: ¿cómo sabemos que en una prueba particularmente compleja las reglas no fallarán y pasarán una prueba basura para obtener un resultado correcto? En otras palabras, ¿no trasladamos simplemente la carga de los LLM que alucinan a reglas que inventaron los matemáticos (plausiblemente falibles)?
Aquí es donde ocurre la verdadera magia: dado que el razonamiento en sí ahora está establecido con precisión, ¡nos volvemos meta y demostramos cosas sobre nuestras reglas para las pruebas mismas!
Una prueba de solidez
"No creo en la ciencia empírica. Sólo creo en la verdad a priori".
— atribuido a K. Gödel
Incluso si un algoritmo verifica que las reglas de la prueba se aplicaron correctamente, todavía no sabemos si la prueba está verificada; después de todo, ¡los programas tienen errores todo el tiempo! En otras palabras, ¿cómo sabemos que las reglas de manipulación son correctas?
Es posible que el lector perspicaz ya haya notado nuestro juego de manos. Como seres humanos, nos preocupamos por la verdad de nuestras declaraciones: queremos sacar conclusiones verdaderas de lo que ya sabemos. Sin embargo, las máquinas se preocupan por la secuencia de símbolos en una línea de prueba y cómo se crea una nueva línea reorganizándolas mecánicamente (recuerde: puede obtener la derivada de x2 + 3 reorganizando los símbolos, ¡sin saber qué es una pendiente!). ¿Cuál es entonces la conexión entre los símbolos y la verdad? Idealmente, estas dos perspectivas deberían alinearse: al usar reglas sobre premisas verdaderas, debería obtener nuevas líneas que sean verdaderas en sí mismas. En otras palabras, las reglas preservan la verdad: no importa cuán complejas sean las pruebas, ninguna aplicación de una regla producirá un enunciado falso a partir de uno verdadero.
Cuando pasamos de investigar pruebas específicas a discutir lo que deberían hacer todas las pruebas, pasamos de la lógica a la metalógica. Es la metalógica la que responde a nuestra pregunta, que se llama la “solidez” del sistema, es decir, una prueba de que, en cada secuencia de manipulaciones que conducen de las premisas a una conclusión, la conclusión es necesariamente verdadera siempre que las premisas lo sean. Como las pruebas de solidez son tediosas, mostramos cómo la prueba funciona para una sola regla y aprovechamos la oportunidad para presentar cómo se modela el concepto de verdad en nuestro lenguaje.
La prueba anterior agregó alfa Y beta como un nuevo paso a partir de alfa, y la beta aparece por separado. Hasta ahora, todo bien. Para modelar la verdad, definimos una interpretación, que es una asignación I de valores de verdad (1 = Verdadero, 0 = Falso) a nuestras variables, con la definición recursiva estándar para oraciones complejas:
I(p Y q) = 1 si y sólo si I(p) = 1 y I(q) = 1 I(NO q) = 1 si y sólo si I(q) = 0 …
Esta definición se sentiría como un déjà vu para cualquier programador que alguna vez haya hecho algo como if boolean_var y boolean_other_var, y eso se debe a que AND, OR, NOT en Python están modelados según la semántica estándar de los conectivos lógicos (¡uno de los muchos vínculos entre programación y lógica!).
Una función de interpretación define un posible estado del mundo asignando variables a booleanos: por ejemplo, un mundo tiene p verdadero y q falso, otro mundo tiene ambos falso, y así sucesivamente (en el caso de codificación, la interpretación se realiza en el script al inicializar boolean_var y boolean_other_var). Para completar la verificación de solidez, debemos demostrar la preservación de la verdad en todos los estados posibles del mundo. Usamos una tabla de verdad para descubrir que, siempre que p y q sean verdaderos, p Y q también lo son:
Como queríamos, la regla efectivamente cumple con nuestra definición de consecuencia lógica: cada vez que las premisas son verdaderas, la conclusión necesariamente lo es (fila 1). ¿Es cierto lo contrario? Es decir, si una conclusión se deriva de algunas premisas, ¿hay siempre una prueba de ello? Sólo que en algunos “lenguajes de programación” (como el nuestro), la respuesta es sí: esto se conoce como completitud, y es el dual de solidez (¡también es más interesante, pero mucho más difícil de demostrar!).
Si somos capaces (¡y lo somos!) de garantizar que cada regla que utilizamos preserva la verdad, obtenemos la certeza de que no importa cuán compleja sea una prueba, no importa qué tan lejos en el futuro, no importa si los LLM o los humanos están razonando, el software de verificación de pruebas nunca pasará una prueba basura para un razonamiento correcto.
Salvo errores de implementación (que por supuesto son inevitables) y una traducción fiel del inglés a símbolos, entonces, una prueba verificada es el estándar definitivo para la certeza: una forma precisa e inequívoca de razonamiento que sea matemáticamente sólida y comprobada algorítmicamente. Esto no solo es importante como principio rector al confiar a los LLM descubrimientos matemáticos, sino que también subraya cuán diferentes son las matemáticas de cualquier otra cosa: si bien podemos despertarnos un día y descubrir que Newton estaba equivocado (¡lo hicimos!), nunca nos despertaremos un día y descubriremos que los números primos no son infinitos. Una vez que se verifica una prueba, es conocimiento eterno sobre el que podemos construir de manera segura para obtener nuevos conocimientos:
[Los matemáticos del griego antiguo] no son escolares inteligentes, sino miembros de otra universidad.
GH Hardy
¡Nos vemos, vaqueros de las matemáticas!
"Hablar es barato. Muéstrame el código".
– L. Torvalds
En esta primera pieza, construimos un modelo mental para comprender por qué deberíamos esperar que el razonamiento matemático sea algo que pueda ser verificado de manera confiable por una computadora. Al responder nuestras preguntas iniciales, aprendimos la naturaleza distintiva y mecánica de las pruebas e introdujimos los ingredientes mínimos que necesitamos para representar las pruebas como un programa: un lenguaje y reglas de manipulación (básicamente, ¡un DSL!).
En el repositorio complementario,proof_checker_playground.py muestra una muestra de pruebas válidas e inválidas que aprovecha una pequeña clase de Python que implementa nuestra lógica de verificación. El verificador primero verifica que una serie determinada de pasos sea sintácticamente correcta: como cualquier lenguaje de programación, ¡necesitamos que los símbolos tengan el formato adecuado! Luego, se procede paso a paso, simulando a un matemático comprobando que efectivamente cada nueva línea en la demostración se deriva de las anteriores. Nuestro código logra esto de una manera ligeramente poco ortodoxa en comparación con los probadores más fuertes de la industria, sacrificando el rendimiento (tarea: ¿puedes adivinar por qué es computacionalmente ineficiente? ¿Durante cuánto tiempo crecerá una tabla a medida que aumenta el número de variables?) con fines pedagógicos. Al verificar el paso 4 en esta prueba de muestra:
S₁: … S2: .. S3: A Y B A (3) …
el verificador recuperará la justificación (la premisa en la línea 3), luego construirá una tabla de verdad con las variables requeridas (A, B), con la línea 3 como premisa y el paso objetivo (línea 4) como conclusión:
El lector experto ya puede ver adónde va esto: el paso de demostración se considera correcto si, siempre que las premisas son verdaderas, la conclusión también lo es: ¡la definición de consecuencia lógica con la que partimos!
En el siguiente artículo, capacitaremos a un LLM para generar pruebas y utilizaremos el andamiaje construido hoy para verificar esas pruebas. Aprovecharemos los LLM de código cerrado y el verificador para ayudarnos a crear un conjunto de datos de pruebas verificadas y luego usaremos Tinker para configurar un ciclo de aprendizaje de refuerzo. Solicitamos a un pequeño modelo de código abierto que demuestre una conclusión a partir de algunas premisas, luego pasamos la prueba generada al verificador y recompensamos al modelo si es correcto.
Si bien no está claro en qué medida RL “simplemente” enfatiza las capacidades existentes o aprende cosas novedosas, de cualquier manera esperamos que incluso un modelo pequeño pueda demostrar hechos simples en nuestro “lenguaje de programación”: ¡nos vemos, vaqueros de las matemáticas!
Preguntas frecuentes
Si desea profundizar más, aquí hay algunos seguimientos comunes:
Las reglas preservan la verdad, pero ¿cómo sé que las premisas son verdaderas en primer lugar? Lógicamente hablando, una consecuencia puede derivarse de premisas erróneas, pero una demostración que comience desde 2+2=5 difícilmente será interesante. En la mayoría de los casos del mundo real, nuestras premisas son el resultado de otros teoremas, por lo que sabemos que son consecuencias de otros hechos más fundamentales; la mala noticia es que en algún momento la responsabilidad debería parar y no se pueden invocar más premisas. Resulta que la gran mayoría de las matemáticas pueden estar respaldadas por unas pocas afirmaciones, los axiomas de la teoría de conjuntos: dado que los axiomas son premisas que no se pueden probar, es interesante preguntarnos qué justifica creer en ellas en primer lugar. Sin embargo, los axiomas matemáticos son menos discutibles que, digamos, la moralidad, razón por la cual es mucho más fácil creer en la formalización de las matemáticas (donde todos están de acuerdo con las premisas, por lo que “simplemente” verificamos el razonamiento), que hacer lo mismo con los argumentos legales (donde a menudo las dos partes parten de premisas diferentes). La buena noticia, sin embargo, es que una prueba se parece a un programa de computadora en más de un sentido: una vez que conocemos un teorema, ahora podemos “importarlo” a una prueba más grande de manera similar a como importamos pandas en nuestro código. Si la verificación de pruebas es completamente algorítmica, ¿podemos también escribir un algoritmo para probar todas las verdades? En general, no podemos. La existencia de verdades que no podemos probar es probablemente uno de los hechos matemáticos más profundos del último siglo: ésta es la conclusión esencial del teorema de incompletitud de Gödel. Además, no sabemos si algunas afirmaciones son verdaderas o falsas, ya que nuestro mejor sistema de axiomas a veces no puede decidir (el axioma de elección es un ejemplo famoso de algo independiente de la teoría de conjuntos). ¿Podemos demostrar cosas interesantes sobre la noción misma de prueba? ¡Sí! Si bien el punto de vista de Church es definitivamente un argumento sólido, en su camino hacia la demostración de su célebre teorema, Gödel demostró que el predicado IsProofOf(prueba, afirmación) es algorítmico. Además, ¡existe toda una lógica para la demostrabilidad! ¿Dónde puedo leer más? Mi texto favorito de introducción a nivel intermedio es Lenguaje, prueba y lógica, que está especialmente dirigido a estudiantes que no son de matemáticas; Computabilidad y lógica es un texto intermedio que se centra en la relación entre lógica, prueba y computación.
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).