测试大模型在复杂函数组合验证中的表现，发现其推理能力严重不足。
Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
- 构建300个有数据依赖的多函数程序，评估大模型跨函数推理能力
- 单函数任务表现良好，组合任务性能骤降超过50%
- 揭示模型在规范对齐与推理稳定性上的系统性缺陷
我们提出了DafnyCOMP，一个用于评估大语言模型（LLMs）在Dafny中生成组合式规格的基准。与以往聚焦单函数任务的基准不同，DafnyCOMP针对由多个相互作用函数构成、存在数据依赖的程序，要求跨组件边界进行推理。该基准包含300个自动生成的多函数程序。我们评估了多个前沿的LLM系列，发现尽管它们在单函数验证任务上表现良好，但在组合任务上的性能显著下降。分析表明，存在系统性的跨函数推理失败，包括脆弱的规格、实现与证明之间的不一致，以及不稳定的推理过程。DafnyCOMP因此提供了一个诊断工具，用于衡量大模型在生成可验证、可组合代码方面的进展。
原文摘要 · Abstract (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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。