Un equipo de investigadores desarrolló SysMoBench, un benchmark automatizado para evaluar si los modelos de lenguaje de gran escala (LLMs) pueden modelar sistemas informáticos reales o simplemente recitan especificaciones de protocolos de manuales académicos. El sistema evalúa once sistemas distribuidos y de sincronización concurrente mediante la generación de especificaciones TLA+, un lenguaje formal para sistemas distribuidos. La evaluación se estructura en cuatro fases: sintaxis, ejecución en tiempo de ejecución, conformidad y verificación de invariantes. Los resultados muestran que los LLMs actuales, incluyendo Claude, GPT, Gemini, DeepSeek, Kimi y Qwen, obtienen puntuaciones casi perfectas en las fases iniciales de sintaxis y ejecución. Sin embargo, al evaluar conformidad con el código real y satisfacción de invariantes, el rendimiento cae drásticamente a aproximadamente 46% y 41% respectivamente. Los investigadores identificaron dos patrones de fallo sistemáticos: especificaciones que admiten estados inalcanzables en sistemas reales, y especificaciones que no pueden alcanzar estados que los sistemas reales sí producen. Un ejemplo concreto es que Claude Sonnet modeló recvset de ZooKeeper como una unión de conjuntos cuando debería ser un mapa con sobrescritura de claves. Según los autores, los LLMs producen módulos estructuralmente completos, pero escritos con plantillas formalizadas de libros de texto en lugar de reflejar la implementación real de cada sistema.
Noticias agregadas con IA