Sucesso Local Não Compõe: Avaliando Modelos de Linguagem de Grande Escala para Verificação 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

Resumo

Apresentamos o DafnyCOMP, um benchmark para avaliar modelos de linguagem de grande escala (LLMs) na geração de especificações composicionais em Dafny. Diferente de benchmarks anteriores que se concentram em tarefas de função única, o DafnyCOMP visa programas compostos por múltiplas funções interativas com dependências de dados, exigindo raciocínio além dos limites dos componentes. O benchmark consiste em 300 programas multifuncionais sintetizados automaticamente. Avaliamos várias famílias de LLMs de ponta e constatamos que, embora tenham um bom desempenho na verificação de função única, seu desempenho cai drasticamente em tarefas composicionais. A análise revela falhas sistemáticas no raciocínio cross-funcional, incluindo especificações frágeis, desalinhamento entre implementações e provas, e raciocínio instável. O DafnyCOMP, portanto, fornece uma ferramenta diagnóstica para medir o progresso em direção à geração de código confiável, verificável e composicional com 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.