Le co-fondateur d'Ethereum, Vitalik Buterin, a proposé un nouveau langage de programmation. Il serait compilé directement dans Lean ou HOL, un autre assistant de preuve formel.
L’idée cible une lacune spécifique dans la façon dont les gens lisent les résultats de l’IA. L’intelligence artificielle produit de plus en plus de gros blocs de preuves automatisées, souvent plus rapidement qu’une équipe humaine ne pourrait les écrire à la main. Peu de lecteurs peuvent confirmer rapidement ce que ces preuves établissent réellement.
Un langage conçu uniquement pour les lecteurs d'épreuves IA
Lean est un assistant de preuve, un logiciel que les mathématiciens et les ingénieurs utilisent pour rédiger des preuves qu'un ordinateur peut vérifier ligne par ligne. Les chercheurs d’Ethereum l’utilisent déjà pour vérifier le code cryptographique et la logique de consensus. Les assistants de preuve existent depuis près de 60 ans, mais ce domaine est resté une niche.
Dans son message, Buterin a fait valoir que les étapes internes d'une preuve ne comportent qu'une seule exigence. Cette exigence est l’exactitude mathématique, rien de plus. Les lecteurs n’inspectent jamais directement ces machines. Les définitions et les théorèmes fonctionnent différemment, puisque les humains lisent ces parties pour savoir ce qu'un logiciel garantit réellement.
Buterin a exploré une scission connexe dans un article de blog publié en mai. Là, une preuve mathématique montre qu'un code de bas niveau efficace correspond à une spécification distincte et lisible, de sorte qu'un seul audit couvre les deux versions à la fois.
Son timing correspond également aux propres efforts de reconstruction d’Ethereum, qui portent un surnom distinct, la feuille de route Lean Ethereum. Parallèlement, les chercheurs construisent un ZK-EVM formellement vérifié, une version sans connaissance prouvable de la machine virtuelle (EVM) d'Ethereum, en utilisant des méthodes comparables.
L'IA écrit les preuves, les humains vérifient les affirmations
Les grands modèles de langage peuvent déjà écrire des preuves Lean utilisables. Buterin a nommé Claude et Deepseek 4 Pro comme outils performants, aux côtés de Leanstral, un modèle plus petit spécialement conçu pour Lean. Un exemple de projet est evm-asm, une implémentation EVM vérifiée par rapport à une référence lisible. Cette capacité fait écho aux compétences de raisonnement affichées par les développeurs lors d’un récent défi Buterin AI. Les testeurs ont résolu ce défi en quelques heures.
Les enjeux vont cependant au-delà de la commodité. Les chercheurs en sécurité ont constaté cette année une augmentation des tentatives d’exploitation assistées par l’IA. Le code formellement vérifié offre une défense contre cette tendance. Un langage de spécification plus convivial permettrait aux développeurs de vérifier les affirmations sans parcourir les preuves environnantes.
Au-delà des cercles de recherche d'Ethereum
Buterin continue de tester ces idées en public alors qu'il a récemment fait une démonstration d'un panneau d'affichage anonyme construit avec des preuves de connaissance nulle. La démo a montré comment des allégations vérifiables peuvent passer des référentiels de recherche à des produits fonctionnels. Les chercheurs ont également commencé à vérifier formellement les clients consensuels dans Lean afin de détecter les bogues le plus tôt possible.
Pourtant, la direction fait écho à un modèle familier : séparer le code rapide des affirmations lisibles, puis prouver que les deux correspondent.
Aucun prototype du nouveau langage n’existe encore et Buterin a laissé ouverte la syntaxe exacte. Les développeurs peuvent converger vers une norme partagée ou se contenter de plusieurs dialectes incompatibles. Ce choix pourrait déterminer la rapidité avec laquelle le code vérifié par l’IA atteint les systèmes de production.
Le message Vitalik Buterin propose un langage pour rendre les preuves d'IA lisibles apparaît en premier sur BeInCrypto.
Voir l’article original en anglais
