À l’heure où les technologies d’intelligence artificielle accélèrent les cybermenaces, des entreprises de la Silicon Valley tentent d’éradiquer les failles logicielles en adaptant des méthodes mathématiques avancées. OpenAI, Anthropic et de nouvelles start-up misent sur le langage de programmation Lean pour prouver formellement l’intégrité du code informatique.
En septembre, OpenAI a annoncé qu’une nouvelle technologie d’intelligence artificielle avait résolu en moins d’une semaine le problème de Navier-Stokes, une énigme mathématique qui résistait aux meilleurs esprits depuis des décennies, d’après les informations du New York Times. Cette percée, suivie de près par d’autres publications de la part de l’entreprise, a surpris de grands mathématiciens et ouvert de nouvelles perspectives pour une discipline longtemps considérée comme le sommet de l’accomplissement humain.
Mais les applications de ces compétences mathématiques dépassent largement la recherche universitaire.
Dans la Silicon Valley, des chercheurs adaptent ces mêmes techniques pour éliminer les failles dangereuses, ou bugs
, dans les logiciels informatiques. Tout en prouvant la justesse d’un problème mathématique, un système d’intelligence artificielle peut théoriquement démontrer qu’une application est totalement exempte de failles.
Protéger les logiciels avec les mathématiques formelles
Cette approche, baptisée vérification de logiciels, intervient alors que l’Internet fait face à ses menaces de cybersécurité les plus graves depuis des décennies. Les systèmes d’intelligence artificielle actuels sont désormais capables de s’introduire dans les logiciels en repérant et en exploitant leurs faiblesses avec une rapidité déconcertante, rendant urgente l’émergence d’une nouvelle génération d’IA capable de supprimer ces vulnérabilités.
À Palo Alto, en Californie, la jeune entreprise &Truth figure parmi les sociétés qui développent cette technologie. Des laboratoires comme Anthropic et OpenAI, ainsi que d’autres start-up de la Silicon Valley telles qu’Axiom et Logical Intelligence, cherchent également à vérifier le code mondial à l’aide d’un langage de programmation spécialisé nommé Lean.
Il est possible de faire quelque chose qui n’était pas possible avant. Vous avez vu ce qui s’est passé en mathématiques, en prouvant ces conjectures ouvertes massives. Nous pouvons appliquer les mêmes méthodes formelles à la vérification de logiciels.
Inventé il y a plus de dix ans par le chercheur de Microsoft Leonardo de Moura, Lean servait initialement d’outil aux programmeurs humains. Aujourd’hui, les technologies d’intelligence artificielle génèrent leur propre code et utilisent Lean pour établir des démonstrations mathématiques au moyen d’essais et d’erreurs extrêmes, une technique appelée apprentissage par renforcement.
Confronter la rigueur mathématique au monde réel
Malgré ces avancées, l’entraînement d’IA à la vérification de code s’avère beaucoup plus complexe qu’en mathématiques. Les règles mathématiques sont solidement établies depuis des siècles, tandis que les codes informatiques se révèlent bien plus désordonnés. Pour vérifier une application, il faut d’abord poser des spécifications formelles définissant son comportement attendu avant qu’une intelligence artificielle puisse rédiger le code Lean nécessaire.
Les bogues surviennent lorsqu’un programme s’exécute d’une manière imprévue, par exemple en écrivant des données excédentaires dans la mémoire système et en corrompant d’autres registres, ce que des attaquants malveillants exploitent pour pirater l’application. Si des ingénieurs expérimentés peuvent réaliser ce travail de vérification manuellement, la tâche exige des années d’efforts. Des entreprises comme &Truth visent à réduire ce délai à quelques heures ou quelques jours grâce à l’intelligence artificielle.
Cependant, les créateurs d’applications ne peuvent anticiper toutes les situations rencontrées face à des utilisateurs réels. Comment savez-vous que vos hypothèses sont correctes ? À un moment donné, le code entre en contact avec la réalité complexe
, souligne Will Wilson, directeur général d’Antithesis, une entreprise spécialisée dans les tests de code et de failles de sécurité.
Affronter la crise des cybermenaces
Les structures comme &Truth se trouvent encore loin d’assurer que l’ensemble des logiciels du marché sont totalement exempts de bugs. Néanmoins, alors que le piratage assisté par l’intelligence artificielle fragilise la sécurité en ligne, chaque progrès compte.
Il y a une urgence qui était de plus en plus palpable à partir de la fin de l’année dernière. Ce problème de sécurité est un problème déterminant de notre époque.
Selon Chris Hsu, co-fondateur, président et co-directeur général de &Truth, ce problème de sécurité représente désormais un défi déterminant et urgent pour notre époque.