Resumen: Los modelos formales son esenciales para especificar sistemas informáticos grandes y complejos y verificar su corrección, pero son notoriamente caros de escribir y mantener. Los avances recientes en la IA generativa son prometedores para generar ciertas formas de especificaciones. Sin embargo, el trabajo existente se dirige principalmente a un código pequeño, no a sistemas completos. No está claro si la IA puede lidiar con los artefactos del sistema realistas, ya que esto requiere abstraer sus complejas propiedades de comportamiento en modelos formales. Presentamos a SysMobench, un punto de referencia que evalúa la capacidad de IA para modelar formalmente sistemas grandes y complejos. Nos centramos en los sistemas concurrentes y distribuidos, que son piedras clave de las infraestructuras informáticas críticas de hoy, que abarcan sistemas operativos e infraestructura en la nube. Usamos TLA+, el lenguaje de especificación de TI de facto para sistemas concurrentes y distribuidos, aunque el punto de referencia puede extenderse a otros lenguajes de especificación. Abordamos el desafío principal de evaluar modelos generados por IA mediante la automatización de métricas como la corrección sintáctica y de tiempo de ejecución, la conformidad con el código del sistema y la corrección invariante. Sysmobench actualmente incluye nueve artefactos del sistema diversos: la implementación de la balsa de ETCD y Redis, el Spinlock y Mutex en Asterinas OS, etc.; Se agregan más artefactos activamente. Sysmobench nos permite comprender las capacidades y limitaciones de los LLM y agentes de hoy, poniendo herramientas en esta área en una base firme y abriendo nuevas instrucciones de investigación prometedoras.
Publicado Originalme en export.arxiv.org El 29 de septiembre de 2025.
Ver Fuente Original
