El kit de herramientas de inteligencia artificial define la forma de los probadores automáticos de teoremas de próxima generación y, con ello, la relación entre las matemáticas y las máquinas.
Se dice que en 1970 el ahora fallecido matemático Paul Cohen , único ganador de la Medalla Fields por su trabajo en lógica matemática , ha realizado predicciones infundadas que aún continúan como un deleite o irritación de los matemáticos: "algún día reemplazará a los futuros matemáticos ordenadores ". Cohen, conocido por sus métodos atrevidos al trabajar con la teoría de conjuntos, predijo que todas las matemáticas podrían automatizarse, incluida la redacción de pruebas.
La prueba es un razonamiento lógico paso a paso que confirma la verdad de una hipótesis o suposición matemática. Después de que aparece una prueba, una hipótesis se convierte en teorema. Confirma la exactitud de la declaración y explica por qué es cierta. Pero la prueba es extraña. Es abstracto y no está ligado a la experiencia material. "Son el resultado de un contacto loco entre un mundo ficticio, no físico y criaturas que surgieron de la evolución biológica", dijo el científico cognitivo Simon Dedeo de la Universidad Carnegie Mellon, quien estudia la certeza matemática a través del análisis de estructuras de evidencia. "La evolución no nos preparó para esto".
Las computadoras son buenas para la computación masiva, pero la prueba requiere algo diferente. Las hipótesis surgen del razonamiento inductivo, una intuición especial asociada con un problema interesante, y las demostraciones suelen seguir una lógica deductiva paso a paso. A menudo requieren un pensamiento creativo complejo, así como el arduo trabajo de llenar los vacíos, y las máquinas no pueden manejar esta combinación de habilidades.
Los probadores de teoremas computarizados se dividen en dos categorías. Los probadores de teoremas automatizados (ATP) suelen utilizar métodos de fuerza bruta para moler grandes cantidades de números. Los probadores de teoremas interactivos (ITP) sirven como asistentes humanos y pueden verificar la precisión de los argumentos, así como buscar errores en las pruebas existentes. Sin embargo, incluso si combina estas dos estrategias (como hacen los probadores más modernos), un sistema de razonamiento automático no surgirá de ellas.
El científico cognitivo Simon Dedeo de la Universidad Carnegie Mellon ayudó a demostrar que los humanos y las máquinas crean pruebas matemáticas de manera similar.
Además, muy poca gente acepta estas herramientas y la mayoría de los matemáticos no las utilizan ni las aprueban. “Este es un tema controvertido para los matemáticos”, dijo Dedeo. "A la mayoría de ellos no les gusta la idea".
Uno de los problemas difíciles abiertos en esta área es la cuestión de cuánto se puede automatizar el proceso de creación de pruebas. ¿Podrá el sistema generar una hipótesis interesante y probarla de una manera comprensible para la gente? Un conjunto de avances recientes de laboratorios de todo el mundo ofrecen formas de inteligencia artificial (IA) para responder a esta pregunta. Joseph Urban, del Instituto Checo de Informática, Robótica y Cibernética en Praga, está explorando varios enfoques que utilizan el aprendizaje automático para aumentar la efectividad de los probadores existentes. En julio, su grupomostró un conjunto de hipótesis y pruebas originales creadas y validadas por máquinas. En junio, un grupo de Google Research dirigido por Christian Szegedi publicó los resultados de los intentos de utilizar las fortalezas de los sistemas de procesamiento del lenguaje natural para hacer que la evidencia informática sea más similar en estructura y explicación a las humanas.
Algunos matemáticos ven a los probadores de teoremas como herramientas que pueden revolucionar la forma en que los estudiantes aprenden a escribir pruebas. Otros dicen que hacer que las computadoras escriban pruebas de matemáticas avanzadas es innecesario, si no imposible. Sin embargo, un sistema que puede predecir una hipótesis útil y probar un nuevo teorema puede lograr algo nuevo, una especie de versión de la máquina de comprensión, dijo Szegedi. Y esto sugiere la posibilidad de un razonamiento automático.
Máquinas útiles
Los matemáticos, lógicos y filósofos han debatido durante mucho tiempo qué parte de la realización de pruebas es de naturaleza humana, y el debate sobre la mecanización de las matemáticas continúa hoy en día, especialmente donde la informática se fusiona con las matemáticas puras.
Para los informáticos, los probadores de teoremas no son controvertidos. Proporcionan una manera clara de demostrar que el programa está funcionando, y los argumentos sobre la intuición y la creatividad son menos importantes que encontrar formas efectivas de resolver problemas. Por ejemplo, Adam Chlipala , un informático del Instituto de Tecnología de Massachusetts, ha desarrollado herramientas de prueba de teoremas que generanAlgoritmos criptográficos que protegen las transacciones en Internet, a pesar del hecho de que, por lo general, las personas crean tales algoritmos. Su código de grupo ya se utiliza en la mayoría de las comunicaciones en el navegador Google Chrome.
Emily Riel de la Universidad Johns Hopkins usa probadores de teoremas para capacitar a estudiantes y asistentes de computación.
“Puede tomar cualquier enunciado matemático y codificarlo con una herramienta, y luego combinar todos los argumentos y obtener una prueba de seguridad”, dijo Chlipala.
En matemáticas, los probadores de teoremas ayudaron a producir demostraciones complejas y computacionalmente intensivas que de otro modo habrían tomado miles de años-hombre matemáticos. Un ejemplo sorprendente es la hipótesis de Keplersobre el empaque más denso de bolas en el espacio tridimensional (históricamente, estas eran naranjas o balas de cañón). En 1998, Thomas Hales y su alumno, Sam Ferguson, completaron esta demostración utilizando una variedad de técnicas matemáticas computarizadas. El resultado fue tan engorroso - la prueba tomó 3 GB - que 12 matemáticos lo analizaron durante varios años antes de anunciar que estaban 99% seguros de su verdad.
La hipótesis de Kepler no es el único problema famoso resuelto por máquinas. Con el teorema de los cuatro colores, que afirma que cuatro colores siempre son suficientes para pintar cualquier mapa bidimensional en el que no hay dos áreas en contacto del mismo color, se descubrió en 1977 utilizando un programa de computadora que procesaba mapas de cinco colores, y demostró que todos se pueden convertir en cuatro colores. En 2016, tres matemáticos utilizaron un programa de computadora para probar el antiguo problema booleano de los trillizos pitagóricos , pero la primera versión de la prueba fue de 200 TB. Si tiene una conexión a Internet lo suficientemente rápida, puede descargarla en tres semanas.
Sentimientos encontrados
Estos ejemplos a menudo se promocionan como éxitos, pero también agregan su propio sabor a la controversia. El código de computadora que probó el teorema de los cuatro colores hace más de 40 años no pudo ser verificado por humanos. "Los matemáticos han debatido desde entonces si esto es una prueba o no", dijo el matemático Michael Harris de la Universidad de Columbia.
Muchos matemáticos, junto con Michael Harris de la Universidad de Columbia, cuestionan la necesidad de crear probadores de teoremas computarizados, y que esto último haría innecesarios a los matemáticos.
Otro descontento de los matemáticos está relacionado con el hecho de que si quieren usar probadores de teoremas, primero necesitan aprender a programar y luego descubrir cómo expresar su problema en un lenguaje comprensible por computadora, y todo esto los distrae de hacer matemáticas. “Para cuando reformule la pregunta de una manera adecuada para esta tecnología, resolveré este problema yo mismo”, dijo Harris.
Mucha gente simplemente no ve la necesidad de resolver teoremas. "Tienen su propio sistema, lápiz y papel, y funciona", dijo Kevin Buzzard., matemático del Imperial College de Londres, que cambió la dirección de la investigación hace tres años de las matemáticas puras a probadores de teoremas y demostraciones formales. “Las computadoras hacen cálculos asombrosos para nosotros, pero nunca resolvieron un problema difícil por sí mismas”, dijo. "Y hasta que eso suceda, los matemáticos no se lo creerán".
Pero Buzzard y otros creen que es posible que deban examinar más de cerca la tecnología. Por ejemplo, “las pruebas informáticas pueden no ser tan extrañas como pensamos”, dijo Dedeo. Recientemente, junto con Scott Viteri, un científico informático de Stanford, realizó ingeniería inversa de varias pruebas canónicas famosas (incluidas algunas de los PrincipiosEuclid) y docenas de pruebas generadas por un programa de computadora para probar los teoremas de Coq en busca de similitudes. Descubrieron que la estructura ramificada de las pruebas de máquina era notablemente similar a la de las pruebas hechas por humanos. Esta propiedad común, dijo, podría ayudar a los investigadores a encontrar una manera hacer que los programas de ayuda expliquen.
"Las pruebas de máquina pueden no ser tan crípticas como parecen", dijo Dedeo.
Otros dicen que los probadores de teoremas pueden ser herramientas útiles para enseñar tanto informática como matemáticas. En la Universidad Johns Hopkins, la matemática Emily Rielha desarrollado cursos en los que los estudiantes escriben pruebas utilizando probadores de teoremas. “Los hace muy organizados y piensan con claridad”, dijo. "Es posible que los estudiantes que escriben una prueba por primera vez no comprendan de inmediato lo que se les exige o no capten la estructura lógica".
Riel también dice que últimamente ha estado utilizando probadores de teoremas cada vez más en su trabajo. "No tienen que usarse todo el tiempo, y nunca reemplazarán el garabato en una hoja de papel", dijo, "pero el uso de asistentes de computadora para las pruebas ha cambiado mi idea de cómo escribir pruebas".
Los probadores de teoremas también ofrecen una manera de mantener las matemáticas justas. En 1999, un matemático soviético, ruso y estadounidenseVladimir Alexandrovich Voevodsky , descubrió un error en una de sus pruebas. Desde entonces hasta su muerte en 2017, promovió activamente el uso de computadoras para verificar pruebas. Hales dijo que él y Ferguson encontraron cientos de errores en sus pruebas originales probándolos con computadoras. Incluso los primeros teoremas de los Elementos de Euclides no son ideales. Si una máquina puede ayudar a los matemáticos a evitar tales errores, ¿por qué no aprovecharla? Harris ofreció una objeción práctica a esta propuesta, sin embargo, no se sabe cuán razonable: si los matemáticos tienen que dedicar tiempo a formalizar las matemáticas para que una computadora las entienda, no podrán dedicar ese tiempo a nuevas matemáticas.
Sin embargo, Timati Gowers, matemático y matemático ganador del premio Cambridge Fields, quiere ir aún más lejos: imagina cómo los probadores de teoremas reemplazarán a los revisores humanos en las principales revistas en el futuro. "Veo cómo esto puede convertirse en una práctica estándar: si desea que su trabajo sea aceptado, debe ejecutarlo a través de un revisor automático".
Conversación con computadoras
Antes de que las computadoras puedan probar o desarrollar evidencia, los investigadores primero deben superar un obstáculo importante: la barrera de comunicación entre los lenguajes de los humanos y las computadoras.
Los probadores de teoremas de hoy se han diseñado sin tener en cuenta la compatibilidad con los matemáticos. El primer tipo, ATP, se usaba comúnmente para probar la veracidad de una declaración, a menudo probando todas las opciones posibles. Pregúntele a la ATP si es posible viajar de Miami a Seattle, y probablemente pasará por todas las ciudades a las que conducen las carreteras de Miami, y al final encontrará una ciudad que lleve a Seattle.
Timati Gowers de la Universidad de Cambridge cree que los probadores de teoremas reemplazarán algún día a los revisores humanos
Usando ATP, el programador puede codificar todas las reglas o axiomas y luego preguntarse si una hipótesis particular sigue esas reglas. Y luego la computadora hace todo el trabajo. "Simplemente ingresa la hipótesis que desea probar y espera obtener una respuesta", dijo Daniel Huang, un científico de la computación que recientemente dejó UC Berkeley para comenzar una startup.
Pero hay un problema: ATP no explica su trabajo. Todos los cálculos se realizan dentro de la máquina y, para una persona, parecen una larga secuencia de ceros y unos. Huang dijo que era imposible mirar la prueba y probar el razonamiento, ya que todo parece un montón de datos aleatorios. “Nadie puede mirar esa evidencia y decir: todo está claro”, dijo.
La segunda categoría, el ITP, tiene enormes conjuntos de datos que contienen decenas de miles de teoremas y demostraciones con las que pueden comprobar la precisión de una demostración. A diferencia de los ATP, que funcionan dentro de una caja negra que simplemente emite respuestas, los ITP requieren interacción y, a veces, dirección de una persona, por lo que no son tan inaccesibles. "Una persona puede sentarse y averiguar qué técnicas se están utilizando para probar", dijo Huang. Tal evidencia fue estudiada por Dedeo y Viteri.
En los últimos años, los ITP se han vuelto cada vez más populares. En 2017, la trinidad que probó el problema booleano de los trillizos pitagóricos utilizó un ITP llamado Coq para crear y probar una versión formal de su prueba. En 2005, Georges Gontier de Microsoft Research Cambridge utilizó Coq para formalizar el teorema de los cuatro colores. Hales también usó ITPs llamados HOL Light e Isabelle para probar formalmente la conjetura de Kepler (HOL significa lógica de orden superior).
Hoy, la vanguardia de este campo está tratando de combinar el aprendizaje con el razonamiento. ATP a menudo se combina con ITP para integrar el aprendizaje automático para mejorar el rendimiento de ambas técnicas. Los expertos creen que los programas ATP / ITP pueden utilizar el razonamiento deductivo e incluso intercambiar ideas matemáticas de la misma manera que lo hacen los humanos, o al menos de manera similar.
Límites del razonamiento
Joseph Urban cree que este enfoque combinado puede casar el razonamiento deductivo e inductivo, que es necesario para obtener evidencia. Su grupo creó probadores de teoremas basados en el aprendizaje automático, lo que permite que las computadoras aprendan de la experiencia por sí mismas. En los últimos años, han estado explorando el poder de las redes neuronales, capas de unidades informáticas que ayudan a las máquinas a procesar la información de una manera más o menos similar a cómo funcionan las neuronas de nuestro cerebro. En julio, su grupo informó nuevas hipótesis generadas por una red neuronal entrenada en la demostración de teoremas.
En parte, Urban se inspiró en el trabajo de Andrei Karpaty, quien hace varios años entrenó una red neuronal para producir disparates matemáticos que parecían convincentes para los no profesionales. Pero Urban no necesitaba las tonterías: él y el grupo desarrollaron su propia herramienta que busca pruebas, habiéndose entrenado en millones de teoremas. Utilizaron la red para generar nuevas hipótesis y probar su validez con un programa ATP llamado E.
La red ha emitido más de 50.000 nuevas fórmulas, aunque se han repetido decenas de miles. “Parece que todavía no podemos probar hipótesis más interesantes”, dijo Urban.
Szegedi, de Google Research, ve el problema del razonamiento automático en la evidencia informática como parte de un campo mucho más amplio: el procesamiento del lenguaje natural, que incluye el reconocimiento de patrones en el uso de palabras y oraciones. El reconocimiento de patrones también es la idea central de la visión por computadora, en la que Szegedi trabajó anteriormente en Google. Como otros grupos, su equipo quiere crear probadores de teoremas que puedan buscar pruebas útiles y explicarlas.
Inspirado por el rápido desarrollo de herramientas de inteligencia artificial como AlphaZero, el software de DeepMind que puede vencer a los humanos en el ajedrez, el go y el shogi, el grupo Szegedi quiere utilizar los últimos avances en el reconocimiento del lenguaje para registrar evidencia. Dijo que los modelos de lenguaje pueden demostrar un razonamiento matemático sorprendentemente preciso.
Su grupo en Google Research describió recientemente una forma de usar modelos de lenguaje, que las redes neuronales usan a menudo, para generar nueva evidencia. Después de entrenar al modelo para reconocer la estructura de árbol de los teoremas probados, lanzaron un experimento gratuito, simplemente pidiendo a las redes neuronales que generaran y probaran teoremas sin supervisión. De las miles de hipótesis generadas, el 13% resultó demostrable y nuevo (sin repetir otros teoremas en la base de datos). Dijo que tal experimento dice que las redes neuronales pueden aprender, en cierto sentido, a comprender cómo se ve la evidencia.
"Las redes neuronales son capaces de desarrollar una apariencia artificial de intuición", dijo Szegedi.
Por supuesto, todavía no está claro si estos intentos cumplirán la profecía de Cohen hace 40 años. Gowers dijo que cree que las computadoras pueden superar a los matemáticos en razonamiento para el 2099. Al principio, dice, los matemáticos disfrutarán de una edad de oro, “cuando hacen cosas interesantes y las computadoras son aburridas. Pero creo que no durará mucho ".
Después de todo, si las máquinas continúan desarrollándose cada vez más y tienen acceso a una gran cantidad de datos, deben aprender a hacer cosas muy bien e interesantes. “Aprenderán a hacer sus propias solicitudes”, dijo Gowers.
Harris no está de acuerdo. No cree que las pruebas informáticas sean necesarias, o que acabarán "haciendo innecesarios a los matemáticos humanos". Si los informáticos, dice, algún día pueden programar la intuición sintética, todavía no competirá con la intuición humana. "Incluso si las computadoras entienden, no entenderán en el sentido humano".