Una investigación desarrollada por Physical Superintelligence asegura haber demostrado en tres días la conjetura de Aaronson-Ambainis, una pregunta abierta desde hace casi dos décadas. El resultado, formalizado con ayuda de un verificador matemático, abre nuevas posibilidades para la investigación científica y plantea interrogantes sobre la autoría, la confianza y la validación del conocimiento
Imaginemos una fila de interruptores. Cada uno puede encenderse o apagarse y, según la combinación elegida, una pequeña aguja cambia de posición sobre una escala. Algunos interruptores apenas modifican su lectura; otros provocan variaciones considerables. Aunque parezca un ejercicio sencillo, detrás de ese mecanismo se esconde una de las preguntas que durante años han ocupado a investigadores de la matemática y la computación cuántica: ¿puede identificarse siempre alguna variable capaz de influir de manera apreciable en el resultado de una operación matemática?
La respuesta a esa pregunta acaba de recibir una demostración que podría tener consecuencias para nuestra comprensión de los ordenadores cuánticos. Este viernes 6 de noviembre, la empresa Physical Superintelligence (PSI) anunció que su sistema interno de investigación había encontrado una prueba para la conjetura de Aaronson-Ambainis, un problema que permanecía abierto desde 2008.
Según explicó la compañía, el sistema consiguió completar la demostración durante su tercer día de trabajo. Para llegar a ella utilizó instancias de un modelo de inteligencia artificial desarrollado por Anthropic que todavía no se ha presentado al público. El resultado también pasó por Lean, un programa especializado que comprueba demostraciones matemáticas paso a paso.
La noticia llama la atención por la rapidez del hallazgo, pero su importancia va mucho más allá del tiempo empleado. Por primera vez, un sistema de investigación basado en inteligencia artificial participa de forma central en la solución de una conjetura de gran relevancia para la teoría de la computación cuántica. Y lo hace mediante un procedimiento que combina modelos de lenguaje, herramientas matemáticas, verificación informática y supervisión humana.
Para comprender el alcance del resultado conviene detenerse en la pregunta original. Los ordenadores cuánticos prometen resolver determinados problemas con una rapidez que las computadoras convencionales no pueden alcanzar. Sin embargo, esa ventaja no aparece en cualquier tarea.
Uno de los ejemplos más conocidos procede del trabajo del matemático Peter Shor, quien en 1994 presentó un algoritmo cuántico capaz de factorizar números enteros grandes con una eficiencia muy superior a la de los métodos clásicos conocidos. Su propuesta aprovechaba una propiedad matemática particular: la existencia de patrones repetitivos que el ordenador cuántico podía detectar.
La estructura del problema es importante. En determinadas operaciones, las simetrías, las periodicidades y otras regularidades permiten que una máquina cuántica encuentre soluciones con menos consultas a los datos. Pero ¿qué ocurre cuando las entradas son aleatorias y no presentan patrones aprovechables? ¿Podría una computadora cuántica conservar una ventaja exponencial incluso en esas circunstancias?
Scott Aaronson y Andris Ambainis formularon una conjetura para abordar esa cuestión. Su trabajo apareció como prepublicación en 2009 y llegó a la revista Theory of Computing en 2014, bajo el título The Need for Structure in Quantum Speedups. Los investigadores plantearon que determinados polinomios matemáticos, aun cuando dependan de numerosas variables, deben contener al menos una cuya modificación influya de forma apreciable en el resultado.
Un polinomio, explicado sin recurrir a demasiadas fórmulas, funciona como una operación que combina números y variables mediante sumas, multiplicaciones y otras relaciones. En el problema estudiado, las variables representan bits, es decir, valores que pueden ser cero o uno. La influencia de una variable mide cuánto cambia el resultado promedio cuando se invierte su valor.
La conjetura sostiene que, bajo ciertas condiciones, siempre habría una variable con suficiente influencia. Esa propiedad permitiría a un ordenador clásico identificar qué partes de la información necesita consultar para imitar, con un margen de error pequeño, el comportamiento de un algoritmo cuántico.
La consecuencia resulta significativa: para determinadas preguntas de respuesta afirmativa o negativa y cuando las entradas son aleatorias, una computadora convencional podría reproducir el resultado de una cuántica sin necesitar una cantidad exponencial de consultas adicionales. La ventaja cuántica, por tanto, no aparecería de manera generalizada. Dependería de que el problema presentara una estructura matemática que la máquina pudiera aprovechar.
El artículo original de Aaronson y Ambainis ya había establecido esa conexión entre la conjetura y los límites de las aceleraciones cuánticas. La demostración anunciada por PSI permitiría cerrar una de las piezas matemáticas que faltaban para sostener ese razonamiento. Conviene precisar, sin embargo, que el resultado se refiere al número de consultas a los datos dentro de un modelo teórico, no al tiempo total que necesita cualquier ordenador para ejecutar una tarea. Tampoco elimina las ventajas cuánticas en problemas estructurados.
El aspecto más llamativo del anuncio reside en el procedimiento utilizado. La empresa atribuye el resultado a un sistema de investigación construido por David Turturean, miembro de su equipo técnico, quien definió el problema, desarrolló la infraestructura que permitió trabajar con los modelos y supervisó el proceso de elaboración del manuscrito.
PSI no ha revelado cuál fue el modelo de Anthropic empleado. Sí reconoce que los modelos de inteligencia artificial produjeron los enunciados matemáticos, el primer borrador de la investigación y la formalización de la demostración. Turturean revisó el artículo y asumió la responsabilidad por su corrección.
Aquí entra en escena Lean, una herramienta que merece una explicación aparte. Se trata de un asistente de demostraciones matemáticas que permite escribir una prueba en un lenguaje formal y comprobar si cada paso se desprende de las reglas y definiciones anteriores.
Para entender su función, podemos compararlo con un árbitro que no acepta una afirmación por la autoridad de quien la formula. Cada movimiento debe cumplir las reglas del juego. Si un paso lógico carece de fundamento, el sistema lo rechaza.
En matemáticas, esta comprobación tiene un valor considerable. Una demostración puede contener cientos de pasos y depender de relaciones tan complejas que una equivocación resulte difícil de detectar durante una lectura convencional. Lean examina esas conexiones y verifica que la conclusión se derive de los supuestos establecidos.
El repositorio público del proyecto, publicado en Github, contiene la investigación y su formalización en Lean 4. Según la documentación técnica, los cuatro teoremas principales pasaron las comprobaciones del sistema sin recurrir a pruebas incompletas ni añadir nuevos axiomas. La empresa también documentó verificaciones mediante dos implementaciones independientes del núcleo de Lean.
No obstante, existe una distinción que es tan importante como el resultado: comprobar formalmente una demostración no equivale a certificar cada afirmación de un artículo científico. El propio repositorio reconoce que el manuscrito no pasó íntegramente por Lean. Algunas secciones, entre ellas las dedicadas a los antecedentes, las consecuencias y las preguntas abiertas, carecen de una correspondencia formal en el programa.
Además, un especialista debe comprobar que la afirmación matemática introducida en el sistema representa fielmente el problema original. El programa puede verificar con enorme precisión una demostración construida sobre una definición, pero no decide por sí solo si esa definición expresa correctamente la pregunta que los investigadores querían resolver. Por eso, la revisión humana conserva un papel decisivo.
La noticia también ha despertado interés por la participación de otros investigadores en la evaluación del resultado. PSI afirma que Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan, de la Universidad de Stanford, han examinado la demostración y enviado comentarios. Este grupo había conseguido en agosto último resolver un caso particular de la conjetura: aquel relacionado con algoritmos cuánticos que consultan los datos en un número fijo de rondas paralelas.
Los cuatro investigadores, según la información divulgada por PSI, calificaron el resultado como un avance de gran importancia y preparan una exposición más breve de la demostración para especialistas. Su valoración constituye una señal de interés científico, aunque todavía no sustituye una revisión independiente completa.
El manuscrito de David Turturean permanece como una prepublicación y no cuenta con la certificación de una revista científica mediante revisión por pares. Tampoco debe confundirse la comprobación formal con ese proceso editorial. La primera examina la validez lógica de los pasos codificados; la segunda permite que otros especialistas estudien los argumentos, cuestionen las decisiones matemáticas y valoren la relevancia del trabajo.
La diferencia cobra mayor importancia cuando el propio sistema que produjo la demostración utiliza un modelo cuyo funcionamiento interno no resulta público. Aunque cualquier investigador puede descargar los archivos de Lean y examinar la prueba formal, no dispone de todos los elementos necesarios para reproducir el proceso que condujo al descubrimiento.
La cuestión afecta a uno de los principios fundamentales de la ciencia: la posibilidad de que otros investigadores examinen y reproduzcan los resultados. En este caso, el producto matemático dispone de una vía de comprobación pública, mientras que el proceso de investigación conserva zonas de opacidad.
La experiencia también obliga a revisar el concepto de autoría científica. ¿A quién corresponde el mérito cuando una inteligencia artificial produce los argumentos centrales, una persona diseña el sistema y supervisa el trabajo, y otro programa verifica la demostración?
Por ahora, el caso muestra que la participación de la inteligencia artificial puede resultar central sin que desaparezca la responsabilidad humana. Turturean figura como autor del manuscrito y responde por su contenido. La máquina aporta la capacidad de explorar y construir argumentos, pero los investigadores deben establecer las condiciones de trabajo, evaluar los resultados y asumir las consecuencias de lo publicado.
La experiencia de PSI se suma a una transformación que alcanza distintas áreas de la investigación. Los modelos de inteligencia artificial ya ayudan a examinar grandes cantidades de información, formular hipótesis, identificar relaciones y explorar soluciones que podrían escapar a una búsqueda convencional.
En matemática, sin embargo, la exigencia de precisión plantea un desafío particular. Una respuesta convincente no basta. Cada afirmación necesita una demostración que resista el examen de otros especialistas. De ahí el interés de herramientas como Lean, capaces de convertir los razonamientos en instrucciones verificables por una computadora.
El resultado también tiene un antecedente intelectual importante. La demostración aprovecha ideas desarrolladas por Shachar Lovett y Jiapeng Zhang, así como herramientas matemáticas relacionadas con el trabajo de David Reimer. El avance no surgió de la nada: reunió conocimientos acumulados durante años y encontró una manera de conectarlos para resolver la desigualdad que faltaba.
La propia empresa explica que su sistema encontró una primera demostración y después consiguió mejorar el resultado en dos ocasiones. Esa capacidad para explorar distintas rutas matemáticas, apoyarse en trabajos anteriores y refinar una solución constituye uno de los aspectos más interesantes del experimento.
Queda por comprobar hasta dónde podrá extenderse este método. Resolver una conjetura de gran importancia no significa que las máquinas puedan abordar cualquier problema matemático, ni que los investigadores humanos hayan perdido su lugar. Pero sí muestra que las herramientas de IA comienzan a participar en tareas que hasta hace poco parecían reservadas a especialistas con una formación muy avanzada.
El caso de Aaronson y Ambainis muestra que una máquina puede participar de manera decisiva en esa tarea. El verdadero desafío consiste ahora en establecer cómo comprobar sus resultados, quién responde por ellos y qué garantías necesita la comunidad científica antes de incorporarlos a su conocimiento.
La matemática siempre ha exigido pruebas. En adelante, algunas de ellas podrían llevar también la huella de una inteligencia artificial. Pero, incluso cuando una máquina encuentre el camino hacia una respuesta, la ciencia tendrá que conservar la capacidad de explicar por qué debemos confiar en ella.
