En este artículo, proponemos Astrogator, un sistema que introduce un lenguaje de consulta formal para aclarar la intención del usuario y verificar la corrección del código generado. Esto soluciona el problema de errores de los modelos de lenguaje a gran escala (LLM) que generan código basándose en descripciones en lenguaje natural. Astrogator se basa en el lenguaje de programación Ansible y consta de un lenguaje de consulta formal, un método computacional que representa el comportamiento del programa Ansible y un intérprete simbólico para la verificación. En una prueba comparativa de 21 tareas de generación de código, se verificó código correcto en el 83 % de los casos y se identificó código incorrecto en el 92 %.
