局所的な成功は合成されない：合成的形式検証のための大規模言語モデルのベンチマーキング

要旨

我々はDafnyCOMPを紹介する。これは、Dafnyにおける合成的仕様生成に対する大規模言語モデル（LLM）の評価を目的としたベンチマークである。従来のベンチマークが単一関数タスクに焦点を当てていたのに対し、DafnyCOMPはデータ依存関係を持つ複数の相互作用する関数で構成されるプログラムを対象としており、コンポーネント間を跨ぐ推論を必要とする。このベンチマークは、自動合成された300の多関数プログラムから構成されている。我々はいくつかの最先端LLMファミリーを評価し、それらが単一関数の検証では良好な性能を示す一方で、合成的タスクでは性能が急激に低下することを明らかにした。分析の結果、クロスファンクショナルな推論における体系的な失敗が明らかになり、脆弱な仕様、実装と証明の間の不一致、不安定な推論などが含まれることが分かった。したがって、DafnyCOMPは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.

局所的な成功は合成されない：合成的形式検証のための大規模言語モデルのベンチマーキング

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

要旨

Support