Il y a une différence entre une IA qui résout plus rapidement des problèmes connus et une IA qui découvre quelque chose de véritablement nouveau. La première est impressionnante. La seconde change tout.
Axiom vient de franchir ce cap lorsque son AxiomProver a résolu la conjecture ouverte de Fel, un véritable problème mathématique non résolu mathématique qui attendait depuis longtemps dans la littérature scientifique que quelqu’un — ou quelque chose — le résolve.
Voici comment AxiomProver l’a réellement résolue
AxiomProver a reçu trois éléments : un document expliquant le problème en langage courant, une instruction en une ligne (« Énonce et démontre la conjecture de Fel en Lean »), ainsi que le système de vérification de preuves à utiliser.
D’abord, il a lu et compris le problème en déterminant quels objets mathématiques étaient en jeu et ce qu’il fallait démontrer.
Ensuite, il a tout traduit en Lean, un langage de preuve qui joue le rôle d’un arbitre strict pour les mathématiques. Chaque étape logique doit être justifiée par des principes fondamentaux, et l’ordinateur vérifie que chacune est correcte. C’est comme disposer d’un vérificateur des faits capable de repérer la moindre erreur dans votre raisonnement.
Est ensuite venue la partie créative : AxiomProver a choisi une stratégie de démonstration fondée sur les fonctions génératrices exponentielles, une technique qui transforme des motifs complexes de mathématiques discrètes en fonctions continues plus faciles à manier, les manipule algébriquement, puis revient en arrière pour démontrer que la formule d’origine est bien valable.
Imaginez cette technique comme la transformation de briques LEGO en pâte à modeler : on remodèle plus facilement l’ensemble, puis on revient aux briques pour démontrer qu’elles s’assemblent parfaitement. Enfin, AxiomProver a exécuté la démonstration étape par étape dans Lean, chaque mouvement logique étant vérifié par ordinateur. Résultat : une démonstration complète et formellement vérifiée.
Pourquoi c’est important au-delà des mathématiques
Quand l’IA peut découvrir de nouvelles vérités mathématiques de manière autonome, elle pourrait potentiellement débloquer des avancées en science des matériaux, dans la découverte de médicaments, en informatique quantique et dans tous les domaines où des problèmes mathématiques non résolus constituent des goulots d’étranglement. En somme, les mathématiques sont à la base de tout, de la cryptographie qui sécurise votre compte bancaire à la physique qui maintient les avions dans les airs.
Les mêmes techniques qu’utilise AxiomProver pourraient bientôt vérifier que les logiciels sont fiables et à l’abri du piratage. Imaginez une IA capable de garantir mathématiquement que votre dispositif médical ne tombera pas en panne ou que le code de votre voiture autonome ne connaîtra aucune défaillance.
Note de la rédaction : ce contenu a d’abord été publié dans la newsletter de notre publication sœur, The Neuron. Pour découvrir d’autres articles de The Neuron, inscrivez-vous à sa newsletter ici.