Daily Arxiv

Esta página recopila y organiza artículos sobre inteligencia artificial publicados en todo el mundo.
La información aquí presentada se resume utilizando Google Gemini y el sitio se gestiona sin fines de lucro.
Los derechos de autor de los artículos pertenecen a sus autores y a las instituciones correspondientes; al compartir el contenido, basta con citar la fuente.

Mejora de la generación automatizada de invariantes de bucle para programas complejos con modelos de lenguaje grandes

Created by
  • Haebom

Autor

Ruibang Liu, Guoqiang Li, Minyu Chen, Ling-I Wu, Jingyu Ke

Describir

Este artículo propone una herramienta novedosa, ACInv, para abordar los desafíos de la verificación automatizada de programas, crucial para desarrollar software confiable, especialmente al analizar programas reales con estructuras de datos complejas y flujo de control. ACInv genera invariantes de bucle combinando el análisis estático con un modelo de lenguaje a gran escala (LLM). Extrae información de bucle mediante análisis estático y la integra en el prompt del LLM. Posteriormente, utiliza un evaluador basado en LLM para verificar los invariantes generados y fortalecerlos, debilitarlos o rechazarlos para obtener invariantes óptimos. Los resultados experimentales muestran que ACInv supera a las herramientas existentes en conjuntos de datos que contienen estructuras de datos, manteniendo un rendimiento comparable al de la herramienta de vanguardia, AutoSpec, en programas numéricos sin estructuras de datos. ACInv resuelve un 21 % más de ejemplos que AutoSpec en todo el conjunto de datos y genera plantillas de estructuras de datos de referencia.

Takeaways, Limitations

•
Takeaways:
◦
Presentamos un método novedoso que resuelve eficazmente el problema de generar invariantes de bucle para programas complejos combinando análisis estático y LLM.
◦
Supera a las herramientas existentes en programas que incluyen estructuras de datos.
◦
Proporciona la capacidad de crear plantillas de estructuras de datos de referencia.
◦
Verificamos y mejoramos la precisión de los invariantes utilizando un evaluador basado en LLM.
•
Limitations:
◦
El rendimiento de los programas numéricos sin estructuras de datos es comparable al de las herramientas de última generación, pero no muestra mejoras de rendimiento abrumadoras.
◦
Dado que depende del rendimiento de LLM, las limitaciones de LLM pueden afectar el rendimiento de ACInv.
◦
El rendimiento puede variar según el alcance y la diversidad del conjunto de datos experimentales. Podrían requerirse experimentos más exhaustivos.
👍
Made with Slashpage