Résumé - Vers la vérification formelle du code généré par des LLM à partir de prompts naturels

Vers la vérification formelle du code généré par des LLM à partir de prompts naturels

2025-07-17 16:54:42

{"Aaron Councilman","David Fu","Aryan Gupta","Chengxiao Wang","David Grove","Yu-Xiong Wang","Vikram Adve"}

{cs.PL,cs.AI}

Le papier propose un système appelé Astrogator pour vérifier la correctnesse du code généré par des Modèles de Langage à Grande Echelle (LLMs) à partir de descriptions naturelles. L'objectif est de fournir des garanties formelles de correctness, améliorer l'expérience d'utilisation des assistants IA pour le codage et permettre le développement de logiciels en langage naturel aux utilisateurs possédant peu ou pas de connaissances en programmation. ### Points Clés : * **Défi** : Les LLMs génèrent souvent un code incorrect difficile à détecter par les utilisateurs. Cela constitue un problème significatif dans les environnements de développement de logiciels en langage naturel et des assistants IA pour le codage. * **Solution** : Astrogator intègre un langage de requête formel pour représenter l'intention de l'utilisateur et vérifier le code généré par les LLMs par rapport à lui. * **Langage de Requête Formel** : Le langage est conçu pour être proche de la syntaxe du langage naturel mais bien défini. Il utilise des concepts de haut niveau et une base de connaissances pour éviter l'ambiguïté. * **Vérification** : Astrogator utilise l'interprétation symbolique et un calcul pour représenter le comportement des programmes Ansible et vérifier leur correctness. * **Évaluation** : Sur un ensemble de benchmark de 21 tâches de génération de code, Astrogator a pu vérifier le code correct dans 83% des cas et identifier le code incorrect dans 92%. ### Contributions Clés : 1. **Formalisation du Développement de Logiciels en Langage Naturel** : Définit un cadre formel pour le développement de logiciels en langage naturel et la correctness. 2. **Langage de Requête Formel** : Propose un langage de requête formel pour capturer l'intention de l'utilisateur et faciliter la vérification. 3. **Approche de Vérification** : Développe une approche de vérification utilisant l'interprétation symbolique et un calcul. 4. **Implémentation** : Met en œuvre le système dans Astrogator pour le langage de programmation Ansible. 5. **Évaluation** : Évalue le système sur un ensemble de benchmark et démontre son efficacité. ### Limitations : * **Support Limité du Langage** : Ne prend actuellement en charge que le langage Ansible. * **Langage de Requête Limité** : Le langage de requête formel et la base de connaissances nécessitent un développement supplémentaire. * **Gestion des Hypothèses** : Le système peut accepter un code incorrect sous certaines hypothèses, nécessitant une intervention de la part de l'utilisateur. ### Conclusion : Astrogator est une approche prometteuse pour vérifier la correctnesse du code généré par les LLMs. Il fournit un cadre formel pour le développement de logiciels en langage naturel et démontre son efficacité sur un ensemble de benchmark. Un développement supplémentaire est nécessaire pour résoudre les limitations et étendre le support linguistique.