💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

Ce document présente VerIbmc, un pipeline neuro-symbolique qui exploite des modèles de langage locaux à poids ouverts, combinés à la synthèse d'invariants symboliques et à un retour itératif de vérificateur, pour parvenir à une génération d'invariants de boucle de pointe pour la vérification de logiciels, offrant ainsi une alternative respectueuse de la vie privée et rentable aux outils propriétaires basés sur le cloud.

Auteurs originaux : Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Publié 2026-06-16

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

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

Imaginez que vous essayez de prouver qu'une machine complexe (un programme informatique) ne tombera jamais en panne, peu importe le nombre de fois où elle est exécutée. La partie la plus difficile de cette preuve est de comprendre les « boucles » de la machine — les parties où elle répète une tâche encore et encore. Pour prouver que la machine est sûre, vous devez trouver un Invariant de Boucle.

Considérez un Invariant de Boucle comme une « règle de sécurité » qui doit être vraie à chaque fois que la machine commence un nouveau cycle de sa boucle. Par exemple, si une boucle compte à rebours de 10 à 0, la règle de sécurité pourrait être : « Le nombre est toujours compris entre 0 et 10. » Si vous pouvez prouver que cette règle est respectée au début, reste vraie après chaque étape et mène à une fin sécurisée, toute la machine est prouvée sûre.

Le problème est que trouver ces règles automatiquement est incroyablement difficile. C'est comme essayer de deviner la combinaison secrète d'un coffre-fort sans aucun indice.

L'ancienne méthode vs La nouvelle méthode

L'ancienne méthode (Raisonnement symbolique) :
Traditionnellement, les ordinateurs essayaient de trouver ces règles en utilisant des mathématiques et une logique strictes. C'est comme un comptable hyper précis vérifiant chaque chiffre. C'est très fiable, mais c'est lent et cela se bloque souvent sur des problèmes complexes et désordonnés. C'est comme essayer de résoudre un labyrinthe en vérifiant chaque mur un par un.

La méthode du « Cloud » (Grands modèles d'IA) :
Récemment, des gens ont commencé à utiliser de massifs modèles d'Intelligence Artificielle (IA) pour deviner ces règles. Ces IA sont comme des étudiants brillants et très cultivés qui ont lu des millions d'exemples de code. Elles peuvent deviner la bonne règle très rapidement. Cependant, pour les utiliser, vous devez généralement envoyer votre code vers un énorme serveur de cloud coûteux (comme envoyer vos plans secrets à un étranger). C'est mauvais pour les entreprises qui doivent garder leur code privé, et cela coûte beaucoup d'argent.

La Solution : VerIbmc (Le « Super-Assistant » Local)

Les auteurs de cet article ont construit un nouveau système appelé VerIbmc. Considérez cela comme un atelier local où vous pouvez utiliser un assistant IA intelligent sans jamais quitter votre bâtiment.

Voici comment fonctionne VerIbmc, en utilisant une analogie simple :

Imaginez que vous essayiez de résoudre un puzzle difficile (l'invariant de boucle).

Le Détective Déterministe (Phases 0 & 1) : Avant de demander de l'aide à l'IA, VerIbmc envoie un détective strict et logique (un outil appelé ESBMC) pour examiner le puzzle. Le détective vérifie d'abord les faits simples. Si le puzzle est facile, le détective le résout instantanément. S'il trouve quelques indices solides (comme « le nombre est toujours positif »), il les note sur un tableau blanc.
L'Assistant IA Local (Phase 2) : Si le détective est bloqué, il appelle l'Assistant IA Local. Mais voici l'astuce : l'IA ne part pas de zéro. Le détective remet à l'IA le tableau blanc avec les indices qu'il a déjà trouvés.
La Boucle de Rétroaction : L'IA propose une solution complète. Le détective la vérifie.
- Si elle est fausse, le détective ne dit pas simplement « Non ». Il dit : « Cette partie est fausse, mais cette autre partie est en fait correcte. » Il prend la partie correcte, l'écrit sur le tableau blanc et demande à l'IA de réessayer, en utilisant les nouveaux indices.
- Cela se répète encore et encore jusqu'à ce que le puzzle soit résolu ou qu'ils manquent de temps.

Deux façons de penser (CoT vs ToT)

L'article a également testé comment l'IA devrait « penser » pendant la résolution du puzzle :

Chain-of-Thought (CoT - Chaîne de pensée) : L'IA pense de manière linéaire, étape par étape, comme si elle écrivait une seule histoire.
Tree-of-Thoughts (ToT - Arbre de pensées) : L'IA se ramifie, comme un arbre. Elle essaie plusieurs chemins à la fois, voit lequel semble prometteur, et concentre alors son énergie sur les meilleurs chemins. L'article a constaté que pour les modèles d'IA les plus puissants, cette méthode de branchement était excellente, mais pour les modèles plus petits et plus faibles, elle faisait parfois perdre du temps.

Les Résultats : Pourquoi cela importe

Les chercheurs ont testé ce système sur des centaines de différents puzzles de programmation en utilisant cinq modèles d'IA différents à « poids ouverts » (des modèles que n'importe qui peut télécharger et exécuter sur son propre ordinateur).

La vie privée d'abord : Comme tout s'exécute sur une machine locale, aucun code ne quitte l'organisation. C'est comme faire ses devoirs de mathématiques dans sa propre chambre plutôt que de les donner à un étranger.
Rentabilité : Vous n'avez pas besoin de payer des frais coûteux aux grandes entreprises de cloud.
Performance : La meilleure configuration (utilisant un grand modèle local appelé GPT-OSS-120B) a résolu 86,4 % des problèmes. C'est meilleur que de nombreux outils traditionnels et compétitif par rapport aux outils d'IA basés sur le cloud et coûteux.
Le boost « Gratuit » : Le système a découvert que la phase du « Détective » (la partie symbolique) a résolu 75 problèmes toute seule, sans avoir besoin de l'IA. Pour les modèles d'IA plus faibles, les indices du détective les ont aidés à résoudre 35 problèmes de plus qu'ils n'auraient pu en résoudre seuls.

L'essentiel

VerIbmc prouve que vous n'avez pas besoin de supercalculateurs de cloud coûteux et envahissants pour la vie privée pour vérifier la sécurité des logiciels. En combinant un détective logique strict avec un assistant IA local intelligent qui apprend de ses erreurs, vous pouvez obtenir des résultats de haut niveau directement sur votre propre ordinateur. C'est une façon de rendre la vérification de logiciels privée, abordable et puissante.

Résumé technique : Vérification de logiciels neuro-symbolique avec VerIbmc

Énoncé du problème

La synthèse d'invariants de boucle demeure un goulot d'étranglement central dans la vérification formelle de logiciels. Bien que des techniques symboliques (par exemple, l'interprétation abstraite, la résolution de contraintes) et des méthodes pilotées par les données de type « deviner et vérifier » existent, elles peinent souvent face à la scalabilité, l'expressivité ou la diversité des codes réels. Récemment, les grands modèles de langage (LLM) ont montré un potentiel pour générer des invariants candidats en exploitant des motifs appris à partir de corpus de code. Cependant, les approches neuro-symboliques existantes reposent généralement sur des modèles propriétaires fermés, accessibles via des API cloud externes. Cette dépendance introduit des obstacles majeurs pour le déploiement industriel :

Confidentialité et conformité : Le code source doit être transmis à des services tiers, ce qui soulève des préoccupations de confidentialité.
Reproductibilité : La dépendance vis-à-vis de fournisseurs externes complique l'intégration dans des pipelines de vérification contrôlés.
Coût et durabilité : Les modèles de grande taille sont coûteux en termes de calcul et de consommation énergétique, limitant leur application pratique pour les flux de travail de vérification continue.

Les auteurs postulent que ces défis nécessitent une transition vers des modèles de langage à poids ouverts, déployables localement, capables de fonctionner entièrement au sein de l'infrastructure d'une organisation sans exposer le code propriétaire.

Méthodologie : Le pipeline VerIbmc

Le document présente VerIbmc, un pipeline neuro-symbolique conçu pour synthétiser des invariants de boucle pour des programmes C en associant le raisonnement symbolique à des LLM à poids ouverts hébergés localement. Le système utilise ESBC (Efficient SMT-Based Context-Bounded Model Checker) comme oracle de vérification. Le pipeline est conçu selon le principe de « l'escalade uniquement si nécessaire », privilégiant le raisonnement symbolique déterministe et peu coûteux avant de solliciter le LLM.

Architecture centrale

Le pipeline opère en trois phases distinctes :

Phase 0 (Vérification de base) : ESBMC vérifie le programme non annoté. Si le programme est trivialement sûr ou prouvable comme non sûr, le processus se termine immédiatement, évitant ainsi un effort de synthèse inutile.
Phase 1 (Génération de candidats symboliques) : Si la Phase 0 retourne « Inconnu », le système énumère symboliquement des invariants candidats atomiques par comparaison par paires des variables d'entrée de la boucle et des constantes. Ces atomes sont vérifiés pour leur inductivité via ESBC. Le système maintient trois magasins : Prouvable ( $P$ ), Disprovable ( $D$ ) et Inconnu ( $U$ ). Si la conjonction de tous les atomes prouvables suffit à prouver la post-condition, le pipeline se termine avec succès sans aucun appel au LLM.
Phase 2 (Boucle de raffinement par LLM) : Si la phase symbolique est insuffisante, le pipeline entre dans une boucle itérative où un LLM est sollicité pour générer de nouveaux invariants.
- Mécanisme de rétroaction : Le LLM reçoit le programme actuel, le contenu des magasins $P$ , $D$ et $U$ sous forme de rétroaction structurée, ainsi que des exemples de few-shot.
- Décomposition et recombinaison : Lorsqu'un candidat généré par le LLM échoue à la vérification, le système le décompose en sous-formules (atomes). Les atomes sont individuellement vérifiés et ajoutés au magasin approprié. La conjonction de tous les atomes actuellement prouvables est ensuite re-vérifiée. Cela permet de sauvegarder les composants utiles des propositions échouées du LLM.
- Terminaison : La boucle continue jusqu'à ce qu'un invariant valide soit trouvé, que le budget d'itération soit épuisé, ou qu'un délai d'attente (timeout) survienne.

Stratégies d'inférence

Les auteurs évaluent quatre stratégies d'inférence basées sur deux axes de conception :

Rétroaction du vérificateur (Priorité symbolique) :
- Basic (Basique) : Exécute le pipeline complet en trois phases, utilisant le prior symbolique de la Phase 1 et le filtrage par atome.
- LLM-Only (LLM seul) : Ignore la Phase 1 et la décomposition par atome, s'appuyant uniquement sur le LLM pour générer des invariants inductifs en tant qu'entités globales. Cela sert de base d'ablation.
Structure de raisonnement :
- Chain-of-Thought (CoT - Chaîne de pensée) : Utilise un prompting standard avec des exemples de raisonnement étape par étape (Inductif, Logique de Hoare, Clause de Horn ou dérivation directe).
- Tree-of-Thoughts (ToT - Arbre de pensée) : Explore plusieurs styles de dérivation en parallèle lors d'une étape de « reconnaissance » (scouting), les évalue en fonction du nombre d'atomes prouvables générés, et concentre le budget d'itération restant sur les deux meilleurs styles de performance.

Principales contributions

Pipeline neuro-symbolique : Un système complet intégrant des LLM à poids ouverts servis localement avec ESBC pour la synthèse automatisée d'invariants de boucle, opérant entièrement sur l'infrastructure interne.
Évaluation systématique des stratégies : Une comparaison exhaustive des variantes purement LLM, guidées par le symbolique et Tree-of-Thoughts (ToT), démontrant l'impact de la rétroaction symbolique et des structures de raisonnement.
Gains de la rétroaction symbolique : Démonstration que le fait de fournir des atomes d'invariants prouvables comme contexte au LLM produit des gains constants, particulièrement pour les modèles plus faibles (par exemple, Llama-3.1-8B gagne +35 benchmarks résolus par rapport à une base pure-LLM).
Analyse du prompt engineering : Évaluation de différents styles de prompting (CoT vs ToT) et de modèles de raisonnement (Inductif, Logique de Hoare, Clause de Horn) sur la synthèse d'invariants.
Benchmarking à grande échelle : Une évaluation étendue à travers cinq familles de modèles (de 7B à 120 milliards de paramètres), quatre stratégies d'inférence et cinq familles de benchmarks (520 problèmes, 499 effectifs), totalisant 10 400 résultats par problème.

Résultats expérimentaux

L'évaluation a été menée sur un serveur équipé de quatre GPU NVIDIA RTX A6000 en utilisant cinq modèles à poids ouverts : GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B et Llama-3.1-8B.

Performance globale : La meilleure configuration unique (GPT-OSS-120B avec la stratégie Basic) a résolu 431 sur 499 problèmes (86,4 %).
Comparaison avec l'état de l'art (SOTA) :
- VerIbmc surpasse substantiellement les outils symboliques traditionnels (CPA-Checker, 2ls, ESBMC-Kind) et les outils purement neuronaux (Code2Inv) lorsqu'ils sont exécutés sur le même matériel local.
- Sur les ensembles de benchmarks partagés, VerIbmc est compétitif ou légèrement en dessous des outils les plus puissants augmentés par LLM (Clause2Inv, LaM4Inv, LORIS) qui dépendent d'API externes coûteuses (ex: GPT-4). Notamment, VerIbmc atteint ces résultats sans transmettre de code vers le cloud.
- VerIbmc est capable de passer à l'échelle sur l'ensemble complet du benchmark SV-COMP (154 problèmes), incluant des programmes avec des tableaux, des boucles imbriquées et des pointeurs, là où beaucoup d'outils concurrents échouent en raison de limitations de frontend.
Impact de la phase symbolique : La Phase 1 symbolique a résolu 75 problèmes sans aucun appel au LLM. Pour les modèles plus faibles, l'augmentation symbolique a apporté des gains significatifs (jusqu'à +35 problèmes résolus supplémentaires pour Llama-3.1-8B).
ToT vs CoT : Le prompting ToT a montré un arbitrage entre diversité et précision. Bien qu'il ait atteint des paires problème-modèle uniques inaccessibles à CoT, il a souvent engendré un surcoût en temps de calcul (wall-clock) et, pour les modèles plus faibles, a entraîné une diminution nette des problèmes résolus en raison de l'épuisement du budget d'itération. Pour les modèles les plus forts (GPT-OSS-120B), la différence de performance entre CoT et ToT était négligeable.
Capacité du modèle : Les résultats indiquent que la capacité du modèle est le principal moteur de la précision. L'écart entre les modèles les plus forts et les plus faibles est nettement plus important que la variance de performance introduite par le changement de stratégie au sein d'un même modèle.

Signification et affirmations

L'article affirme que VerIbmc démontre qu'une approche neuro-symbolique basée sur les LLM peut être appliquée efficacement à la synthèse d'invariants de manière respectueuse de la vie privée et énergétiquement efficace. En opérant entièrement sur une infrastructure locale avec des modèles à poids ouverts, l'approche élimine le besoin de modèles frontières propriétaires coûteux verrouillés derrière des API.

Les auteurs soulignent que leur méthode est sûre par construction : chaque invariant candidat est validé par un vérificateur formel (ESBMC) avant acceptation. Bien que le système soit incomplet en raison de l'indécidabilité du problème, il offre une voie pratique, scalable et reproductible pour la vérification assistée par IA des logiciels de production. Ce travail constitue un pas vers des pipelines de vérification prêts pour l'industrie, où la confidentialité des données et l'efficacité des ressources sont des exigences critiques.