Terence Tao sobre los verificadores de pruebas y los copilotos de IA para matemáticas
(scientificamerican.com)- A medida que las demostraciones matemáticas se formalizan con más rigor, herramientas como Lean están verificando las pruebas humanas y cambiando la base de confianza de la colaboración a gran escala
- Con la acumulación de bibliotecas estándar como mathlib, está bajando la barrera de entrada para formalizar desde teoremas de nivel universitario hasta áreas nuevas
- En la formalización de la conjetura PFR participaron más de 20 personas, que se repartieron pequeños pasos de la demostración, mientras Terence Tao se enfocó en gestionar la dirección general más que en revisar línea por línea
- Por ahora, la IA está más cerca de ayudar como copiloto de demostraciones en tareas de formalización, verificación e iteración, que de “resolver” las matemáticas
- La investigación matemática podría transformarse en un trabajo más explícito y dividido, con tareas como definir la dirección humana, formalizar detalles, entrenar IA e interpretar pruebas generadas por IA
La formalización está cambiando la colaboración matemática
- La investigación matemática tradicional se parecía más a una colaboración entre pocas personas, y Tao considera que normalmente unas 5 personas están cerca del límite superior del tamaño de colaboración
- Con verificadores automáticos de pruebas (proof checkers), también se puede colaborar con cientos de personas que no se conocen entre sí
- Los colaboradores suben código y el compilador de Lean lo verifica
- La confianza no depende solo de relaciones personales, sino que puede confirmarse mediante resultados de verificación formal
- En la formalización del resultado reciente sobre la conjetura Polynomial Freiman-Ruzsa (PFR) participaron más de 20 personas
- La demostración se dividió en muchos pasos pequeños
- Cada participante se encargó de demostrar un paso
- Tao gestionó la dirección general del avance, en lugar de revisar cada aporte línea por línea
No todos los matemáticos necesitan ser programadores
- En los proyectos de formalización es posible dividir roles
- Algunas personas se enfocan en la dirección matemática
- Otras se especializan en convertir pequeños fragmentos matemáticos en pruebas formales
- Incluso matemáticos poco familiarizados con las computadoras, como Peter Scholze, pueden participar en proyectos de Lean
- Si una gran tarea matemática se divide en partes pequeñas, se puede contribuir a una subtarea específica sin entender toda la teoría completa
Lean, mathlib y la búsqueda hicieron posible su uso práctico
- Una de las grandes razones por las que la matemática formal se volvió práctica es el avance de las bibliotecas matemáticas estándar
- Lean cuenta con un proyecto de gran escala llamado mathlib
- Teoremas básicos de matemáticas de pregrado, como cálculo y topología, se van incorporando uno por uno a la biblioteca
- El objetivo es llevar la biblioteca hasta el nivel de posgrado
- Eso facilitará formalizar nuevas áreas de las matemáticas
- Para construir demostraciones hay que encontrar teoremas ya verificados como verdaderos, por lo que también se vuelven importantes los motores de búsqueda más inteligentes
- Después de formalizar todo el proyecto PFR, la compilación de verificación tarda apenas unos 30 minutos
- El cuello de botella no está tanto en la potencia de cómputo, sino en la usabilidad, la facilidad de uso y la adaptación de las personas a las herramientas
- Lean se considera actualmente el lenguaje formal con la comunidad más activa
- Para proyectos de autor único, otros lenguajes pueden ser mejores
- Lean es fácil de aprender y tiene buenas bibliotecas y comunidad
- Más adelante podría ser reemplazado por otras alternativas, pero hoy es el lenguaje formal dominante
El costo de formalización sigue siendo alto
- Tao cree que puede formalizar ciertos proyectos, pero que hoy eso podría requerir un mes de su tiempo
- Todavía no estamos en una etapa en la que todos los resultados se formalicen de manera rutinaria
- Hay que elegir casos en los que ayude a aprender Lean
- Casos donde haya mucho interés en la corrección del resultado
- Proyectos donde la formalización aporte valor real
- A medida que mejore la tecnología, el costo de formalización podría bajar
- Hoy puede tomar 10 veces más que el método tradicional
- En el futuro podría reducirse a alrededor de 2 veces, e incluso a menos de 1 vez
La IA puede convertirse en copiloto de los matemáticos
- Tao imagina un futuro en el que, en vez de tipear las demostraciones directamente, los matemáticos se las expliquen a sistemas como GPT, y la IA intente formalizarlas en Lean durante el proceso
- Si la verificación pasa, se podrían entregar juntos el artículo en LaTeX y la prueba en Lean
- Si el usuario lo desea, podría ser un asistente que ayude incluso con el envío a revistas
- Actualmente, la ruta más rápida para formalizar sigue siendo que una persona primero cree la idea y el borrador de la demostración
- A largo plazo, también podrían ser posibles proyectos en los que las personas formalicen pequeños fragmentos sin conocer toda la demostración, y la IA y los humanos los conecten para probar grandes teoremas
- Tao cree que harán falta varios años para que ese enfoque sea posible
- La tecnología actual todavía es insuficiente y la formalización sigue siendo una tarea dolorosa
La distancia frente a la idea de que “las matemáticas se resolverán”
- Tony Wu y Christian Szegedy han dicho que, en 2 o 3 años, las matemáticas estarán “resueltas” en el sentido de que las máquinas encontrarán demostraciones mejor que los humanos
- Tao no cree que las matemáticas vayan a resolverse en 3 años, aunque sí piensa que la IA podría volverse útil para los matemáticos y mostrar avances claros en ese plazo
- La IA puede ser un copiloto al que se le pida ayuda cuando un paso de una demostración parece verdadero, pero una persona no lo ve de inmediato
- Aunque la IA llegue a hacer matemáticas al nivel que hoy hacen los humanos, los matemáticos humanos podrían pasar a un nivel más alto de matemáticas
- La IA también podría permitir demostrar cientos o miles de teoremas a la vez
- Los matemáticos humanos asumirían el rol de dirigir qué hará la IA
- Tao considera que una estimación de 2 o 3 años para ese cambio es algo agresiva
Comprensión de pruebas y demostraciones generadas por IA
- Una demostración matemática no es solo un procedimiento para confirmar que algo es verdadero, sino también un proceso para entender por qué lo es
- En el futuro cercano, es probable que la IA primero automatice trabajos tediosos y triviales, mientras los humanos siguen marcando la dirección
- Si la IA produce una demostración difícil de entender y poco elegante, las personas pueden volver a analizarla
- Por ejemplo, en una demostración que obtiene una conclusión a partir de 10 supuestos, se puede verificar si sigue siendo válida al quitar uno de esos supuestos
- Podría surgir un nuevo tipo de matemático dedicado a extraer ideas de demostraciones generadas por IA
- Las primeras pruebas de IA podrían parecer carentes de intuición
- Las personas pueden hacerlas más comprensibles y encontrarles estructura
Problemas abiertos y límites de la IA
- Para demostrar una conjetura abierta, primero es necesario dividirla en fragmentos más pequeños
- Es mucho más fácil transformar un problema en uno más difícil que convertirlo en uno más sencillo
- Tao cree que la IA todavía no ha mostrado ser mejor que los humanos en esa tarea de descomposición
- Es interesante usar IA para sugerir posibles conexiones entre distintas áreas
- La tasa de éxito actual es baja
- De 10 propuestas, quizá solo 1 sea interesante y 9 no sirvan
- Tao cree que esto podría cambiar en el futuro
El problema de los datos en el conocimiento matemático
- Uno de los problemas para entrenar IA matemática es la falta de datos suficientes
- Los artículos en línea pueden usarse para entrenamiento, pero mucha intuición matemática no queda registrada en los papers
- Conversaciones entre matemáticos
- Clases
- La forma de orientar a estudiantes
- Intentos fallidos y procesos de corrección
- Las demostraciones publicadas son resultados comprimidos, y la gente tiende a publicar solo los casos exitosos
- Los datos realmente valiosos son los procesos que muestran que se intentó algo, no funcionó y luego cómo se corrigió
- En el futuro, los intentos de investigación y sus fracasos podrían registrarse para entrenar IA o para evitar que otros investigadores repitan fracasos
- Tao da como ejemplo una situación en la que alguien acepta registrar su proceso de investigación para usar un sistema avanzado tipo AI Lean en 2040
El cambio hacia una matemática más explícita
- Mucho conocimiento matemático queda encerrado en la cabeza de matemáticos individuales, y solo una parte muy pequeña permanece de forma explícita
- A medida que aumente la formalización, más conocimiento tácito se convertirá en conocimiento explícito
- Los libros de texto formalizados podrían dar lugar a libros interactivos
- Comenzarían con explicaciones de alto nivel de una demostración
- Los pasos que no se entiendan podrían desplegarse con más detalle
- Si se desea, se podría bajar hasta el nivel de los axiomas
- Este enfoque podría facilitar que matemáticos de un área contribuyan a otra
- Se pueden especificar con precisión subtareas de un gran proyecto
- Es posible participar en las piezas necesarias sin entenderlo todo
1 comentarios
Comentarios de Hacker News
https://archive.is/Idouw
La expresión project manager mathematicians recuerda la sátira que Edsger Dijkstra escribió en 1975, “A letter to my old friend Jonathan” [1], y su texto de seguimiento [2]
Era una crítica que mostraba lo ridículo que sería aplicar a las matemáticas la forma en que se construye software, pero en cierto sentido fue algo visionaria
El punto central era criticar el absurdo de aplicar propiedad intelectual, especialmente a la verdad matemática, y por suerte en la actual tendencia hacia la mecanización esa parte no parece ser una gran preocupación
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
Es un texto con buena intuición, pero creo que lo que falta es que los LLM están abstrayendo de maneras cada vez más sobrehumanas
Tao dijo que “es fácil volver un problema más difícil, pero difícil volverlo más simple, y la IA nunca ha demostrado ser mejor que los humanos en esto”, pero por la forma en que operan los LLM podría volverse posible una intuición de mucho más alto nivel
Ahora están más cerca de ser asistentes, verificadores de hechos y encargados del trabajo tedioso, pero pronto pasarán a sugerir intuiciones. Los LLM ya tienen intuiciones que nosotros no vemos al trabajar con embeddings y comprimir conocimiento
El momento en que Hinton pone como ejemplo la relación entre una bomba nuclear y un montón de compost: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
No son más que máquinas entrenadas para imitar la forma en que escriben los humanos, y no existe el conjunto de datos necesario para imitar algo más inteligente que los humanos
No tengo dudas de que el aprendizaje automático superará la inteligencia humana, pero el cuello de botella es encontrar cómo hacer que aprenda de sus propias salidas sin intervención humana, en lugar de seguir ajustándose contra la totalidad de los textos del mundo
Ramanujan hizo descubrimientos matemáticos brillantes sin educación formal y habiendo visto apenas unos pocos libros de matemáticas, una cantidad que desde la perspectiva de los datos de entrenamiento de un modelo de aprendizaje automático es casi nada
Me tomó unos 10 segundos ponerlo en palabras, pero si conoces la información necesaria la respuesta era obvia
Hinton dice que esto muestra razonamiento analógico, pero hay muchos textos en línea sobre jardinería y sobre la física de los montones de compost, así que es muy probable que ChatGPT ya lo hubiera visto durante el entrenamiento
Por eso, este ejemplo parece un caso en que no se controló si el LLM ya había visto en esencia la respuesta en el texto de entrenamiento
También es interesante la parte más adelante del video en la que Ilya dice “hay una prueba de existencia. El cerebro humano es una red neuronal” (https://youtu.be/Gg-w_n9NJIE?t=4966). En general estoy de acuerdo con la idea de que el cerebro humano también es una red neuronal, pero también hay muchas objeciones: las neuronas reales no operan a 8 bits, y difieren en tipos celulares, ADN, entorno químico hormonal, etc., así que me parece que ahí hay una bifurcación filosófica
Eso podría hacerse en minutos u horas
En cambio, para conseguir un experto humano adicional hace falta que aparezca alguien a quien le guste profesionalmente la matemática, que atraviese décadas de formación y alta especialización, y ni siquiera hay garantía de que esa persona llegue hasta el final o alcance el nivel necesario para empujar la frontera del conocimiento
Mientras se espera todo ese tiempo, también podría crearse en paralelo una cantidad de expertos de IA del orden de billones
El ancho de banda con el que el cerebro humano absorbe nueva información es bajo, pero las máquinas pueden copiar el conocimiento de toda una vida en segundos, mantener miles de conversaciones en paralelo e incluso serializar partes de un cerebro para enviarlas a otras IA. Si además se llega a la materia programable, sería posible crear computronium de forma exponencial, y hasta un omega point donde miles de años de investigación ocurran en segundos
No sé nada de matemáticas, pero esto me recuerda a la historia del software. Antes, proyectos asombrosos como RollerCoaster Tycoon eran obras hechas casi por una sola persona.
Después, la ingeniería de software se modularizó de una forma parecida a la que se describe en la entrevista, y ahora se ha vuelto una enorme línea de ensamblaje donde gente como yo produce React para ganarse la vida, y parece que la productividad por persona o la habilidad requerida se acercaron casi a 0.
Me da la impresión de que, cuando un campo está en su apogeo, un genio puede llevar cien cosas en la cabeza y hacer el mejor trabajo, y cuando eso es reemplazado por una línea de ensamblaje, ese campo deja de poder crear cosas realmente valiosas.
La ingeniería de software no ha dejado de hacer cosas geniales; de hecho, yo diría que ocurrió exactamente lo contrario.
Bromas aparte, algún día llegará el momento de corregir un bug crítico, y ahí se verá la habilidad real. Que un producto o servicio se haya vuelto estable y rentable no significa que los desarrolladores originales ya se fueron ni que nadie pueda lograr algo grande.
Decir que este campo ya no produce cosas realmente valiosas es muy equivocado.
Es como comparar una catedral construida por 100 personas a lo largo de 100 años con una choza hecha por una sola persona en un mes. La choza también se mantiene en pie y te da un lugar donde vivir, pero no es una catedral.
Del lado del desarrollo web, incluso si solo quieres mirar Python, hay tantos frameworks y tecnologías en cada pequeño engrane de la rueda que de verdad es difícil seguir el ritmo.
La habilidad suele seguir aproximadamente una distribución log-normal, así que la gente excepcional siempre es escasa, y los campos pequeños en sus inicios pueden tener una densidad irrealmente alta de talento de primer nivel porque la falta de infraestructura de apoyo hace que solo sobrevivan personas con talento extremo.
Forzar la unión de 47 frameworks modernos para sacar otra app de tareas no es lo mismo, en lo fundamental, que generar un impacto significativo.
Desde la perspectiva de costo-beneficio, hay un óptimo local muy fuerte en producir mucho código barato en vez de invertir a largo plazo en cosas grandes, y mientras más madura se vuelve un área, más baja se vuelve la barrera mínima de habilidad para llegar a ese punto.
Tampoco hay muchas organizaciones enfocadas en formar talento de primer nivel. Por eso, a medida que el campo crece, es fácil explicar por qué la habilidad promedio cae por abandono, y si manejas mal la distribución, luego puede salir caro corregirlo.
La demostración verificada por computadora es un área donde la IA podría volverse útil en un plazo relativamente corto. Aun así, quizá se parezca más a la red neuronal de un motor de ajedrez que a un LLM completo.
Demostrar todo a mano es aburrido y toma mucho tiempo, así que ya se usan muchos solvers, pero las tácticas o los solvers sufren si les lanzas demasiados teoremas y lemas auxiliares.
Una red neuronal como máquina de búsqueda para encontrar lemas relevantes mediante pattern matching encaja muy bien.
La inducción y la unificación de orden superior también son, en esencia, síntesis de código, y recorrer por fuerza bruta todos los árboles sintácticos posibles es muy ineficiente.
De cualquier modo, los solvers hacen backtracking, así que no pasa nada si la IA propone lemas inútiles el 95% de las veces, y aun así podría ser un avance dramático frente a la búsqueda manual.
Aun así, no estoy seguro de que la demostración verificada por computadora sea necesariamente buena para la comunicación. Las demostraciones legibles para humanos son de alto nivel y omiten detalles por varias razones, no solo por longitud.
El problema central es que tienen que estar conectados con la definición formal de los objetos matemáticos usados en una demostración.
Pero las personas no piensan así cuando escriben o leen una demostración. Normalmente tienen una intuición informal y de alto nivel de lo que están haciendo “en términos morales”, y completan los detalles formales según haga falta.
El código de computadora funciona hasta cierto punto porque la semántica formal del lenguaje está mucho más cerca del modelo mental, pero en matemáticas el objetivo suele ser distinto.
La estrategia sledgehammer de Isabelle combina demostradores automáticos de teoremas como E, Z3, SPASS y Vampire para intentar demostrar o refutar un objetivo.
En teoría suena bien, pero en la práctica termina produciendo una demostración reconstruida que aplica 12 lemas aparentemente arbitrarios, y esas demostraciones no se pueden leer y son muy frágiles.
No parece que la IA vaya a resolver ese problema por arte de magia.
Las redes neuronales actuales tienen una eficiencia de muestra extremadamente baja, y los datasets de matemáticas formales son mucho más pequeños que los de código Python, por ejemplo.
Hace unos meses Terence Tao dio una excelente charla sobre este tema y habló con más detalle del uso de Lean: https://www.youtube.com/watch?v=AayZuuDDKP0
Un matemático en activo dijo que, en investigación, logró que GPT-4o demostrara probablemente un nuevo lema auxiliar
“Mi pareja es matemática, y la semana pasada usó ChatGPT por primera vez para demostrar algunos lemas auxiliares para investigación. Ya sospechaba que esos teoremas eran verdaderos y tenía una idea general del enfoque, pero no era especialista en ese tipo de proposiciones. Fue la primera vez que obtuve del modelo una demostración correcta y útil
El primer lema auxiliar lo encontró un colaborador al calcular para valores pequeños de e. ChatGPT no pudo hallar la demostración hasta que se le indicó que probara con la función de Möbius
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
El segundo parece más estándar y probablemente Mathematica también habría podido hacerlo. Pero como Mathematica no da una derivación limpia, sigue siendo útil
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
Estas cosas se están volviendo aterradoramente buenas en razonamiento y en temas pesados
Si el campo del aprendizaje automático sigue concentrándose en añadir capacidades de sistema 2 para complementar el pensamiento de sistema 1, que en general tienen los LLM, la cosa podría ponerse intensa
Memoria impresionante, no razonamiento nuevo
Nosotros lo pensamos como una suma sobre particiones ordenadas y no como una suma de particiones con coeficientes |τ|!, pero por supuesto ambas cosas son lo mismo
Si se consideran particiones ordenadas cíclicamente, es decir, usando coeficientes (|τ|-1)! en lugar de |τ|!, el resultado es 0 y no (-1)^e
La demostración combinatoria de Beren construye una biyección entre particiones cíclicamente ordenadas de longitud par e impar eligiendo un elemento especial: si ese elemento está solo, se fusiona con la siguiente parte; si no está solo, se separa en su propia parte
En el caso lineal, se aplica algo parecido empezando por el último elemento, pero las particiones en las que el último elemento está solo en la última parte no encuentran pareja, así que se procede recursivamente con el elemento anterior
Al final todo queda emparejado y solo sobrevive la partición en la que todos los elementos están separados y en el orden original. Según la paridad del tamaño del conjunto original, la suma con signos lleva a la proposición original
Tampoco se sabe cuántos términos tiene la suma sobre “τ ≤ τ”, y tampoco cuadra cómo eso se conecta con establecer uno de los lados izquierdo o derecho en el punto 3 y luego concluir el otro
En realidad, lo que hizo ChatGPT fue recordar la función de Möbius del retículo de particiones, repetirla sin demostración y luego soltar palabrería que solo parecía plausible
Precisamente plantear esa función de Möbius es, en esencia, la parte central, y la pregunta equivale casi a demostrar que esa función tiene esa forma
Además, la fórmula general que dio ChatGPT también es ligeramente incorrecta, y solo acierta en el caso |σ| = 1, que es el importante para la demostración actual
De hecho, esto se puede ver enseguida sin usar explícitamente toda la maquinaria de la función de Möbius, si se define N(t,e) como el número de particiones en e clases de equivalencia divididas en t grupos, y se hace una inducción elemental con la recurrencia N(t,e+1)=N(t-1,e)+tN(t,e)
En esta entrevista destacan tres cosas
Primero, Tao imagina un futuro en el que las ideas matemáticas, igual que otros productos de la sociedad, se “producen”, y habla de project manager mathematicians. Cree que la razón por la que las matemáticas aún no se han industrializado así es la falta de herramientas, y ve en la IA y los asistentes de prueba algo revolucionario en ese aspecto. Aun así, la interacción y la guía humanas siguen siendo necesarias
Segundo, hay muchísimo conocimiento tácito que no queda plasmado en los papers. Cosas como la intuición o el conocimiento de los fracasos son importantes, así que incluso los mejores matemáticos necesitan hablar entre sí para no repetir los mismos errores
Tercero, es fácil pensar que las matemáticas ya están suficientemente formalizadas, pero los papers suponen mucho conocimiento compartido. Formalizar las demostraciones de una manera que los asistentes de prueba puedan entender ayuda a que más gente comprenda qué es lo que realmente está ocurriendo
Como mostró Tao en su charla sobre el proyecto Polymath, queda claro que siempre está buscando nuevas formas de hacer investigación matemática
Por ahora, quizá esto sea un tipo de proyecto posible solo para medallistas Fields como Tao o Scholze, que pueden darse el lujo de dedicar 10 veces más tiempo a una demostración
Hace poco hablé con un posdoctorado de matemáticas de primer nivel y me dijo que no conoce a nadie a su alrededor que use lean4 en trabajo real
Para alguien en el inicio de su carrera, probablemente sea mejor confiar en la intuición y publicar el paper
Para ver este tema correctamente, no basta con unas pocas impresiones personales
En cambio, en áreas con un estilo más intuitivo, como la topología de baja dimensión, esperaría ver menos gente usando verificadores de pruebas
Aquí intuitivo no significa menos riguroso. Una demostración con dibujos de cierta equivalencia de homotopía es mucho más difícil de trasladar a algo que Lean pueda entender que una lista de desigualdades
Como referencia, estoy en geometría/topología y todavía no he visto ni oído de nadie que use estas herramientas
https://lean-lang.org/
https://github.com/leanprover/lean4
“Si la IA proporciona una demostración incomprensible y fea, se puede analizar. Si esta demostración usa 10 supuestos para obtener una conclusión, ¿sigue funcionando la demostración si se elimina uno de los supuestos? Ese tipo de ciencia aún no existe porque todavía no hay muchas demostraciones generadas por IA, pero aparecerá un nuevo tipo de matemático que tomará las matemáticas generadas por IA y las hará más comprensibles”, es exactamente lo mismo que pienso sobre el diseño de APIs públicas del código
Un rol que tradicionalmente solo desempeñaban desarrolladores experimentados ahora podría simplificarse enormemente y volverse accesible para todos