NETYS 2025 : IA et raisonnement formel, quand les mathématiques réinventent la science

Lors de la 13ᵉ l’édition de NETIS 2025, un évènement international consacré à l’intelligence artificielle (IA) qui s’est tenu à l’Université Mohammed VI Polytechnique (UM6P), Swarat Chaudhuri, professeur à l’Université de Texas et Google DeepMind, a présenté une vision avant-gardiste de l’IA au service de la découverte scientifique.

La preuve formelle, un problème mathématique pour l’IA ?

Lors d’une présentation, il a été question de transformer les mathématiques en un environnement propice au développement de l’IA. Concrètement, chaque objectif consiste à prouver un théorème en utilisant une suite de tactiques symboliques. Ensuite, chaque étape du raisonnement est interprétée comme un niveau franchi, guidé par des algorithmes de recherche assistés par l’IA.

En effet, cette approche repose notamment sur l’usage de réseaux neuronaux capables d’explorer un espace de preuves en proposant, à chaque étape, la meilleure tactique possible pour progresser vers une démonstration complète. Swarat Chaudhuri évoque le projet DeepMind, dans lequel un réseau est entraîné sur plus de 100 millions de théorèmes mathématiques afin d’apprendre les bonnes stratégies via l’apprentissage par renforcement. À chaque tentative réussie ou échouée, le système affine son comportement.

Cependant, certains manquements sont constatés : les modèles de langage, comme GPT, ne peuvent pas générer des raisonnements mathématiques en langage naturel tout en les traduisant simultanément sous une forme compréhensible. Néanmoins, loin d’être de simples outils de saisie de texte, ces modèles se montrent capables d’analyser des énoncés complexes, de les reformuler, puis de décomposer les problèmes en sous-énoncés, avant de les résoudre de manière hiérarchique, explique le professeur.

Cette méthodologie est particulièrement efficace dans le cas de la vérification des compilateurs. Le processus commence par la définition des langages source et cible, ainsi que de leurs sémantiques. Par la suite, l’IA est capable de prouver que chaque étape de la compilation préserve la signification du programme. À travers une preuve de bas niveau, l’IA élabore des tactiques cohérentes et s’appuie sur des lemmes intermédiaires pour démontrer des propriétés complexes, conclut l’expert.

Lire aussi: L’UM6P lance « HACK The Future of Work » pour anticiper l’impact de l’IA sur l’emploi

De la formalisation au raisonnement empirique

Au-delà des mathématiques, la puissance des LLMs s’étend à la découverte scientifique. Le processus de recherche scientifique, c’est-à-dire de la formulation d’hypothèses à l’interprétation des données, peut aujourd’hui être partiellement automatisé grâce à des méthodes issues de la régression symbolique. Cette technique, bien connue en analyse de données, consiste à dériver des équations explicatives à partir d’observations.

Historiquement, les méthodes de régression symbolique s’appuyaient sur des algorithmes évolutionnaires tels que la programmation génétique. Ceux-ci généraient une population d’expressions mathématiques que l’on faisait évoluer selon des fonctions de fitness. Désormais, les LLMs enrichissent ce processus : ils interviennent pour suggérer des croisements, muter des programmes et extraire des concepts linguistiques abstraits à partir de résultats expérimentaux.

Dans ce sens, Swarat Chaudhuri cite l’exemple de phénomènes tels que la loi de Zipf, la loi de Moore ou encore certaines lois astrophysiques qui, bien que d’origines différentes, partagent des structures similaires, comme les lois de puissance. Ce type de motifs, difficilement reconnaissables par des méthodes purement symboliques, est détecté plus efficacement par les LLMs grâce à leur entraînement sur de vastes corpus.

Une autre avancée majeure présentée est la création de CSLib, une bibliothèque universelle de formalisation des connaissances en informatique. Inspirée du projet Mathlib dédié aux mathématiques, cette initiative vise à formaliser des concepts fondamentaux tels que le calcul, les structures de données, la complexité, et bien plus encore.

La promesse est ambitieuse : créer un socle de connaissances formelles servant à la fois à l’enseignement, à la recherche et à l’automatisation des preuves. Parallèlement, le développement d’un langage intermédiaire (NPM) permettrait d’écrire des algorithmes annotés de spécifications formelles (précision, complexité, vérifiabilité), traduisibles en langages tels que C ou Rust. Une véritable révolution pour la programmation vérifiée.

Lire aussi: UM6P inaugure son implantation à Station F et lance le programme NextAfrica

Vers une IA chercheuse ?

Lors de son intervention, le professeur de l’université du Texas explique que ces outils ne se limitent pas à l’analyse mathématique ou informatique. Ils s’illustrent également dans des domaines appliqués, tels que la découverte de lois physiques ou la conception de circuits électroniques. Un agent combinant LLMs et algorithmes évolutionnaires a ainsi permis de trouver des heuristiques d’ordonnancement plus efficaces pour les centres de données de Google, ainsi que des algorithmes innovants pour la multiplication de matrices.

Ce nouveau paradigme, que l’on pourrait qualifier d’évolution dirigée par les LLM, réunit deux forces : l’intuition générée par les modèles de langage et la rigueur du raisonnement formel. L’agent alterne entre génération d’hypothèses, abstraction de concepts, et vérification empirique ou formelle, dans une boucle d’apprentissage quasi autonome.

Ce que met en lumière la présentation de Swarat Chaudhuri, c’est que le langage utilisé généralement dans le code est devenu une véritable interface entre les mondes abstraits des mathématiques, du code et de la physique. Cette caractéristique, longtemps ignorée, s’impose désormais comme un catalyseur essentiel de l’automatisation scientifique.

Les LLMs permettent non seulement de traduire les pensées humaines en langage machine, mais aussi de raisonner, corriger et apprendre de manière autonome. Grâce à eux, l’intelligence artificielle passe du statut d’outil passif à celui de partenaire actif dans la découverte.

La frontière entre preuve formelle, langage naturel et créativité scientifique s’efface progressivement. Ce qui émerge, c’est une synergie inédite entre l’humain et la machine, où la formalisation rigoureuse nourrit l’IA, et où l’intuition linguistique des modèles accélère la recherche. À l’aube de cette nouvelle ère, un futur dans lequel l’intelligence artificielle assiste et complète les grandes avancées scientifiques n’est plus une utopie, mais une réalité en gestation.