La technique de prompts structurés mise au point par les chercheurs de Meta donne aux LLM la capacité de vérifier des correctifs de code sans les exécuter avec une précision pouvant atteindre jusqu’à 93% lors des tests. Cette méthode baptisée « raisonnement semi-formel », pourrait contribuer à réduire la dépendance vis-à-vis des environnements sandbox gourmands en ressources actuellement nécessaires à la validation automatisée du code. Cette avancée intervient alors que les entreprises cherchent à déployer des agents IA pour des tâches comme la détection de bogues et la validation de correctifs. Les approches traditionnelles basées sur l'exécution peinent souvent à s'adapter à des bases de code volumineuses et hétérogènes. Au lieu d'utiliser un raisonnement libre pouvant conduire à des hallucinations, cette technique introduit des certificats logiques structurés. Ceux-ci exigent que les modèles énoncent explicitement leurs hypothèses et retracent les chemins d'exécution avant de tirer une conclusion.

L’approche a été évaluée sur trois tâches clés, à savoir la vérification de l'équivalence des correctifs, la localisation des défauts et la réponse aux questions sur le code. Les chercheurs ont constaté que le raisonnement semi-formel améliorait la précision pour chacune d'entre elles. « En ce qui concerne l'équivalence des correctifs, la précision passe de 78 % à 88 % sur des exemples sélectionnés avec soin et atteint 93 % sur des correctifs générés par des agents en conditions réelles, se rapprochant ainsi de la fiabilité requise pour les signaux de récompense en apprentissage par renforcement sans exécution », ont déclaré les chercheurs dans leur article. Pour la réponse aux questions sur le code, la méthode atteint une précision de 87 %, soit une amélioration de neuf points de pourcentage par rapport au raisonnement agentique standard. En matière de localisation des défauts, il augmente la précision du Top 5 de cinq points de pourcentage par rapport aux approches standard.

Des modèles de raisonnement structurés

Le raisonnement semi-formel occupe un juste milieu entre le chat non structuré et la vérification formelle rigide. Alors que le raisonnement standard propose aux modèles de faire des affirmations sans justification, cette approche utilise un modèle prédéfini qui impose un processus étape par étape. « Plutôt que de former des LLM spécialisés ou de formaliser la sémantique, nous fournissons aux agents des modèles de raisonnement structurés qui exigent des preuves explicites pour chaque affirmation », ont expliqué les chercheurs. Ils précisent que « les LLM agissent comme des certificats : l’agent doit énoncer les prémisses, tracer les chemins de code pertinents et fournir des conclusions formelles. Le format structuré encourage naturellement le raisonnement inter-procédural, car la cartographie des chemins de programme oblige l’agent à suivre les appels de fonction plutôt que de deviner leur comportement. »

En pratique, cela oblige le modèle à se comporter comme un développeur parcourant le code ligne par ligne. Les chercheurs ont indiqué que, dans un cas impliquant le framework Django, l’approche structurée avait révélé qu’une fonction au niveau du module masquait la fonction format() intégrée à Python. Alors que le raisonnement standard n’avait pas saisi cette nuance, l’analyse semi-formelle a correctement identifié que le code échouerait.

Un changement de paradigme avec des limites

Selon les analystes, le raisonnement semi-formel marque un tournant dans l’ingénierie logicielle, passant d’une IA d’assistance à une IA plus responsable, une distinction qui pourrait redéfinir la manière dont les entreprises abordent la révision du code. « Des outils comme GitHub Copilot ont habitué les développeurs à interagir avec l'IA comme s'il s'agissait d'un moteur de suggestions rapide et fluide », a déclaré Sanchit Vir Gogia, analyste en chef chez Greyhound Research. « Vous demandez, il génère, vous acceptez ou modifiez. Le système est optimisé pour la rapidité et la plausibilité. Ce pour quoi il n’est pas optimisé, c’est la preuve. » La méthode des chercheurs de Meta modifie cette dynamique. Au lieu de récompenser les modèles pour leur apparence correcte, il leur impose de démontrer leur justesse en retraçant la logique et en fondant leurs conclusions. Pour les développeurs, l’attention se déplace de la révision des résultats à l’évaluation du raisonnement qui les sous-tend. « Cela implique plus profondément que la révision de code elle-même commence à évoluer », a fait remarquer M. Gogia. « Historiquement, la révision de code a constitué un goulot d’étranglement humain lié autant au transfert de connaissances et à la validation de la conception qu’à la détection des bogues. Dans la pratique, elle ne parvient souvent pas à détecter les problèmes critiques tout en ralentissant l’intégration. Ce à quoi nous assistons aujourd’hui, c’est l’ébauche d’une couche de vérification pilotée par des machines, dans laquelle le système suit la logique et l’humain valide le résultat. »

Ce changement n'est toutefois pas sans compromis. Le raisonnement structuré entraîne une charge supplémentaire en termes de calcul et de flux de travail, ce qui soulève des questions quant à la manière dont il devrait être déployé dans des environnements de développement réels. « Plus d’étapes, plus de tokens, plus de latence », a pointé M. Gogia. « Dans des expériences contrôlées, cela peut se justifier par une plus grande précision. Dans les environnements de développement réels, cela se traduit par des builds plus lents, des cycles de feedback plus longs et une augmentation des dépenses d’infrastructure. Si cela est appliqué sans discernement, les développeurs le contourneront. Non pas parce qu’ils ne sont pas d’accord avec ce système, mais parce qu’il les gêne. » Il existe également un risque technique. Les chercheurs ont remarqué que si le format structuré réduit les conjectures, il peut aussi produire des réponses « sûres mais erronées ». Dans ces cas-là, l’IA construit une chaîne de raisonnement élaborée mais incomplète, présentant une conclusion incorrecte sous un format convaincant et hautement structuré qu’un humain aura peut-être du mal à réfuter rapidement.