Pour prouver ces avancées, l’entreprise a publié un manuscrit de 249 pages et des certificats de preuve formels via le langage Lean 4 sur GitHub.
L’annonce marque une rupture avec les capacités de raisonnement des modèles de langage précédents. Contrairement aux réponses probabilistes classiques, Astra a produit des preuves vérifiables par machine, permettant à tout utilisateur disposant d’un ordinateur de valider mathématiquement les résultats sans dépendre de la parole d’OpenAI.
Dix résultats et des certificats Lean 4
Les avancées revendiquées par OpenAI couvrent un spectre large de disciplines complexes. Le résultat le plus notable concerne la première construction explicite de groupes non sofiques, un problème majeur de la théorie des groupes.
Pour accompagner ces affirmations, OpenAI a mis à disposition trois types de documents :
- Un manuscrit collectif de 249 pages détaillant les preuves.
- Des guides de raisonnement (walkthroughs) rédigés par le modèle.
- Des certificats de preuve formels en Lean 4, déposés sur GitHub, qui permettent une vérification informatique rigoureuse.
Cette approche vise à transformer l’IA d’un outil de suggestion en un outil de découverte scientifique.
Un modèle interne en attente de déploiement
L’entreprise a souligné que l’évaluation de ses modèles sur des problèmes de recherche ouverts fait désormais partie intégrante de son processus de développement.
Réactions et enjeux de la Singularité
La capacité d’une IA à résoudre des problèmes mathématiques dont les meilleurs experts humains étaient incapables depuis des décennies a déclenché des réactions fortes.
L’enjeu technique réside dans la transition vers le raisonnement formel. En utilisant Lean 4, Astra ne se contente pas de prédire le mot suivant, mais construit une structure logique dont chaque étape est validée par un noyau de preuve informatique. Cela élimine les hallucinations mathématiques, un défaut majeur des versions précédentes de GPT.
L’industrie attend désormais de savoir si Astra sera intégré à ChatGPT ou s’il restera un outil spécialisé pour la recherche. La question demeure ouverte quant à savoir si le modèle a découvert de nouvelles méthodes de preuve ou s’il a simplement optimisé la recherche de solutions dans des espaces de possibilités massifs.
Sur le même sujet
