FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

Le papier présente FM-Agent, un cadre innovant utilisant des LLM pour automatiser le raisonnement compositionnel de type Hoare sur de grands systèmes en générant des spécifications de fonctions à partir des intentions des développeurs exprimées en langage naturel, permettant ainsi de découvrir des centaines de bugs critiques dans des codebases de plus de 143 000 lignes.

L'essentiel

Imaginez que vous demandez à un robot très intelligent (un modèle de langage, ou LLM) de construire une immense cathédrale en Lego, pièce par pièce, sans jamais vous montrer les plans. Le robot est rapide et créatif, mais il a tendance à faire des erreurs subtiles : un mur penche, une fenêtre est mal placée, ou une fondation est fragile.

Le problème, c'est que la cathédrale est si grande (des centaines de milliers de pièces) que même les meilleurs architectes humains ne peuvent pas vérifier chaque brique manuellement. C'est là qu'intervient FM-Agent, le nouveau héros de cette histoire.

Voici comment fonctionne ce système, expliqué simplement :

1. Le problème : Le "Brouillard" de la complexité

Traditionnellement, pour vérifier si un logiciel est correct, il faut écrire un "contrat" très précis pour chaque fonction (une petite partie du code). C'est comme écrire une règle stricte pour chaque brique Lego : "Si vous mettez cette brique rouge ici, elle doit supporter exactement 5 kg."

• Le hic : Écrire ces contrats prend des années. De plus, quand le code est généré par une IA, personne ne connaît vraiment l'intention derrière chaque ligne. Si on écrit le contrat en regardant seulement le code (qui peut être faux), on risque de valider une erreur.

2. La solution de FM-Agent : L'approche "Top-Down" (Du haut vers le bas)

Au lieu de regarder la brique et de deviner ce qu'elle devrait faire, FM-Agent regarde ce que le voisin attend de la brique.

• L'analogie du chef d'orchestre : Imaginez un chef d'orchestre (le code qui appelle la fonction) qui dit à un musicien (la fonction) : "J'ai besoin que tu joues une note aiguë et claire."
• FM-Agent écoute ce que le chef demande. Même si le musicien joue faux (bug), FM-Agent sait que l'intention était "note aiguë". Il compare donc la performance réelle avec la demande du chef, et non avec la performance du musicien.
• Résultat : Si le musicien joue une note grave, FM-Agent crie : "Attends ! Le chef voulait du aigu ! Il y a un bug !"

3. La magie du langage naturel

Les vérificateurs classiques parlent une langue mathématique compliquée (des formules). Les humains et les IA parlent français (ou anglais).

• L'innovation : FM-Agent parle le langage des humains. Il comprend que "le moteur doit s'arrêter si la température dépasse 100 degrés" est une spécification valide, sans avoir besoin de la traduire en équations mathématiques. Il utilise l'IA pour raisonner directement sur ces phrases simples, comme un inspecteur de police qui lit un rapport.

4. Le test final : Le "Choc de réalité"

Parfois, l'IA peut halluciner et penser qu'il y a un bug alors qu'il n'y en a pas. Pour éviter de crier au loup pour rien, FM-Agent a un troisième bras : le Validateur de Bugs.

• L'analogie du test de crash : Si FM-Agent soupçonne un problème, il ne se contente pas de dire "Je pense que c'est faux". Il écrit un petit programme (un test) pour provoquer le bug.
• C'est comme si un ingénieur disait : "Je pense que cette porte est mal verrouillée." Au lieu de juste le noter, il prend un marteau, tape sur la porte, et regarde si elle s'ouvre. Si elle s'ouvre, le bug est confirmé. Si elle résiste, c'était une fausse alerte.

Les résultats concrets

Les chercheurs ont testé FM-Agent sur des systèmes énormes (un compilateur, un système d'exploitation, une base de données), tous créés par des IA.

• Le bilan : En seulement 2 jours, FM-Agent a trouvé 522 nouveaux bugs que les développeurs (humains et IA) avaient manqués.
• La gravité : Certains de ces bugs auraient pu faire planter tout le système, corrompre des données ou créer des failles de sécurité.

En résumé

FM-Agent, c'est comme un inspecteur de contrôle qualité ultra-rapide qui :

1. Écoute ce que le client veut (l'intention), pas ce que l'ouvrier a fait (le code).
2. Parle la langue humaine pour comprendre les règles.
3. Fait des tests réels pour prouver que le problème existe vraiment.

C'est une avancée majeure pour s'assurer que les géants du code générés par l'IA ne s'effondrent pas sur eux-mêmes.

Résumé technique

1. Problématique

L'essor du développement logiciel assisté par les grands modèles de langage (LLM) permet de générer des systèmes à grande échelle (par exemple, des compilateurs de plus de 100 000 lignes de code). Cependant, ces systèmes contiennent souvent des bogues dus aux hallucinations des LLMs.
La vérification formelle automatique de ces systèmes se heurte à deux obstacles majeurs :

• Complexité et échelle : Les techniques existantes (exécution symbolique, vérificateurs semi-automatiques) peinent à passer à l'échelle en raison de l'explosion des chemins d'exécution et de la complexité des dépendances inter-procédures.
• Le goulot d'étranglement des spécifications : La logique de Hoare, qui permet un raisonnement compositionnel (vérifier chaque fonction indépendamment), nécessite des spécifications formelles précises pour chaque fonction. Rédiger ces spécifications manuellement est trop coûteux. De plus, lorsque le code est généré par des LLMs, les développeurs manquent souvent de compréhension profonde du comportement attendu, rendant la rédaction de spécifications précises encore plus difficile. Les méthodes existantes qui génèrent des spécifications à partir de l'implémentation échouent car l'implémentation elle-même peut être erronée.

2. Méthodologie : FM-Agent

FM-Agent est le premier cadre de travail permettant un raisonnement compositionnel automatisé pour des systèmes à grande échelle. Il repose sur trois piliers principaux utilisant les LLMs :

A. Génération de Spécifications "Top-Down" (Du haut vers le bas)

Contrairement aux approches traditionnelles qui déduisent le comportement à partir du code (bottom-up), FM-Agent adopte une approche descendante :

• Principe : Il dérive les spécifications d'une fonction (pré-conditions et post-conditions) en analysant comment ses appelants (callers) l'utilisent et ce qu'ils en attendent.
• Avantage : Cela capture l'intention du développeur (ou de l'agent de codage) plutôt que le comportement potentiellement buggé de l'implémentation. Si une fonction est appelée par plusieurs entités, FM-Agent fusionne les attentes de chaque appelant pour créer une spécification complète.
• Planification : L'algorithme détermine un ordre de génération partiel (basé sur le graphe d'appels et les composantes fortement connexes) permettant de générer des spécifications pour de multiples fonctions en parallèle.

B. Raisonnement de Style Hoare sur le Langage Naturel

FM-Agent généralise les règles d'inférence de la logique de Hoare pour fonctionner directement avec des spécifications en langage naturel :

• Inférence itérative : À partir de la pré-condition, le système utilise un LLM pour inférer la post-condition de chaque bloc de code (instructions, boucles, branches).
• Vérification : Si la post-condition finale d'un chemin d'exécution ne peut pas impliquer la post-condition attendue dans la spécification, un bogue potentiel est signalé.
• Précision : Bien que le raisonnement soit en langage naturel, le système peut traduire des conditions précises en formules logiques pour être vérifiées par des solveurs SMT, améliorant ainsi la fiabilité.

C. Validation par Génération de Tests

Pour confirmer la présence d'un bogue et en expliquer la cause :

• FM-Agent génère automatiquement des cas de test au niveau de l'entrée système (et non au niveau de la fonction seule).
• En exploitant la capacité des LLMs à comprendre les corrélations entre les entrées système et le comportement interne, il crée des scénarios qui déclenchent spécifiquement les bogues détectés.
• Un validateur exécute ces tests pour confirmer le bogue, réduisant ainsi les faux positifs dus aux hallucinations du LLM.

3. Contributions Clés

1. Premier cadre de raisonnement compositionnel automatisé : FM-Agent est la première solution capable de raisonner sur des systèmes entiers (jusqu'à 143k lignes de code) sans spécifications formelles manuelles.
2. Paradigme "Caller-Driven" : Une méthode innovante pour générer des spécifications basées sur l'usage attendu par les appelants, rendant le processus robuste face aux implémentations buggées.
3. Extension de la Logique de Hoare : Adaptation des règles d'inférence formelles pour opérer sur des spécifications en langage naturel, comblant le fossé entre l'intention humaine et la vérification formelle.
4. Validation par Tests Systémiques : Une approche qui génère des tests d'intégration pour valider les bogues détectés par le raisonnement, offrant des retours exploitables pour les développeurs.

4. Résultats de l'Évaluation

L'évaluation a été menée sur quatre systèmes à grande échelle générés par des agents de codage (CCC, VibeTensor, VibeOS, Bespoke OLAP), totalisant 277 000 lignes de code et 8 549 fonctions.

• Détection de bogues : FM-Agent a découvert 522 bogues nouveaux, même si ces systèmes avaient déjà été testés et corrigés par leurs développeurs via des méthodes traditionnelles (tests unitaires, intégration, revues de code multi-agents).
• Impact des bogues : Les bogues détectés sont critiques, entraînant des plantages système, des corruptions de mémoire, des résultats de requêtes incorrects ou des boucles infinies.
  • Exemple : Dans le compilateur CCC, 339 bogues ont été trouvés, dont certains provoquant des crashs de compilation ou une génération de code IR incorrecte.
• Performance et Échelle : Le raisonnement sur l'ensemble des systèmes a pris environ 2 jours et a consommé 3,4 milliards de tokens. La méthode permet une forte concurrence (génération de spécifications par phases et couches), ce qui rend l'approche scalable.
• Comparaison : Une version ablation (générant des spécifications uniquement à partir du code, sans approche top-down) n'a trouvé que 57 bogues sur le même système, prouvant l'efficacité cruciale de l'approche basée sur les appelants.

5. Signification et Impact

Ce travail marque une avancée significative dans l'assurance qualité du logiciel généré par l'IA :

• Complémentarité : FM-Agent ne remplace pas les vérificateurs formels classiques (qui garantissent la justesse mais nécessitent des spécifications manuelles), mais il les complète en offrant une méthode scalable pour détecter des bogues dans des systèmes où la vérification formelle traditionnelle est impossible.
• Adaptabilité à l'ère des LLMs : Il répond directement au défi posé par le développement logiciel autonome, où la documentation et la compréhension humaine des détails de l'implémentation sont souvent absentes.
• Futur de la vérification : Il ouvre la voie à une hybridation entre le raisonnement formel et les capacités sémantiques des LLMs, permettant de raisonner sur des spécifications en langage naturel et d'automatiser la découverte de bugs dans des systèmes complexes.

En résumé, FM-Agent démontre qu'il est possible de passer à l'échelle des méthodes formelles pour les systèmes modernes en utilisant les LLMs non seulement pour générer du code, mais aussi pour déduire les intentions, raisonner sur la correction et valider les erreurs de manière autonome.