L'équipe du réseau Ethereum a publié une série de billets invités par le développeur principal de Vyper utilisant le pseudonyme big_tech_sux, consacrée au rôle de la vérification formelle à l'ère du développement rapide de l'intelligence artificielle.
L'auteur affirme que les progrès des LLM rendent la preuve mathématique de l'exactitude des programmes plus accessible, et que pour les contrats intelligents, qui gèrent des milliards de dollars, la vérification formelle devient progressivement une nécessité.
L'IA modifie l'approche de la vérification des logiciels
La série de billets explique que la vérification formelle est une méthode mathématique qui permet de prouver le bon fonctionnement d'un programme pour tous les scénarios d'exécution possibles, et pas seulement pour ceux couverts par les tests.
À titre d'exemple, l'auteur a cité la fonction f(x) = x/2, pour laquelle on peut prouver mathématiquement que le résultat ne dépassera jamais la valeur d'entrée.
Selon lui, cette méthode est capable de trouver des erreurs extrêmement rares, pratiquement impossibles à détecter par des tests ordinaires.
« La vérification formelle peut révéler un cas sur un quadrillion qui ne se manifestera jamais pendant les tests, mais qui pourrait conduire à une défaillance catastrophique », a souligné l'auteur.
En même temps, il a reconnu que jusqu'à récemment, l'utilisation de cette approche nécessitait le travail de grandes équipes d'experts, qui créaient des modèles mathématiques des programmes et menaient des preuves complexes.
Selon le développeur, les LLM modernes simplifient considérablement ce processus à mesure que l'on s'approche de l'IAG.
Néanmoins, l'auteur a souligné que même avec l'aide de l'IA, la vérification formelle reste un processus complexe et gourmand en ressources. En particulier, la transformation du code en un modèle formel peut contenir des inexactitudes qui affectent la fiabilité des résultats.
Le développement de l'IA modifie l'équilibre entre attaque et défense
Le document note que le développement de l'intelligence artificielle augmente simultanément l'efficacité tant des défenseurs que des attaquants malveillants.
L'auteur a rappelé un cas où un modèle OpenAI, pas encore publié, a pu trouver des vulnérabilités zero-day permettant de contourner plusieurs couches de protection.
Dans ce contexte, la vérification formelle, selon l'auteur, permet de faire pencher l'avantage en faveur des défenseurs.
« Alors que les attaquants n'ont besoin de trouver qu'une seule séquence de données d'entrée pour pirater un système, les défenseurs peuvent utiliser la vérification formelle pour prouver sa résistance à toutes les données d'entrée possibles », a-t-il souligné.
C'est pourquoi pour les logiciels critiques, en particulier les contrats intelligents qui gèrent des milliards de dollars de fonds utilisateurs, la vérification formelle devient « non pas une option, mais un prérequis nécessaire ».
Il convient de noter que cela poursuit le débat qu'avait initié précédemment le cofondateur d'Ethereum, Vitalik Buterin, concernant l'utilisation de l'IA pour la vérification formelle du code.
end-content
