Des chercheurs présentent EasyProver, un système qui s’appuie sur des agents d’IA pour prouver ou réfuter des énoncés en Lean, un langage conçu pour écrire des preuves vérifiables par machine. Ils présentent également Aegis, un banc d’essai qui transforme des problèmes de programmation compétitive en tâches de vérification associées à des implémentations en Rust.
Lors de l’évaluation des chercheurs, EasyProver a prouvé 1 054 des 2 000 énoncés Aegis échantillonnés, avec une limite de 30 minutes par énoncé. L’article fait aussi état de résultats élevés sur des bancs d’essai établis pour la démonstration de théorèmes, dont les scores, selon les chercheurs, sont proches de la saturation.
Pourquoi c'est important
Pour les équipes de développement qui envisagent des vérifications formelles sur du code Rust, Aegis propose des tâches qui prennent en compte des détails comme les conversions d’entiers et le comportement en cas d’échec. On ignore toutefois si EasyProver peut vérifier efficacement leur propre code.
