OpenAI : son modèle Astra a résolu 10 problèmes mathématiques complexes pour 2 000 dollars

OpenAI a révélé samedi que son modèle interne Astra a produit de nouveaux résultats pour 10 problèmes de mathématiques et d'informatique théorique restés ouverts depuis au moins dix ans, publiant des preuves vérifiables par machine pour chaque affirmation. L'entreprise a rapporté un coût en jetons d'environ 2 000 dollars aux tarifs API actuels pour l'ensemble des 10 solutions.forbes+1

Des preuves vérifiées dans plusieurs domaines

Les résultats couvrent l'empilement de sphères en haute dimension, la théorie du codage, la cryptographie, la combinatoire extrémale et la théorie des jeux quantiques. Le résultat phare est une construction explicite d'un groupe non sofique, une question ouverte depuis 1999, qui réfute la conjecture selon laquelle tous les groupes dénombrables sont sofiques. Astra a également réfuté la conjecture de rigidité de Connes de 1980 et résolu trois problèmes du catalogue de Paul Erdős, dont le problème 183 sur les nombres de Ramsey multicolores.newscientist+1

OpenAI a publié un manuscrit de 249 pages accompagné de certificats de preuve Lean 4 sur GitHub sous licence Apache 2.0, signalant un nombre de "sorry" égal à zéro, ce qui signifie qu'aucune étape d'aucune preuve formalisée n'est restée sans démonstration. Le noyau Lean renvoie un verdict binaire : la preuve compile ou non, éliminant le besoin de faire confiance aveuglément à la sortie du modèle.siliconangle+1

Thomas Bloom, qui gère le catalogue des problèmes d'Erdős, a qualifié ces résultats de "grande nouvelle" et les a classés au-dessus du contre-exemple de distance unitaire d'Erdős produit par un modèle précédent d'OpenAI en mai. Abhishek Saha, de l'Université Queen Mary de Londres, a déclaré que chacune des 10 solutions "serait une réalisation significative et impressionnante".newscientist+1

Les sceptiques appellent à la prudence

L'annonce a suscité des critiques acerbes. Gary Marcus, un sceptique notoire de l'IA, a décrit la publication comme "incroyable, mais largement survendue", arguant que le succès dans les mathématiques formellement vérifiables ne se généralise pas aux domaines où la vérification est plus complexe. Il a noté que le chiffre de 2 000 dollars ne couvre que les tentatives réussies et exclut les salaires des mathématiciens et informaticiens ayant aidé à préparer les documents.garymarcus.substack

Francesco Fournier-Facio, de l'Université de Cambridge, a remis en question la transparence des travaux, arguant que la solution sur la soficité repose largement sur des articles antérieurs d'Andreas Thom et Gábor Kun datant de 2016 et 2019. L'affirmation initiale d'OpenAI selon laquelle les 10 problèmes "n'avaient connu aucun progrès sur le résultat principal depuis au moins une décennie" a été amendée après que Fournier-Facio s'est plaint de son inexactitude.newscientist

Implications plus larges

Astra reste non publié. OpenAI le décrit comme une famille de modèles conçue pour coordonner plusieurs agents sur des tâches étendues. Le PDG Sam Altman a présenté le modèle à des décideurs politiques à Washington, mais l'entreprise n'a pas annoncé de date de sortie ni précisé s'il sera commercialisé sous le nom de GPT-6 ou une autre variante.siliconangle

Ce calendrier intervient alors que la communauté mathématique s'oppose aux entreprises d'IA. En juin, l'Union mathématique internationale a approuvé la Déclaration de Leiden, avertissant que les entreprises d'IA "utilisent des recherches publiées sans consentement, contournent l'examen par les pairs et menacent l'intégrité de la preuve et de l'attribution".siliconangle