局部成功无法组合：面向组合式形式化验证的大型语言模型基准测试
Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
- Shanghai AI Lab（上海人工智能实验室）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
提出含300个多功能程序的 DafnyCOMP 基准，评估 LLM 的 Dafny 组合式规约生成能力，揭示其跨函数推理存在系统性失败。
AI中文摘要：
我们提出 DafnyCOMP，这是一个用于评估大型语言模型（LLM）在 Dafny 中进行组合式规约生成的基准。不同于以往关注单函数任务的基准，DafnyCOMP 针对由多个相互交互且存在数据依赖的函数组成的程序，要求跨组件边界进行推理。该基准包含 300 个自动合成的多功能程序。我们评估了若干最先进的 LLM 系列，发现尽管它们在单函数验证上表现良好，但在组合式任务上性能急剧下降。分析揭示了跨函数推理中的系统性失败，包括脆弱的规约、实现与证明之间的不一致，以及不稳定的推理。因此，DafnyCOMP 提供了一种诊断工具，用于衡量利用 LLM 实现可靠、可验证且可组合的代码生成的进展。
英文摘要：
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.
