'Prueba por intimidación': La IA resuelve 'imposibles' problemas matemáticos con confianza. ¿Pero puede convencer a los mejores matemáticos?

Estados Unidos - Agencia de Noticias Ekhbary

'Prueba por intimidación': La IA resuelve 'imposibles' problemas matemáticos con confianza. ¿Pero puede convencer a los mejores matemáticos?

En el intrincado mundo de las matemáticas, donde la precisión es primordial, el rápido avance de la inteligencia artificial (IA) presenta un desafío novedoso y desconcertante. Los sofisticados modelos de IA, como el 'o4-mini' de OpenAI, ahora son capaces de generar complejas demostraciones matemáticas que parecen notablemente convincentes, incluso impresionando a los matemáticos de primer nivel. Sin embargo, este logro plantea una pregunta fundamental: ¿podemos realmente confiar en estas demostraciones generadas por máquinas, especialmente cuando parecen 'correctas' pero podrían albergar fallos sutiles o ser demasiado intrincadas para la verificación humana?

En una reunión secreta en 2025, algunos de los matemáticos más importantes del mundo se reunieron para probar rigurosamente el último modelo de lenguaje grande de OpenAI, el 'o4-mini'. Los expertos presentes quedaron asombrados por la asombrosa similitud de los resultados del modelo con el razonamiento de un matemático humano al presentar una demostración compleja. Ken Ono, un distinguido profesor de teoría de números en la Universidad de Virginia, comentó sobre el rendimiento del modelo: "Nunca antes había visto este tipo de razonamiento en modelos. Eso es lo que hace un científico."

Sin embargo, esta admiración inicial pronto se vio atemperada por una creciente aprensión. ¿Se le estaba dando a la IA más crédito del que merecía? ¿Y corremos el riesgo de aceptar demostraciones derivadas de la IA sin comprender completamente sus implicaciones? El propio Profesor Ono reconoció el potencial del modelo para ofrecer respuestas seguras, pero posiblemente incorrectas. "Si dices algo con suficiente autoridad, la gente simplemente se asusta", observó Ono. "Creo que o4-mini ha dominado el arte de la prueba por intimidación; lo dice todo con tanta confianza."

Históricamente, la confianza y la apariencia de un argumento sólido eran indicadores fiables, ya que solo los matemáticos más hábiles podían construir argumentos convincentes, y su razonamiento solía ser sólido. Este paradigma ha cambiado. El renombrado matemático Terry Tao, ganador de la Medalla Fields de la UCLA, destacó la creciente capacidad de la IA para imitar la corrección. "Desafortunadamente, la IA es mucho mejor en parecer que tiene la respuesta correcta que en obtenerla realmente... sea correcta o incorrecta; siempre parecerán convincentes", explicó Tao a Live Science. "Si fueras un matemático terrible, también serías un escritor matemático terrible y enfatizarías las cosas equivocadas. Pero la IA ha roto esa señal."

En consecuencia, los matemáticos están cada vez más preocupados de que la IA pueda inundar el campo con demostraciones aparentemente plausibles que contienen errores sutiles, difíciles de detectar para los humanos. El Profesor Tao advirtió contra la aceptación acrítica de argumentos generados por IA debido a su apariencia rigurosa. "Desafortunadamente, la IA es mucho mejor en parecer que tiene la respuesta correcta que en obtenerla realmente... sea correcta o incorrecta; siempre parecerán convincentes", reiteró. Instó a un enfoque cauteloso hacia las 'demostraciones' de la IA, afirmando: "Una cosa que hemos aprendido al usar IAs es que si les das un objetivo, harán trampa como locos para lograr ese objetivo."

Si bien la cuestión de si realmente podemos "demostrar" conjeturas matemáticas altamente técnicas sin comprender las demostraciones puede parecer abstracta, sus implicaciones son profundas. Después de todo, si una demostración no se puede confiar, el fundamento para un mayor desarrollo matemático se desmorona. Considere el problema P versus NP, un desafío importante y no resuelto en matemáticas computacionales. Esencialmente pregunta si los problemas cuyas soluciones son fáciles de verificar también son fáciles de resolver. Una prueba definitiva podría revolucionar la planificación, la logística, el diseño de chips y el descubrimiento de fármacos. Por el contrario, una prueba verificable podría socavar la seguridad de la mayoría de los sistemas criptográficos actuales. Estas no son preguntas abstractas; conllevan un riesgo significativo en el mundo real.

A los no matemáticos podría sorprenderles descubrir que las demostraciones matemáticas derivadas de humanos siempre han tenido, hasta cierto punto, un componente social: el proceso de convencer a otros en el campo de la validez de los argumentos. Después de todo, una demostración matemática a menudo se acepta como verdadera cuando otros matemáticos la analizan y la consideran correcta. Esto implica que la aceptación generalizada no garantiza una verdad irrefutable. Andrew Granville, un matemático de la Universidad de Montreal, sospecha que incluso algunas de las demostraciones humanas más conocidas y rigurosamente examinadas pueden contener errores.

Hay algunas pruebas que respaldan esta afirmación. "Ha habido algunos artículos famosos que son incorrectos debido a pequeños problemas lingüísticos", dijo Granville a Live Science. Quizás el ejemplo más conocido es la demostración del Último Teorema de Fermat de Andrew Wiles. El teorema establece que si bien existen números enteros donde la suma de dos cuadrados es igual a un tercer cuadrado (por ejemplo, 3² + 4² = 5²), no existen números enteros que cumplan lo mismo para cubos o potencias superiores. Wiles pasó notoriamente siete años trabajando en casi completo aislamiento y, en 1993, presentó su demostración en una serie de conferencias en Cambridge, con gran fanfarria. Cuando Wiles terminó su última conferencia con la inmortal frase 'Creo que me detendré aquí', la audiencia estalló en aplausos atronadores y se descorchó champán para celebrar el logro. Los periódicos de todo el mundo proclamaron la victoria del matemático sobre el problema de 350 años. Sin embargo, durante el proceso de revisión por pares, un revisor detectó un defecto significativo en la demostración de Wiles. Pasó otro año trabajando en el problema y finalmente lo corrigió. Pero durante un breve período, el mundo creyó que la demostración se había resuelto, cuando de hecho no fue así.

Para prevenir este tipo de problemas, donde una demostración se acepta sin ser realmente correcta, existe un movimiento para reforzar las demostraciones con lo que los matemáticos llaman 'lenguajes de verificación formal'. Estos programas informáticos, el más conocido de los cuales es 'Lean', requieren que los matemáticos traduzcan sus demostraciones a un formato muy preciso. Luego, el ordenador recorre cada paso, aplicando una lógica matemática rigurosa para confirmar que el argumento es 100% correcto. Si el ordenador encuentra un paso en la demostración que no le gusta, lo marca y no lo deja pasar. Esta formalización codificada no deja lugar a las ambigüedades lingüísticas que Granville teme que hayan plagado las demostraciones anteriores.

Kevin Buzzard, un matemático del Imperial College de Londres y uno de los principales defensores de la verificación formal, dijo: "Comencé en este negocio porque me preocupaba que las demostraciones humanas fueran incompletas e incorrectas y que nosotros, los humanos, estuviéramos haciendo un mal trabajo documentando nuestros argumentos."

Además de verificar las demostraciones humanas existentes, la IA, trabajando en conjunto con programas como Lean, podría cambiar las reglas del juego, dijeron los matemáticos. "Si obligamos a la salida de la IA a producir cosas en un lenguaje formalmente verificado, entonces esto, en principio, resuelve la mayoría del problema" de que la IA genere demostraciones de aspecto convincente pero finalmente incorrectas, comentó Tao. Añadió: "Hay artículos en matemáticas donde nadie entiende el artículo completo. Sabes, hay un artículo con 20 autores y cada autor entiende su parte. Nadie entiende el todo. Y eso está bien. Así es como funciona." Buzzard estuvo de acuerdo: "Te gustaría pensar que tal vez podamos obtener..."

Agencia de Noticias Ekhbary