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.

Cobblestone: un enfoque de "divide y vencerás" para automatizar la verificación formal

Created by
  • Haebom

Autor

Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First

Describir

Este artículo propone Cobblestone, una novedosa herramienta de síntesis de pruebas que aprovecha un modelo de lenguaje a gran escala (LLM) para mejorar la eficiencia de la verificación formal mediante asistentes de prueba como Coq. Cobblestone genera posibles pruebas utilizando el LLM, que posteriormente se utilizan para dividir el problema en partes más pequeñas. Identifica automáticamente las partes probadas con éxito e itera sobre las partes restantes para finalmente producir una prueba correcta. A pesar de la incertidumbre del LLM, Cobblestone garantiza la corrección de las pruebas generadas. Los resultados experimentales muestran que Cobblestone supera a las herramientas de vanguardia existentes, demostrando muchos teoremas que otras herramientas basadas en LLM no logran demostrar. Su eficiencia queda demostrada por un coste medio de ejecución de 1,25 $ y un tiempo de ejecución de 14,7 minutos. Además, puede utilizar la información externa de los usuarios u otras herramientas para aprovechar la estructura de la prueba o lemas relacionados, demostrando hasta el 58 % de los teoremas. Este estudio demuestra el potencial de aprovechar el progreso parcial y la información externa para mejorar la eficiencia de la automatización de la verificación formal.

Takeaways, Limitations

•
Takeaways:
◦
Demostramos que la síntesis de pruebas mediante métodos de dividir y vencer utilizando LLM puede mejorar significativamente la eficiencia de la automatización de la verificación formal.
◦
Supera las limitaciones de las herramientas existentes basadas en LLM y presenta nuevas posibilidades para demostrar más teoremas.
◦
Destacamos la importancia de las estrategias para aprovechar eficazmente el progreso parcial y los insumos externos en la automatización de la verificación formal.
◦
Proporciona un método rentable para automatizar la verificación formal.
•
Limitations:
◦
Depende del rendimiento de LLM, y las limitaciones de LLM pueden afectar el rendimiento de Cobblestone.
◦
El rendimiento aún puede estar limitado para ciertos tipos de limpiezas.
◦
El alcance de los conjuntos de datos de referencia puede ser limitado y se necesita una evaluación del desempeño en una variedad más amplia de problemas.
👍
Made with Slashpage