El éxito local no se compone: evaluación comparativa de modelos de lenguaje extenso para la verificación formal composicional.

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

September 27, 2025

Autores: Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

cs.AI

Resumen

Presentamos DafnyCOMP, un punto de referencia para evaluar modelos de lenguaje de gran escala (LLMs) en la generación de especificaciones composicionales en Dafny. A diferencia de puntos de referencia previos que se centran en tareas de una sola función, DafnyCOMP se enfoca en programas compuestos por múltiples funciones interactivas con dependencias de datos, lo que requiere razonamiento a través de los límites de los componentes. El punto de referencia consta de 300 programas multifunción sintetizados automáticamente. Evaluamos varias familias de LLMs de última generación y encontramos que, aunque tienen un buen desempeño en la verificación de funciones individuales, su rendimiento disminuye drásticamente en tareas composicionales. El análisis revela fallos sistemáticos en el razonamiento entre funciones, incluyendo especificaciones frágiles, desalineación entre implementaciones y pruebas, y razonamiento inestable. DafnyCOMP proporciona así una herramienta diagnóstica para medir el avance hacia la generación de código confiable, verificable y composicional con LLMs.

English

We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-function tasks, DafnyCOMP targets programs composed of multiple interacting functions with data dependencies, requiring reasoning across component boundaries. The benchmark consists of 300 automatically synthesized multi-function programs. We evaluate several state-of-the-art LLM families and find that, while they perform well on single-function verification, their performance drops sharply on compositional tasks. Analysis reveals systematic failures in cross-functional reasoning, including fragile specifications, misalignment between implementations and proofs, and unstable reasoning. DafnyCOMP thus provides a diagnostic tool for measuring progress toward reliable, verifiable, and compositional code generation with LLMs.