💻 computer science

PROMISE: Proof Automation as Structural Imitation of Human Reasoning

Le papier présente PROMISE, un cadre innovant qui améliore significativement l'automatisation de la génération de preuves formelles en reformulant le processus comme une recherche d'état basée sur l'imitation structurelle du raisonnement humain, surpassant ainsi les méthodes existantes sur des benchmarks complexes comme seL4.

Auteurs originaux : Youngjoo Ahn, Sangyeop Yeo, Gijung Lim, Jongmin Lee, Jinyoung Yeo, Jieung Kim

Publié 2026-04-08

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Youngjoo Ahn, Sangyeop Yeo, Gijung Lim, Jongmin Lee, Jinyoung Yeo, Jieung Kim

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🧱 PROMISE : Comment apprendre à un robot à construire des preuves mathématiques sans se perdre

Imaginez que vous devez construire une cathédrale géante, pierre par pierre. C'est ce que font les ingénieurs logiciels quand ils vérifient formellement des systèmes critiques (comme le noyau d'un système d'exploitation qui gère des avions ou des hôpitaux). Chaque "pierre" est une preuve mathématique qui garantit qu'il n'y a pas de faille de sécurité.

Le problème ? C'est un travail épuisant. Pour construire la cathédrale seL4 (un système d'exploitation ultra-sécurisé), des humains ont dû passer des décennies à poser chaque pierre manuellement. C'est comme essayer de construire un gratte-ciel en utilisant uniquement des cuillères en plastique : c'est possible, mais c'est lent et risqué.

Récemment, l'intelligence artificielle (les "LLM" comme ChatGPT) est arrivée pour aider. Mais jusqu'à présent, ces IA étaient un peu comme des touristes perdus : elles pouvaient écrire de jolies phrases, mais elles se perdaient dès qu'elles devaient construire une structure complexe avec des milliers de dépendances. Elles regardaient le texte de la demande et essayaient de deviner la suite, souvent en se trompant.

PROMISE est une nouvelle méthode qui change la donne. Voici comment elle fonctionne, avec des analogies simples.

1. Le problème : Chercher l'aiguille dans la botte de foin (Méthode ancienne)

Les anciennes méthodes d'IA fonctionnaient un peu comme un moteur de recherche Google classique.

L'approche : Si vous demandez à l'IA de prouver une chose, elle cherche dans sa mémoire des textes qui contiennent les mêmes mots-clés.
L'analogie : Imaginez que vous essayez de réparer une montre complexe. Vous demandez à un assistant : "Comment réparer une montre ?" et il vous donne un manuel qui parle de "montres" et de "ressorts". Mais il ne vous dit pas comment tourner la vis spécifique à ce moment précis.
Le résultat : L'IA trouve des preuves qui ressemblent aux vôtres par les mots, mais pas par la logique. C'est comme essayer de suivre une recette de gâteau en lisant seulement les ingrédients, sans savoir l'ordre des étapes. Ça ne marche pas pour les gros projets.

2. La solution PROMISE : Suivre les traces de pas (L'approche nouvelle)

PROMISE ne regarde plus les mots. Il regarde la structure du mouvement.

L'analogie de l'escalier : Imaginez que prouver un théorème, c'est monter un escalier très haut.
- Les anciennes méthodes regardaient la photo de l'escalier et disaient : "Ah, cet escalier ressemble à celui de la maison d'à côté, je vais essayer de monter comme ça."
- PROMISE, lui, regarde comment on monte les marches. Il observe les "traces de pas" : Comment l'ingénieur humain a-t-il fait pour passer de la marche 10 à la marche 11 ? A-t-il glissé ? A-t-il utilisé une main courante ?
Le fonctionnement : Au lieu de chercher un texte similaire, PROMISE cherche des séquences de mouvements similaires. Il dit : "Attends, dans ce cas précis, pour passer de l'état A à l'état B, les humains ont toujours fait telle manipulation. Allons-y !"

3. Comment PROMISE "pense" (Le processus)

PROMISE fonctionne comme un explorateur très méthodique qui ne se contente pas de deviner, mais qui vérifie chaque pas.

Il regarde le paysage (Recherche Structurelle) : Au lieu de chercher des mots, il compare la forme de votre problème actuel avec des problèmes passés. "Tiens, ce problème ressemble à celui que j'ai vu il y a deux ans, où l'on a dû faire trois pas précis pour avancer."
Il choisit ses outils (Recherche de Noms) : Une fois qu'il sait comment bouger, il cherche les bons outils (les théorèmes exacts) dans la boîte à outils pour faire ce mouvement.
Il teste et corrige (La Boucle de Vérification) :
- L'IA propose un mouvement.
- Un "gardien" (le logiciel de vérification Isabelle) vérifie si le mouvement est légal.
- Si c'est faux, on essaie une autre voie.
- Si c'est juste, on avance d'un cran.
- C'est comme un jeu d'échecs où l'IA ne joue pas au hasard, mais explore plusieurs coups possibles en même temps pour trouver le chemin le plus sûr.

4. Pourquoi c'est une révolution ?

Les résultats montrent que PROMISE est bien plus efficace que les méthodes précédentes, surtout sur les gros projets comme seL4.

Résistance aux modèles : Que vous utilisiez une petite IA (gratuite) ou une grosse IA (très puissante), PROMISE fonctionne aussi bien. C'est comme si le système de navigation (PROMISE) était si bon que même un conducteur débutant arrive à destination aussi vite qu'un pilote d'essai.
Évolutivité : Là où les autres méthodes s'effondrent quand le projet devient trop grand (comme un gratte-ciel), PROMISE continue de grimper parce qu'il comprend la logique de la construction, pas juste les mots.

En résumé

PROMISE ne demande pas à l'IA de "rêver" d'une preuve parfaite d'un coup. Il lui apprend à imiter la façon dont les humains raisonnent pas à pas.

Au lieu de chercher un texte similaire dans une bibliothèque, il cherche des patterns de mouvement dans l'histoire de la construction. C'est comme passer d'un apprenti qui lit le manuel à un apprenti qui regarde les traces de pas de son maître pour savoir exactement où poser ses pieds.

C'est un pas de géant vers l'automatisation de la sécurité des logiciels critiques, rendant notre monde numérique plus sûr, sans avoir besoin de décennies de travail humain pour chaque nouvelle mise à jour.

1. Problématique et Contexte

La vérification formelle de logiciels (notamment pour les systèmes critiques comme les micro-noyaux) offre des garanties mathématiques de correction, mais son adoption reste limitée par son coût humain et son manque de scalabilité. La construction de preuves interactives (ITP) nécessite des années d'efforts d'experts, comme l'a démontré le projet de vérification du micro-noyau seL4.

Bien que les Grands Modèles de Langage (LLM) aient montré des résultats prometteurs dans la génération de code et de preuves mathématiques simples, ils échouent souvent à l'échelle des grands projets de vérification système. Les approches actuelles souffrent de deux limitations majeures :

Génération en un seul coup (Single-shot) ou recherche superficielle : Elles traitent la génération de preuves comme une tâche de prédiction de tactique isolée ou une simple récupération de texte (RAG) basée sur la similarité lexicale.
Ignorance de la structure profonde : Elles ne capturent pas les dépendances structurelles complexes entre les modules, les fichiers et les couches d'abstraction, ni l'évolution dynamique de l'état de la preuve.

Le papier identifie que les ingénieurs humains ne raisonnent pas seulement par similarité de texte, mais en suivant des motifs d'évolution de l'état de la preuve (séquences de transformations de buts, d'hypothèses et de contextes).

2. Méthodologie : Le Framework PROMISE

PROMISE (PROof MIning via Structural Embeddings) est un cadre d'extraction de preuves qui reformule la génération de preuves comme un processus de recherche itérative et étatique, guidé par la similarité structurelle plutôt que textuelle.

Architecture et Flux de Travail

Le système fonctionne via une recherche en faisceau (Beam Search) sur les états de preuve Isabelle/HOL, plutôt que par une génération linéaire.

Modélisation par États de Preuve : Une preuve est vue comme une séquence de transitions d'états ( $s_0 \xrightarrow{t_1} s_1 \dots \xrightarrow{t_n} s_n$ ), où chaque étape modifie les buts et les hypothèses.
Générateur de Commandes (C) : Pour chaque nœud de la recherche (état de preuve courant), le système :
- Récupération Structurelle (Structural Retrieval) : Au lieu de chercher des lemmes similaires par mots-clés, PROMISE recherche des traces de transition d'états de preuve historiquement réussis qui ressemblent structurellement à l'état actuel. Cela permet de réutiliser des schémas de raisonnement (ex: "réécriture suivie de simplification").
- Récupération de Noms (Name Retrieval) : Identification des lemmes et définitions concrets disponibles dans le contexte actuel pour ancrer la génération.
- Construction de Prompt : Création d'un prompt "few-shot" contenant des modèles de tactiques structurelles (sans les noms de lemmes spécifiques pour éviter le copier-coller) et un inventaire de théorèmes valides.
- Génération et Filtrage : Le LLM génère plusieurs candidats de tactiques. Ceux-ci sont normalisés, filtrés statiquement (syntaxe, validité) puis vérifiés par l'assistant de preuve Isabelle via un pont Scala-Isabelle.
Recherche en Faisceau (Beam Search) : Les candidats valides sont notés selon une fonction de score qui privilégie la réduction du nombre de sous-buts, la concision de la preuve et la diversité des tactiques utilisées. Le processus itère jusqu'à ce que la preuve soit close ou que les limites de profondeur/budget soient atteintes.

Points Clés Techniques

Indépendance du modèle : PROMISE fonctionne avec n'importe quel LLM (GPT-3.5, GPT-4, Qwen2.5) sans entraînement supplémentaire (model-agnostic).
Prévention des fuites (Leakage Prevention) : Le système s'assure strictement que la preuve originale de la cible n'est jamais utilisée comme exemple de récupération.
Vérification Machine : Chaque étape est validée par Isabelle, garantissant que seules les preuves mathématiquement correctes sont acceptées.

3. Contributions Clés

Nouvelle Perspective de la Génération de Preuves : Passage d'une vue basée sur la prédiction de tactiques ou la récupération de texte à une vue basée sur l'évolution structurelle des états de preuve.
Framework PROMISE : Un système opérationnel qui combine la récupération de motifs de transition structurels et la sélection de lemmes contextuels pour guider une recherche de preuve étatique.
Évaluation Complexe : Une évaluation rigoureuse sur le benchmark seL4/l4v (223 théorèmes), couvrant des dépendances inter-fichiers complexes, des preuves de sécurité et des logiques de séparation.

4. Résultats Expérimentaux

Les expériences ont été menées sur le benchmark seL4 en utilisant plusieurs modèles (Qwen2.5-Coder-7B, GPT-3.5-Turbo, GPT-4.1) et comparées à des états de l'art comme Selene et Rango.

Performance Supérieure : PROMISE surpasse systématiquement les approches précédentes.
- Sur le modèle Qwen2.5-Coder-7B, PROMISE atteint un taux de réussite global de 56,5 %, contre 34,0 % pour Rango et 26,8 % pour Selene (ACC5).
- Les gains relatifs atteignent jusqu'à +186 % (soit +26 points absolus) par rapport aux meilleures bases de référence dans certains scénarios.
Robustesse aux Modèles : Contrairement aux autres méthodes dont la performance varie fortement selon la puissance du LLM, PROMISE maintient des performances stables à travers différents modèles (de 7B à GPT-4), démontrant que la stratégie de récupération structurelle compense les faiblesses des modèles plus petits.
Cas d'Échec (GPT-4/P2) : La seule exception où Rango est légèrement meilleur (2 points) sur GPT-4 pour les preuves de niveau P2 est attribuée à une sur-contrainte du prompt de PROMISE qui limite la capacité de raisonnement natif de GPT-4, suggérant que les modèles très avancés peuvent parfois mieux performer avec moins de guidage structurel rigide.

5. Signification et Impact

Ce travail démontre que la scalabilité de l'automatisation des preuves pour les systèmes logiciels réels ne dépend pas uniquement de la puissance brute des LLM, mais de la façon dont l'information est récupérée et structurée.

Changement de Paradigme : Il prouve que la récupération de motifs structurels (comment une preuve évolue) est plus efficace que la récupération de contenu statique (quel lemme est utilisé).
Faisabilité Industrielle : En réussissant à automatiser une partie significative des preuves sur seL4 (un système complexe avec des centaines de milliers de lignes de preuves), PROMISE ouvre la voie à une réduction drastique du coût humain de la vérification formelle.
Fondation pour l'Avenir : L'approche suggère que les futurs systèmes de vérification doivent intégrer des mécanismes de "mining" structurel pour gérer les dépendances complexes des grands projets logiciels, rendant la vérification formelle plus accessible et scalable.

En résumé, PROMISE transforme la génération de preuves d'une tâche de prédiction textuelle en un processus de recherche guidée par la structure, imitant la manière dont les ingénieurs humains réutilisent des schémas de raisonnement éprouvés à travers de vastes bases de code.