Physical Superintelligence (PSI) afirma que un sistema de investigación con un modelo no público de Anthropic produjo una demostración de la conjetura Aaronson-Ambainis, un problema que relaciona las matemáticas con los límites de la computación cuántica. La empresa dice que el asistente de pruebas Lean aceptó el argumento formal; la correspondencia con la conjetura original y el alcance del resultado siguen sujetos a revisión.
El laboratorio anunció el trabajo el 6 de noviembre y sostiene que obtuvo una prueba completa durante el tercer día de ejecución del sistema. Después lo puso a trabajar en problemas relacionados y, según su relato, la herramienta mejoró dos veces el resultado; Lean también aceptó la versión final. PSI no identificó el modelo de Anthropic utilizado.
La conjetura, atribuida a los científicos de la computación Scott Aaronson y Andris Ambainis, estaba abierta desde 2008, según PSI. El manuscrito de David Turturean y los archivos de la formalización están disponibles en un repositorio público para que otros investigadores los examinen.
Qué comprueba Lean y qué queda fuera
Lean es un asistente que verifica si una demostración expresada en su lenguaje sigue las reglas lógicas y los supuestos definidos. El repositorio de PSI afirma que sus teoremas finales se comprobaron sin pasos pendientes ni axiomas añadidos. La empresa también registró comprobaciones con otra implementación del verificador.
Eso permite inspeccionar y repetir las pruebas informáticas, pero el propio repositorio advierte que una persona debe confirmar si el enunciado escrito en Lean expresa la conjetura original. El artículo redactado para lectores humanos tampoco se comprueba automáticamente como documento completo. Entre las secciones sin equivalente formal están las consecuencias cuánticas que describe el manuscrito.
Hay otra distinción dentro de los resultados publicados. Las tres formulaciones principales no dependen del teorema externo que aparece en la cuarta. Esta ofrece una constante mejor, pero asume ese resultado de otros autores, que PSI no formalizó en el repositorio.
State of Proof, un observatorio de investigación asistida por IA, informó el 6 de noviembre que comparó las huellas digitales de 87 archivos públicos con las de la lista incluida en los registros de PSI. La coincidencia ayuda a identificar los archivos, pero el observatorio aclara que no repitió las comprobaciones ni certificó la corrección matemática. Tampoco había establecido que el manuscrito hubiera completado una revisión por pares.
Qué implicaría para la ventaja cuántica
La pregunta de Aaronson y Ambainis se plantea mediante polinomios, expresiones matemáticas que combinan variables. En términos generales, la conjetura sostiene que, si un polinomio de cierto tipo varía lo suficiente, al menos una de sus variables debe tener una influencia mínima. PSI presenta una cota para esa influencia basada en la variación y el grado del polinomio.
La conexión con la computación cuántica procede del trabajo de los propios Aaronson y Ambainis. Sus autores mostraron que, si se cumple la conjetura, un algoritmo clásico podría estimar la probabilidad de que ciertos algoritmos cuánticos respondan que sí en la mayoría de las entradas. Para un margen de error y una proporción de excepciones fijos, el número de consultas clásicas crecería como una potencia del número de consultas cuánticas. Una consulta es una lectura de la entrada dentro de ese modelo teórico.
La conclusión trata sobre consultas, no sobre cuántos segundos tardaría una computadora comercial. La discusión de los autores sobre tiempo de ejecución requiere supuestos adicionales. Tampoco elimina las ventajas para problemas con estructura especial, como los asociados al algoritmo de factorización de Peter Shor, ni mide el rendimiento de una máquina cuántica física.
Quién revisó el trabajo
Turturean, integrante del equipo técnico de PSI, desarrolló el sistema, delimitó el problema y revisó el manuscrito, cuya corrección asume como responsable, de acuerdo con la empresa. El repositorio indica que modelos de IA produjeron los enunciados matemáticos, el primer borrador del artículo y la formalización en Lean.
PSI señala que su asesor Jim Halverson auditó la prueba y que otra asesora, Phiala Shanahan, comentó la formalización. También dice que Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan, de la Universidad de Stanford, leen el trabajo y preparan una exposición más breve para especialistas. La empresa reproduce una valoración conjunta en la que el grupo lo llama "un resultado enorme".
Los cuatro investigadores ya habían demostrado la predicción de la conjetura para un caso más acotado, en un trabajo difundido en agosto: algoritmos cuánticos que consultan sus entradas en un número fijo de rondas paralelas. El trabajo de PSI pretende cubrir la conjetura general. Con el manuscrito y el código abiertos, otros especialistas pueden contrastar esa pretensión con el enunciado original y revisar por separado el vínculo con las consultas cuánticas.
