Resumen - Hacia la Verificación Formal del Código Generado por LLM a partir de Prompts de Lenguaje Natural

Hacia la Verificación Formal del Código Generado por LLM a partir de Prompts de Lenguaje Natural

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}

El documento propone un sistema llamado Astrogator para verificar la corrección del código generado por Modelos de Lenguaje Grandes (LLMs) a partir de descripciones en lenguaje natural. El objetivo es proporcionar garantías formales de corrección, mejorar la experiencia de uso de Asistentes de Código AI y permitir la programación en lenguaje natural para usuarios con poco o ningún conocimiento de programación. ### Puntos Clave: * **Desafío**: Los LLMs a menudo generan código incorrecto que es difícil de detectar para los usuarios. Esto es un problema significativo en el entorno de programación en lenguaje natural y los Asistentes de Código AI. * **Solución**: Astrogator incorpora un lenguaje de consulta formal para representar la intención del usuario y verificar el código generado por los LLMs en función de él. * **Lenguaje de Consulta Formal**: El lenguaje está diseñado para estar cerca de la sintaxis del lenguaje natural pero estar definido de manera precisa. Utiliza conceptos a alto nivel y una base de conocimientos para evitar ambigüedades. * **Verificación**: Astrogator utiliza interpretación simbólica y un cálculo para representar el comportamiento de programas Ansible y verificar su corrección. * **Evaluación**: En una suite de benchmark de 21 tareas de generación de código, Astrogator fue capaz de verificar código correcto en el 83% de los casos e identificar código incorrecto en el 92%. ### Contribuciones Clave: 1. **Formalización de la Programación en Lenguaje Natural**: Define un marco formal para la programación en lenguaje natural y la corrección. 2. **Lenguaje de Consulta Formal**: Propone un lenguaje de consulta formal para capturar la intención del usuario y facilitar la verificación. 3. **Enfoque de Verificación**: Desarrolla un enfoque de verificación utilizando interpretación simbólica y un cálculo. 4. **Implementación**: Implementa el sistema en Astrogator para el lenguaje de programación Ansible. 5. **Evaluación**: Evalúa el sistema en una suite de benchmark y demuestra su efectividad. ### Limitaciones: * **Soporte de Lenguaje Limitado**: Actualmente solo admite Ansible. * **Lenguaje de Consulta Limitado**: El lenguaje de consulta formal y la base de conocimientos necesitan un desarrollo adicional. * **Manejo de Asumpciones**: El sistema puede aceptar código incorrecto bajo ciertas asunciones, requiriendo intervención del usuario. ### Conclusión: Astrogator es un enfoque prometedor para verificar la corrección del código generado por LLMs. Proporciona un marco formal para la programación en lenguaje natural y demuestra su efectividad en una suite de benchmark. Se necesita un desarrollo adicional para abordar las limitaciones y expandir el soporte de lenguaje.