Le processus de traduction automatique de concepts mathématiques écrits en langage naturel en spécifications et preuves formelles est appelé « auto-formalisation ». Dans le but d’améliorer les modèles d’autoformalisation et les machines de vérification actuels, des chercheurs ont développé une nouvelle méthode, basée sur une IA capable de prendre en charge un tel processus. Plus efficace et plus rapide que les humains dans cette tâche, elle pourrait aussi mener à la découverte de nouvelles théories mathématiques.
Les preuves (ou démonstrations) mathématiques sont aujourd’hui vérifiées par des ordinateurs. Ceci requiert toutefois de « traduire » au préalable la démonstration — qui combine formules, symboles mathématiques et langage naturel — en un langage spécifique, compréhensible par la machine. Cette tâche est cependant très chronophage : il a fallu près de dix ans pour formaliser (et vérifier) de cette manière la conjecture de Kepler, qui décrit la meilleure façon d’empiler une collection d’objets sphériques.
Non seulement un système automatisé réduirait le coût des efforts actuels de formalisation, mais il pourrait connecter les différents domaines de recherche qui automatisent certains aspects du raisonnement mathématique au vaste corpus de connaissances exclusivement écrites en langage naturel. « Un système d’autoformalisation réussi pourrait faire progresser les domaines de la vérification formelle, de la synthèse de programmes et de l’intelligence artificielle », écrivent les chercheurs dans l’article décrivant leur approche.
Une autoformalisation par de Grands modèles de langage
Seule une toute petite fraction des connaissances mathématiques ont été formalisées, puis prouvées à ce jour. Quelques projets existent en matière de compréhension de langages formels, mais sont limités aux langages pour lesquels il existe un grand nombre de corpus sur le web (par exemple, le langage Python).
Les données sur les mathématiques formelles sont très rares : l’Archive of Formal Proofs, ne fait que 180 Mo — soit moins de 0,18% des données d’entraînement de l’OpenAI Codex, une intelligence artificielle développée par OpenAI, qui analyse le langage naturel et génère du code en réponse. Cette IA a été formée à partir de larges quantités de textes et de données de programmation disponibles sur le Web. Elle est notamment utilisée pour alimenter GitHub Copilot, un outil d’auto-complétion de programmation ; elle peut satisfaire environ 37% des demandes, et permet ainsi d’accélérer la programmation.
Pour développer une IA capable de formaliser les problèmes mathématiques, Yuhuai Wu, chercheur chez Google, et ses collègues ont eu l’idée d’exploiter ce Codex — partant du principe que les langages de programmation et les démonstrations mathématiques partagent quelques similitudes.
Ils ont ainsi fourni à Codex un ensemble de 150 problèmes tirés de concours de mathématiques de l’enseignement secondaire. Il se trouve que l’IA a été capable de traduire parfaitement une portion significative (25,3%) des problèmes donnés dans un langage compatible avec Isabelle — un programme open source (à code ouvert) de résolution de démonstrations mathématiques. Selon l’équipe, la plupart des traductions manquées étaient dues au fait que le système ne comprenait pas certains des concepts mathématiques utilisés (à cause d’une mauvaise correspondance entre les définitions formelles et informelles).
Une formalisation automatisée bien meilleure que la formalisation humaine
Pour tester l’efficacité de ce processus, les chercheurs ont ensuite soumis à Codex un ensemble de problèmes qui avaient déjà été formalisés par des humains, obtenant ainsi un second ensemble de problèmes formalisés. Ils ont ensuite fait appel à une autre IA, appelée MiniF2F, pour vérifier les deux versions. Résultat : Codex est apparu bien meilleur que les humains dans la formalisation des problèmes. « Notre méthodologie aboutit à un nouveau résultat de pointe sur le benchmark de démonstration de théorèmes MiniF2F, améliorant le taux de preuve de 29,6% à 35,2% », précisent les chercheurs.
L’équipe a également exploré la traduction inverse, l’informalisation, à savoir la traduction du code Isabelle en langage naturel. Sur les 38 exemples testés, 36 ont été traduits en un énoncé « raisonnablement cohérent », parmi lesquels 29 (soit 76%) étaient plus ou moins corrects. Conclusion : le taux de réussite de l’informalisation est nettement supérieur à celui de la formalisation.
Le taux de réussite de l’autoformalisation peut paraître modeste, mais étant donné la faible quantité de code Isabelle inclus dans l’entraînement de Codex, le fait que le modèle puisse écrire du code syntaxiquement correct est déjà fascinant, soulignent les chercheurs. Il n’existe en outre pratiquement aucune donnée alignée entre le langage naturel et le code Isabelle.
L’équipe pense que le taux de réussite pourrait rapidement être amélioré, jusqu’à rivaliser avec les plus grands mathématiciens. Cette autoformalisation permet non seulement d’améliorer les modèles existants, mais pourrait aussi être appliquée à de nombreuses tâches de vérification (tant dans la conception de logiciel que dans la conception matérielle).
Un défi majeur reste cependant d’appliquer ce modèle à la recherche mathématique, dont la plupart des travaux sont rédigés en LaTeX, un langage et un système de composition de documents qui utilise sa propre syntaxe et ses propres commandes. Il pourrait être beaucoup plus délicat pour le réseau neuronal d’interpréter et de traduire ce type de contenu.