Los matemáticos exploran ideas proponiendo conjeturas y probándolas con teoremas. Durante siglos, construyeron estas demostraciones línea por línea, y la mayoría de los investigadores matemáticos todavía trabajan así hoy. Pero la inteligencia artificial está preparada para cambiar fundamentalmente este proceso. Los asistentes de inteligencia artificial apodados “copilotos” están comenzando a ayudar a los matemáticos a desarrollar pruebas; con una posibilidad real de que algún día esto permita a los humanos responder algunos problemas que actualmente están fuera del alcance de nuestra mente.
En el Instituto de Tecnología de California se está desarrollando un tipo prometedor de copiloto de IA. Puede proponer automáticamente los siguientes pasos en una demostración y ayudar a completar objetivos matemáticos intermedios, ayudando a construir el tejido conectivo lógico entre pasos más grandes. “Si estoy desarrollando una prueba, este nuevo copiloto me da múltiples sugerencias para seguir adelante”, dice Animashree Anandkumar, profesor de informática y ciencias matemáticas en Caltech. Junto con su equipo, Anandkumar presentó al copiloto de IA en un papel preimpreso recienteque aún no ha sido revisado por pares. Lo más importante, dice, es que esas sugerencias “serán todas correctas”.
El copiloto es un modelo de lenguaje grande (LLM), el mismo tipo de sistema de aprendizaje automático detrás de ChatGPT de OpenAI y Gemini de Google. Si bien su entrenamiento es diferente, también es similar a la tecnología que impulsa AlphaProof y AlphaGeometry 2 de Google, los cuales generaron pruebas matemáticas complejas a gran escala. medalla de plata estándar en la Olimpiada Internacional de Matemáticas (OMI) de este año para los mejores estudiantes de secundaria del mundo. Y aunque los LLM pueden generar lo que es, en un sentido técnico, “tonterías”. Las sugerencias erróneas de un copiloto son revisadas y rechazadas. En el caso del copiloto de Caltech, eso se debe al software en el que opera la IA, llamado Lean, que utiliza una lógica matemática rigurosa para detectar declaraciones válidas.
Sobre el apoyo al periodismo científico
Si está disfrutando este artículo, considere apoyar nuestro periodismo galardonado al suscribiéndose. Al comprar una suscripción, ayudas a garantizar el futuro de historias impactantes sobre los descubrimientos y las ideas que dan forma a nuestro mundo actual.
Prueba por código
En los últimos años, Lean se ha vuelto cada vez más popular entre una base de usuarios pequeña pero creciente. El software de código abierto permite a los matemáticos ingresar a sus matemáticas mediante codificación, un proceso conocido como formalización. ¿Cuál es la ventaja? Nunca está mal. En Lean y otras aplicaciones de ayuda a la prueba, el software verifica automáticamente la precisión de las declaraciones matemáticas. Esto está a un mundo de distancia de las matemáticas tradicionales, las llamadas informales, donde los revisores y colegas auditan minuciosamente páginas de tales declaraciones. Ese proceso es propenso a errores humanos y se pasan por alto los errores.
Si está escribiendo una prueba con la ayuda del copiloto de Caltech, puede hacer clic en un botón para solicitar nuevas líneas del lenguaje de programación Lean para representar las matemáticas con las que está trabajando. Varias opciones, que Anandkumar llama “sugerencias tácticas”, aparecerán en el lado derecho de la pantalla; luego simplemente elige la opción que te parezca más apropiada. Si su prueba se dirige en una dirección que tiene conclusiones intermedias obvias o bien conocidas, el copiloto también puede sugerir cómo completar esa trayectoria.
“No hay ningún problema de confianza” con Lean porque el software comprueba el trabajo, afirma Martin Hairer, profesor de matemáticas puras en el Instituto Federal Suizo de Tecnología en Lausana y en el Imperial College de Londres. Aún así, muchos académicos aún no lo han adoptado. “Es difícil de utilizar porque hay que introducir todas las matemáticas como código”, afirma Hairer. Codificar en Lean requiere ingresar detalles que se omitirían al escribir un artículo, señala, por lo que podrían ser necesarias varias páginas de código para mostrar lo que es evidentemente verdadero u obvio.
Pero Hairer, que no participa en el proyecto Caltech, cree que los copilotos de IA acabarán eliminando todo ese trabajo pesado. “Una vez que se presenta una afirmación que es obvia para la mayoría de los matemáticos, un LLM debería poder generar el código correspondiente”, dice, y agrega que este proceso más rápido podría “posiblemente atraer a una nueva generación de matemáticos hacia Lean”.
Anandkumar también predice que más investigadores adoptarán las matemáticas formales asistidas por IA. “Hoy en día, cuando hablo con jóvenes matemáticos o incluso con estudiantes universitarios al principio de sus carreras, veo que están familiarizados con estos sistemas de IA”, afirma. “Harán lo que sea necesario para que el trabajo sea más rápido y más fácil para obtener una ventaja competitiva”.
Transformaciones Matemáticas
Antes de que la comunidad matemática internacional adopte herramientas de inteligencia artificial de manera significativa, estas plataformas deberán volverse mucho más poderosas. Con su medalla de plata en la OMI de este año, AlphaProof y AlphaGeometry 2 de Google han mostrado resultados notables. Pero todavía no han alcanzado el nivel que los investigadores matemáticos necesitan para obtener ayuda con demostraciones complejas; los humanos, en ese sentido, siguen siendo los matemáticos más capaces.
Sin embargo, “pronto habrá sistemas que se acerquen a ese nivel”, afirma David Silver, vicepresidente de aprendizaje por refuerzo de Google DeepMind. “Creo que esto esencialmente elevará a los matemáticos humanos a un lugar donde podrán operar y reflexionar sobre ideas a un nivel mucho más alto”. Las matemáticas están empezando a transformarse, dice, tal como lo hizo cuando se inventó la calculadora electrónica. “En la época anterior a la calculadora, había una amplia gama de matemáticas que eran extremadamente laboriosas y requerían mucho esfuerzo”, dice. “Creo que ahora estamos en esa etapa con las pruebas, y en el futuro veremos pruebas muy complejas que la IA resolverá automáticamente”.
Colaboración a través de IA
La adopción de copilotos de IA también cambiará la forma en que los matemáticos trabajan entre sí. Normalmente operan solos o en pequeños grupos. Compañeros de confianza evalúan sus pruebas pieza por pieza. Pero los asistentes formales de IA podrían capacitar a grupos más grandes de colaboradores humanos para abordar los problemas más importantes dividiéndolos en subproblemas. Cada parte se distribuiría para ser resuelta por diferentes equipos de asociaciones especializadas entre IA y humanos. “Las matemáticas se consideran una tarea solitaria, especialmente en los medios populares, pero ahora parece que la IA se convertirá en el facilitador de la colaboración entre matemáticos”, afirma Anandkumar.
Los matemáticos son generalmente optimistas en cuanto a que los copilotos de IA pronto darán un impulso a los expertos humanos, permitiéndoles invertir su tiempo en problemas más complejos y difíciles. Por ejemplo, en los próximos años las asociaciones entre IA y humanos podrían intentar resolver problemas notoriamente difíciles del Premio del Milenio, tal vez incluso algo tan desafiante como P versus NPuna pregunta de larga data en la informática teórica que pregunta si todo problema cuya solución pueda verificarse rápidamente también puede resolverse rápidamente.
“Ahí es donde nos encontraremos muy pronto”, dice Silver, mientras considera la idea de resolver estas cuestiones. “Problemas tan complejos como ‘P versus NP’, o algo así de difícil, están mucho más allá de donde nos encontramos hoy en términos de siquiera saber cómo empezar”, afirma. “Pero me imagino que, tal vez en unos tres años, podríamos estar en camino de algo así”.