Le succès local ne se compose pas : évaluation des modèles de langage à grande échelle pour la vérification formelle compositionnelle

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

September 27, 2025

papers.authors: Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

cs.AI

papers.abstract

Nous présentons DafnyCOMP, un benchmark pour évaluer les modèles de langage de grande taille (LLMs) sur la génération de spécifications compositionnelles en Dafny. Contrairement aux benchmarks antérieurs qui se concentrent sur des tâches à fonction unique, DafnyCOMP cible des programmes composés de plusieurs fonctions interactives avec des dépendances de données, nécessitant un raisonnement à travers les limites des composants. Le benchmark comprend 300 programmes multifonctionnels synthétisés automatiquement. Nous évaluons plusieurs familles de LLM de pointe et constatons que, bien qu'ils performent bien sur la vérification de fonctions uniques, leur performance chute considérablement sur les tâches compositionnelles. L'analyse révèle des échecs systématiques dans le raisonnement inter-fonctionnel, incluant des spécifications fragiles, un désalignement entre les implémentations et les preuves, ainsi qu'un raisonnement instable. DafnyCOMP offre ainsi un outil diagnostique pour mesurer les progrès vers une génération de code fiable, vérifiable et compositionnelle avec les 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.