Un recuerdo definitorio de mi último año de secundaria fue un examen de matemáticas de nueve horas con solo seis preguntas. Seis de los mejores anotadores ganaron espacios en el equipo de los Estados Unidos para la Olimpiada Internacional de Matemáticas (OMI), la competencia de matemáticas más antigua del mundo para estudiantes de secundaria. No hice el corte, pero de todos modos me convertí en un profesor de matemáticas titular.
La Olimpiada de este año, celebrada el mes pasado en la costa de Sunshine de Australia, tuvo un espectáculo secundario inusual. Mientras que 110 estudiantes de todo el mundo fueron a trabajar en problemas de matemáticas complejas con lápiz y papel, varias compañías de IA probaron en silencio nuevos modelos en desarrollo en una aproximación computarizada del examen. Justo después de las ceremonias de clausura, Opadai y más tarde Google DeepMind anunció que sus modelos obtuvieron medallas de oro (no oficiales) para resolver cinco de los seis problemas. Investigadores como Sébastien Bubeck de Operai celebraron los éxitos de estos modelos como un “Momento de aterrizaje de la luna“Por la industria.
¿Pero son ellos? Va a reemplazar la IA matemáticos profesionales? Todavía estoy esperando la prueba.
Sobre el apoyo al periodismo científico
Si está disfrutando de este artículo, considere apoyar nuestro periodismo galardonado con suscripción. Al comprar una suscripción, está ayudando a garantizar el futuro de las historias impactantes sobre los descubrimientos e ideas que dan forma a nuestro mundo hoy.
La exageración sobre los resultados de IA de este año es fácil de entender porque la Olimpiada es difícil. A saber, en mi último año de secundaria, dejé de lado el cálculo y el álgebra lineal para centrarme en los problemas al estilo de la Olimpiada, que eran más un desafío. Además, los modelos de vanguardia que todavía estaban en desarrollo lo hicieron mucho mejor en el examen que los modelos comerciales que ya existen. En un concurso paralelo administrado por Matharena.aiGéminis 2.5 Pro, Grok 4, O3 High, O4-Mini High y Deepseek R1 Todos no pudieron producir una sola solución completamente correcta. Muestra que los modelos de IA se están volviendo más inteligentes, sus capacidades de razonamiento mejoran dramáticamente.
Sin embargo, todavía no estoy preocupado.
Los últimos modelos acaban de obtener una buena calificación en una sola prueba, al igual que muchos de los estudiantes, y una comparación cara a cara no es del todo justa. Los modelos a menudo emplean un “mejor denorteEstrategia, generando múltiples soluciones y luego calificándose para seleccionar la más fuerte. Esto es similar a que varios estudiantes trabajen de forma independiente, luego se reúnan para elegir la mejor solución y enviar solo esa. Si a los concursantes humanos se les permitiera esta opción, sus puntajes probablemente también mejorarían.
Otros matemáticos están advirtiendo de manera similar contra la exageración. Medallista de OMI de oro Terence Tao (actualmente un matemático en la Universidad de California, Los Ángeles) anotado en Mastodonte Que lo que AI puede hacer depende de cuál sea la metodología de prueba. El presidente de la OMI, Gregor Dolinar, dijo que la organización “no se puede validar los métodos [used by the AI models]incluida la cantidad de cómputo utilizada o si hubo alguna participación humana, o si los resultados se pueden reproducir. “
Además, las preguntas del examen de la OMI no se comparan con los tipos de preguntas que los matemáticos profesionales intentan responder, donde puede llevar nueve años, en lugar de nueve horas, resolver un problema en la frontera de la investigación matemática. Como Kevin Buzzard, profesor de matemáticas en el Imperial College de Londres, dijo en un foro en línea: “Cuando llegué a Cambridge UK como un pregrado que agarraba mi medalla de oro de la Omo, no estaba en posición de ayudar a ninguno de los matemáticos de investigación allí”.
En estos días, la investigación matemática puede tomar más de una vida útil para adquirir la experiencia adecuada. Al igual que muchos de mis colegas, he tenido la tentación de intentar “probar el ambiente”, tener una conversación matemática con un LLM como lo haría con un colega, preguntando “¿Es cierto que …” seguido de una conjetura matemática técnica. El chatbot a menudo suministra un argumento claramente articulado que, en mi experiencia, tiende a ser correcto cuando se trata de temas estándar, pero sutilmente incorrecto en la vanguardia. Por ejemplo, cada modelo que he preguntado ha cometido el mismo error sutil al suponer que la teoría de los idempotentes se comporta lo mismo para las categorías débiles de dimensiones infinitas que para las ordinarias, algo que los expertos humanos (confíen en esto) en mi campo sabe que es falso.
Nunca confiaré en un LLM, que en su núcleo solo predice qué texto vendrá a continuación en una serie de palabras, basada en lo que hay en su conjunto de datos, para proporcionar una prueba matemática de que no puedo verificarme.
La buena noticia es que tenemos un mecanismo automatizado para determinar si se pueden confiar en pruebas. Las herramientas relativamente recientes llamadas “asistentes de prueba” son programas de software (no usan IA) diseñados para verificar si un argumento lógico demuestra el reclamo establecido. Están atrayendo cada vez más atención a los matemáticos como Tao, Buzzard y yo que queremos más seguridad de que nuestras propias pruebas son correctas. Y ofrecen el potencial para ayudar a democratizar las matemáticas e incluso mejorar la seguridad de la IA.
Supongamos que recibí una carta, en letra desconocida, de Erode, una ciudad en Tamil Nadu, India, que pretende contener una prueba matemática. Tal vez sus ideas son brillantes, o tal vez no son sensibles. Tendría que pasar horas estudiando cuidadosamente cada línea, asegurándome de que el argumento fluyó paso a paso, antes de poder determinar si las conclusiones son verdaderas o falsas.
Pero si el texto matemático se escribió en una sintaxis de computadora apropiada en lugar de lenguaje natural, un asistente de prueba podría verificar la lógica por mí. Un matemático humano, como yo, solo necesitaría comprender el significado de los términos técnicos en la declaración del teorema. En el caso de Srinivasa Ramanujan, un genio matemático generacional que provocó Erode, un experto se tomó el tiempo para descifrar cuidadosamente su carta. En 1913, Ramanujan escribió al matemático británico GH Hardy con sus ideas. Afortunadamente, Hardy reconoció la brillantez de Ramanujan y lo invitó a Cambridge a colaborar, lanzando la carrera de uno de los “grandes” matemáticos de todos los tiempos.
Lo interesante es que algunos de los concursantes de AI IMO presentaron sus respuestas en el idioma del Asistente Lean Computer Proof para que el programa de computadora pudiera verificar automáticamente los errores en su razonamiento. Una nueva empresa llamada Harmonic publicó pruebas formales generadas por su modelo para cinco de los seis problemas, y el byteed logró un rendimiento de nivel de plata mediante plateado resolviendo cuatro de los seis problemas. Pero las preguntas tenían que escribirse para acomodar las limitaciones de lenguaje de los modelos, y aún necesitaban días para resolverlo.
Aún así, las pruebas formales son únicamente confiables. Si bien se lleva a cabo los llamados modelos de “razonamiento” que rompan los problemas en pedazos y expliquen su “pensamiento” paso a paso, es probable que el resultado produzca un argumento que suene lógico pero no es, como para constituir una prueba genuina. Por el contrario, un asistente de prueba no aceptará una prueba a menos que sea completamente precisa y completamente rigurosa, lo que justifica cada paso en su cadena de pensamiento. En algunas circunstancias, una solución de onda o aproximación a mano es lo suficientemente buena, pero cuando la precisión matemática es importante, debemos exigir que las pruebas generadas por IA sean formalmente verificables.
No todas las aplicaciones de IA generativa son tan blancos y negros, donde los humanos con la experiencia adecuada pueden determinar si los resultados son correctos o incorrectos. En la vida, hay mucha incertidumbre y es fácil cometer errores. Como aprendí en la escuela secundaria, una de las mejores cosas de las matemáticas es el hecho de que puede demostrar definitivamente que algunas ideas están mal. Así que estoy feliz de que una IA intente resolver mis problemas matemáticos personales, pero solo si los resultados son formalmente verificables. Y todavía no estamos del todo allí.
Este es un artículo de opinión y análisis, y las opiniones expresadas por el autor o los autores no son necesariamente las de Científico americano.
Es hora de defender la ciencia
Antes de cerrar la página, debemos pedir su apoyo. Científico americano ha servido como defensor de la ciencia y la industria durante 180 años, y creemos que en este momento es el momento más crítico en esa historia de dos siglos.
No estamos pidiendo caridad. Si usted convertirse en un suscriptor digital, impreso o ilimitado Para Scientific American, puede ayudar a garantizar que nuestra cobertura se centre en una investigación y descubrimiento significativos; que tenemos los recursos para informar sobre las decisiones que amenazan a los laboratorios en los Estados Unidos; y que apoyamos tanto el futuro como los científicos que trabajan en un momento en que el valor de la ciencia en sí misma a menudo no se reconoce. Haga clic aquí para suscribirse.