PSI affirme qu’une IA d’Anthropic a prouvé la conjecture d’Aaronson-Ambainis

Physical Superintelligence (PSI), une startup spécialisée dans l'IA appliquée à la physique, a annoncé le vendredi 6 novembre qu'un système de recherche qu'elle a conçu a prouvé la conjecture d'Aaronson-Ambainis, un problème de complexité quantique non résolu depuis 2008, en utilisant des instances d'un modèle Anthropic non public. L'entreprise a indiqué que le système avait obtenu une preuve complète au troisième jour d'exécution sur sa propre infrastructure, et que l'assistant de preuve Lean l'avait acceptée. Le résultat n'a pas encore fait l'objet d'une évaluation par les pairs dans une revue scientifique. Pour l'instant, il s'agit d'une revendication de l'entreprise, mais l'article et la preuve vérifiée par machine sont publics, permettant ainsi à des experts externes de les tester.psi.inc

Ce que la preuve démontre

La conjecture pose la question de savoir si les ordinateurs quantiques peuvent être exponentiellement plus rapides que les ordinateurs ordinaires sur des entrées aléatoires, qui ne contiennent presque jamais les motifs cachés exploités par des algorithmes comme la méthode de factorisation de Shor. Aaronson et Ambainis ont montré que si leur énoncé sur les polynômes bornés de bas degré était vrai, les accélérations quantiques sur des entrées aléatoires seraient au plus polynomiales. L'annonce de PSI a résumé le résultat ainsi : "un ordinateur quantique ne peut pas économiser exponentiellement beaucoup de recherches à moins que la chaîne ne présente un motif rare". Le théorème limite le nombre de fois qu'un algorithme lit son entrée, et non le temps de calcul total, ce qui laisse place à des avantages quantiques pratiques.thequantuminsider.com+1

La première preuve offrait une borne plus faible. Après que PSI a orienté le système vers des problèmes ouverts connexes, il a amélioré le résultat à deux reprises, et Lean a accepté la version finale. L'argument suit un plan établi par Shachar Lovett et Jiapeng Zhang. Il remplace une inégalité qu'ils avaient laissée à l'état de conjecture par une nouvelle, prouvée en appariant les configurations d'entrée via un déterminant.psi.inc

Rôles humains et vérifications

David Turturean, membre de l'équipe de PSI, a construit et fait fonctionner le système, a guidé le modèle pour rédiger l'article et est responsable de son exactitude. Les conseillers Jim Halverson et Phiala Shanahan ont audité la preuve et commenté la formalisation. Le dépôt GitHub du projet indique que la preuve, l'article et la formalisation ont été produits par des modèles d'IA. Il précise également que les théorèmes Lean ne contiennent aucun espace réservé ni axiome ajouté, et ont été revérifiés par deux implémentations de noyau indépendantes. Les lecteurs doivent toujours confirmer que l'énoncé formel correspond à la conjecture originale.github.com+1

Les chercheurs de Stanford Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan ont résolu un cas particulier en août. Ils ont lu la preuve complète et, dans une déclaration publiée par PSI, l'ont qualifiée de "résultat énorme" où "tout est réuni de manière assez magique".psi.inc

Questions en suspens

PSI n'a pas précisé quel modèle Anthropic a été utilisé, et Anthropic n'a pas répondu à une demande de commentaire. Cette annonce fait suite à la déclaration d'OpenAI en septembre affirmant avoir résolu un problème impliquant les équations de Navier-Stokes, et elle alimente le débat sur l'impact de l'IA pour les carrières des mathématiciens.businessinsider.com