La startup spécialisée dans l'intelligence artificielle « Axiom Math » a annoncé le succès de son système d'agents autonomes dans la vérification formelle (Formal Verification) de l'intégralité du contenu du « Stacks Project », considéré comme l'un des plus vastes ouvrages de référence mathématiques ouverts jamais rédigés par des mathématiciens.
Convertir la connaissance mathématique en code vérifiable
Le projet Stacks, initié par le professeur de mathématiques de l'Université Columbia Johan de Jong en 2005, comprend environ 7 654 pages couvrant les principes de l'algèbre et de la géométrie algébrique jusqu'aux théories avancées de la théorie des nombres. Les essaims d'agents d'Axiom Math ont réussi à traduire ces textes complexes et interconnectés en environ 16 millions de lignes de code dans le langage « Lean », un langage de programmation spécialisé qui permet aux logiciels de vérification d'examiner chaque preuve mathématique ligne par ligne afin d'en garantir la rigueur logique absolue.
L'entreprise, dont la valorisation boursière atteint 1,6 milliard de dollars après avoir levé 200 millions de dollars lors d'un premier tour de table mené par « Menlo Ventures », vise à construire une base de connaissances fiable et prouvée par le code, sur laquelle les futurs systèmes d'IA pourront s'appuyer pour le développement de logiciels et la recherche scientifique, évitant ainsi la production de conclusions trompeuses ou inexactes connues sous le nom de « déchets génératifs » (AI slop).
Mécanisme de fonctionnement des agents et défis de la cohérence structurelle
Carina Hong, fondatrice et PDG de l'entreprise âgée de 25 ans, qui a quitté son programme de doctorat en mathématiques à l'Université Stanford pour fonder Axiom en mars 2025, a expliqué que le plus grand défi consistait à maintenir la cohérence de milliers de théorèmes et à éviter toute contradiction conceptuelle. De son côté, Ashvin Swaminathan, membre de l'équipe technique de l'entreprise, a souligné que les agents d'IA n'ont pas travaillé sous une direction directe pour chaque étape, mais qu'une structure hiérarchique flexible leur a été imposée, leur permettant de répartir les tâches en parallèle et de tirer parti de modèles spécialisés entraînés au raisonnement mathématique rigoureux, plutôt que de dépendre de modèles de génération de code généralistes.
Que signifie cette avancée pour le secteur technologique ?
Ce développement représente une étape concrète pour combler une lacune majeure dans la preuve mathématique assistée par ordinateur, en particulier dans des domaines tels que la géométrie algébrique. L'utilité de la vérification formelle ne se limite pas aux milieux académiques ; la documentation des preuves via le code informatique offre un environnement fondamental réutilisable. L'entreprise parie que les développeurs et les concepteurs de logiciels sensibles — tels que la conception de puces et les calculs de systèmes critiques — auront besoin de ces bases vérifiées pour prévenir les failles de sécurité et les erreurs cachées résultant de la dépendance croissante envers les agents pour l'écriture de logiciels.