Lokaler Erfolg führt nicht zu Komposition: Benchmarking von großen Sprachmodellen für die kompositionelle formale Verifikation

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

Wir stellen DafnyCOMP vor, einen Benchmark zur Bewertung von großen Sprachmodellen (LLMs) hinsichtlich der generativen Komposition von Spezifikationen in Dafny. Im Gegensatz zu früheren Benchmarks, die sich auf Aufgaben mit einzelnen Funktionen konzentrieren, zielt DafnyCOMP auf Programme ab, die aus mehreren interagierenden Funktionen mit Datenabhängigkeiten bestehen und somit eine übergreifende Argumentation über Komponentengrenzen hinweg erfordern. Der Benchmark umfasst 300 automatisch synthetisierte Programme mit mehreren Funktionen. Wir evaluieren mehrere state-of-the-art LLM-Familien und stellen fest, dass diese zwar bei der Verifikation einzelner Funktionen gut abschneiden, ihre Leistung jedoch bei kompositionellen Aufgaben deutlich abfällt. Analysen zeigen systematische Schwächen in der funktionsübergreifenden Argumentation, darunter fragile Spezifikationen, Fehlausrichtungen zwischen Implementierungen und Beweisen sowie instabile Schlussfolgerungen. DafnyCOMP bietet somit ein diagnostisches Werkzeug, um Fortschritte in Richtung einer zuverlässigen, verifizierbaren und kompositionellen Codegenerierung mit LLMs zu messen.

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.