Il Successo Locale Non Si Compone: Benchmarking dei Modelli Linguistici di Grandi Dimensioni per la Verifica Formale Composizionale

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

September 27, 2025

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

cs.AI

Abstract

Presentiamo DafnyCOMP, un benchmark per valutare i modelli linguistici di grandi dimensioni (LLM) nella generazione di specifiche composizionali in Dafny. A differenza dei benchmark precedenti che si concentrano su compiti a singola funzione, DafnyCOMP si rivolge a programmi composti da più funzioni interagenti con dipendenze dati, richiedendo un ragionamento che attraversi i confini dei componenti. Il benchmark è costituito da 300 programmi multi-funzione sintetizzati automaticamente. Valutiamo diverse famiglie di LLM all'avanguardia e riscontriamo che, sebbene performino bene nella verifica a singola funzione, le loro prestazioni calano drasticamente nei compiti composizionali. L'analisi rivela fallimenti sistematici nel ragionamento cross-funzionale, tra cui specifiche fragili, disallineamenti tra implementazioni e dimostrazioni, e ragionamenti instabili. DafnyCOMP fornisce quindi uno strumento diagnostico per misurare i progressi verso una generazione di codice affidabile, verificabile e composizionale con gli LLM.

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.