Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912611400941568 |
|---|---|
| author | Xu, Xu Li, Xin Qu, Xingwei Fu, Jie Yuan, Binhang |
| author_facet | Xu, Xu Li, Xin Qu, Xingwei Fu, Jie Yuan, Binhang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_23061 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification Xu, Xu Li, Xin Qu, Xingwei Fu, Jie Yuan, Binhang Programming Languages Artificial Intelligence 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. |
| title | Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification |
| topic | Programming Languages Artificial Intelligence |
| url | https://arxiv.org/abs/2509.23061 |