Un equipo de investigadores ha demostrado la síntesis automática de programas cuánticos mediante agentes de grandes modelos de lenguaje, con mejoras de hasta un orden de magnitud en aplicaciones científicas. El trabajo aborda un cuello de botella conocido: los algoritmos cuánticos solo pueden evaluarse clásicamente en instancias pequeñas o restringidas, lo que limita los bucles de descubrimiento automatizado que ya funcionan en matemáticas e informática. La nueva plataforma permite diseñar y validar programas sin ejecutarlos en simuladores clásicos.

El método se apoya en una biblioteca de programas cuánticos construida dentro del demostrador de teoremas Lean. Los agentes sintetizan programas nuevos a partir de especificaciones formales del problema y verifican tanto su corrección como su coste, bajo el rigor de la prueba matemática. Los agentes trabajan en equipos, comparten resultados y conocimiento a través de wikis y discuten ideas en conferencias organizadas, imitando la dinámica de una comunidad de investigación humana.

Los resultados mejoran las referencias previas en búsqueda paralela (hasta 1,4x), aritmética cuántica (290x) y simulaciones relevantes para fusión, fotoquímica y metabolismo de fármacos, con factores de 11x, 8x y 2,5x respectivamente. Combinar inteligencia humana y artificial a gran escala, con garantías de corrección formal, permite diseñar algoritmos que ni los ordenadores clásicos ni los cuánticos actuales pueden probar, acortando el camino hacia la computación cuántica práctica.