Vérification de Programmes à l'Ère de l'IA : Pourquoi les Hallucinations Rendent la Vérification de Code Plus Important

L'IA générative a ravivé un vieux rêve des programmeurs : énoncez simplement une tâche — et la machine écrira le code elle-même. Une nouvelle étude académique tempère cet optimisme, sans nier le progrès réel : la programmation ne représente qu'une petite partie de l'ingénierie logicielle, et ses parties les plus difficiles — les exigences, l'architecture et la vérification — restent toujours du ressort des ingénieurs.

Pourquoi l'IA ne Résout pas le Problème Principal

L'ingénierie logicielle ne consiste pas seulement à écrire du code. Les enquêtes de l'industrie montrent : les développeurs consacrent de 20 à 30 % de leur temps de travail à la programmation directe. Le reste est consacré à la collecte des exigences, à la conception de l'architecture, à l'examen, aux tests et à la correction des erreurs. Les assistants IA peuvent générer des fonctions et expliquer un code inconnu, mais ils ne peuvent pas prouver la correction du système dans son ensemble — c'est une tâche fondamentalement différente.

Le principal problème est les hallucinations. L'IA propose en toute confiance un code qui semble plausible, qui se compile et réussit les tests de base, mais qui contient des erreurs logiques subtiles. Des composants « presque corrects » empilés ensemble forment un système peu fiable. Les auteurs ont rassemblé des incidents documentés avec du code généré par IA en production : des citations légales incorrectes dans les chatbots aux erreurs dans les algorithmes de recommandation médicale. Le schéma est le même : le système fonctionnait correctement dans la plupart des cas — jusqu'à ce qu'il rencontre un cas limite.

Expérience avec AutoProof et Eiffel

Les chercheurs ne se sont pas limités à la théorie et ont mené une expérience concrète. Un système de gestion de conférences a été créé à l'aide d'un assistant IA en conjonction avec AutoProof — un vérificateur formel pour le langage Eiffel. La différence fondamentale avec les tests : la vérification formelle prouve la correction pour toutes les entrées possibles, et non seulement pour un ensemble d'exemples sélectionnés.

Le processus a exigé une discipline itérative stricte :

• Formuler un petit fragment d'exigences comme des pré- et postconditions formelles
• Demander à l'assistant IA d'implémenter le code correspondant
• Exécuter AutoProof et obtenir une erreur de vérification ou une confirmation de correction
• Corriger la spécification ou l'implémentation — et répéter le cycle

Observation clé : l'assistant IA n'a pas vérifié le code indépendamment. Il a aidé à formuler les spécifications et à écrire l'implémentation, tandis qu'un vérificateur formel indépendant vérifiait la correction. Cette division des rôles est fondamentale — et, selon les auteurs, c'est ainsi que seront organisées les chaînes d'outils de prochaine génération.

Fédération d'Agents comme Nouveau Paradigme

Les auteurs proposent une nouvelle perspective sur le développement : non pas un seul assistant IA, mais une fédération d'agents interagissant avec des zones claires de responsabilité. L'un génère le code, un deuxième écrit les tests, un troisième exécute la vérification formelle, un quatrième analyse les incidents de production. Aucun agent n'est entièrement responsable de la correction — c'est une propriété du système dans son ensemble.

« L'hallucination comme type de défaillance rend les garanties de

correction plus, et non moins importantes », affirment les auteurs.

Cette approche exige que les développeurs comprennent l'ingénierie logicielle classique : les spécifications formelles, les invariants, les contrats. L'IA n'élimine pas ces connaissances — elle rend son application pratique plus accessible. Un développeur capable de formuler les exigences avec précision et de lire les résultats du vérificateur est dans une position fondamentalement avantageuse.

Ce Que Cela Signifie

La conclusion des auteurs est prudemment optimiste. Pour le développement quotidien, l'IA est une technologie de nivellement : un développeur sans expérience se rapproche d'un développeur expérimenté, le code routinier est écrit plus rapidement, les erreurs évidentes sont trouvées plus tôt. Pour les systèmes critiques et métier, l'IA devient une technologie d'amplification : un ingénieur expérimenté obtient un outil puissant, mais les leçons classiques de l'ingénierie logicielle s'appliquent plus que jamais. La vérification devient non moins, mais plus importante — précisément parce que l'IA peut faire des erreurs avec confiance et de manière invisible.