PSI afirma que un sistema de IA con un modelo inédito de Anthropic demostró la conjetura de Aaronson-Ambainis

Physical Superintelligence (PSI), una empresa emergente que aplica la IA a la investigación en física, anunció el 6 de noviembre que su sistema interno de investigación había producido una demostración completa de la conjetura de Aaronson-Ambainis. Según Unite.AI y Silicon Report, PSI sostiene que el sistema ejecutaba instancias de un modelo no público de Anthropic y que llegó a la demostración al tercer día de funcionamiento; después se le pidió seguir trabajando y logró dos mejoras más. El repositorio público atribuye a "modelos de IA" los enunciados, el primer borrador y el código Lean, pero no nombra al proveedor, de modo que el vínculo con Anthropic depende del anuncio de PSI.

Qué dice la conjetura

Los ordenadores cuánticos consiguen aceleraciones enormes en algunos problemas con estructura oculta, como la factorización. La conjetura, formulada en 2008 por Scott Aaronson y Andris Ambainis, se ocupa del caso contrario. En términos matemáticos, sostiene que todo polinomio acotado y de grado bajo sobre entradas booleanas tiene al menos una variable con una influencia apreciable en su resultado. Ambos investigadores demostraron que de ello se seguiría que cualquier algoritmo cuántico que haga cierto número de consultas puede imitarse, en la mayoría de las entradas, con un algoritmo clásico que solo necesite polinómicamente más. Dicho de forma sencilla: no habría ventaja cuántica exponencial con datos aleatorios y sin estructura. Es un problema difícil: un preprint de 2019 que decía demostrarla fue retirado tras detectarse un fallo, como contó Aaronson en su blog.

Qué está comprobado y qué no

El repositorio, que fija la versión 4.33.0 de Lean y de Mathlib, afirma que la biblioteca no usa marcadores "sorry" ni axiomas adicionales y que la reproducción en el núcleo superó comprobadores independientes. El README también marca los límites: corresponde al lector confirmar que el enunciado formal, llamado PrintedConjecture, recoge fielmente la conjetura, y el artículo pensado para humanos no está verificado por la máquina. Una variante que ofrece una constante más ajustada depende de un resultado externo no formalizado; según el README, los teoremas principales no dependen de él.

David Turturean, de PSI, desarrolló el sistema y figura como responsable de la corrección del artículo. Los materiales de PSI citan a Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan, que en agosto probaron un caso particular relacionado y califican el trabajo de "un resultado enorme"; preparan una versión más breve. Al cierre de esta nota no constaba revisión en ninguna revista ni reacción pública de Aaronson o Ambainis. El argumento parte de una estrategia de Shachar Lovett y Jiapeng Zhang y sustituye una desigualdad que su plan dejaba sin demostrar.