LongTails : un agent d'IA prouve plus de 30 théorèmes inédits

L'intérêt de la vérification formelle

Le principal atout de LongTails est la vérification automatique de chaque preuve dans le langage formel Lean 4. Elle répond à un défaut bien connu de l'IA en mathématiques : un modèle peut produire un raisonnement convaincant en apparence, mais erroné, ou qui traite un autre problème que celui demandé.

Le système part d'une description formelle des conditions et de l'objectif, puis vérifie que la preuve y correspond. Chaque résultat subit donc un contrôle formel, au lieu de reposer sur un raisonnement simplement plausible.

Des applications au-delà des mathématiques

L'optimisation mathématique consiste à trouver la meilleure option parmi de nombreuses possibilités : la plus rapide, la moins coûteuse, la plus précise ou la plus fiable. Les théorèmes établis indiquent la vitesse d'une méthode et les conditions dans lesquelles elle fonctionne, ce qui permet d'estimer à l'avance le nombre de calculs nécessaires plutôt que de tester des algorithmes au hasard.

L'entraînement des réseaux de neurones, des systèmes de recommandation aux grands modèles de langage, repose sur ces méthodes. Des algorithmes plus efficaces pourraient réduire le temps d'entraînement, les coûts de calcul et la consommation d'énergie des centres de données. Les mêmes outils servent aussi à concevoir des structures légères et solides, planifier des tournées de livraison, répartir la charge des réseaux électriques, chercher de nouvelles molécules et de nouveaux matériaux, ou gérer les risques d'investissement.

Le code de LongTails est désormais ouvert, ce qui permet à d'autres équipes de l'utiliser. Un participant au projet affirme que l'outil a obtenu en quelques jours plus de résultats que lui durant toute sa carrière, et juge cette évolution passionnante. L'équipe veut continuer à prouver de nouveaux théorèmes, accroître la complexité des problèmes et tester les algorithmes obtenus dans des applications concrètes.