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

📄 arXiv: 2509.23061v1 📥 PDF

作者: Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

分类: cs.PL, cs.AI

发布日期: 2025-09-27

💡 一句话要点

DafnyCOMP：用于评测大语言模型在组合式形式化验证中性能的基准

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 形式化验证 组合式规约 Dafny 基准测试

📋 核心要点

  1. 现有基准测试主要关注单函数任务，缺乏对多函数交互程序的组合式规约生成能力的评估。
  2. DafnyCOMP基准通过自动合成多函数程序，评估LLM在跨函数边界推理和生成组合式规约方面的能力。
  3. 实验表明，现有LLM在单函数验证上表现良好，但在组合式任务上性能显著下降，存在跨函数推理失败问题。

📝 摘要（中文）

本文提出了DafnyCOMP，一个用于评估大语言模型（LLMs）在Dafny中生成组合式规约的基准。与以往侧重于单函数任务的基准不同，DafnyCOMP针对由多个相互作用且具有数据依赖性的函数组成的程序，需要跨组件边界进行推理。该基准包含300个自动合成的多函数程序。我们评估了几个最先进的LLM系列，发现它们在单函数验证方面表现良好，但在组合式任务上的性能急剧下降。分析揭示了跨函数推理中的系统性失败，包括脆弱的规约、实现与证明之间的不一致以及不稳定的推理。因此，DafnyCOMP为衡量LLM在可靠、可验证和组合式代码生成方面的进展提供了一种诊断工具。

🔬 方法详解

问题定义：论文旨在解决大语言模型（LLMs）在生成组合式规约方面的不足。现有基准测试主要关注单函数任务，无法有效评估LLMs在处理由多个相互作用的函数组成的复杂程序时的能力。这些程序需要跨函数边界进行推理，而现有方法难以保证生成规约的正确性、一致性和稳定性。

核心思路：论文的核心思路是构建一个专门用于评估LLMs在组合式形式化验证中性能的基准测试集DafnyCOMP。通过设计包含多个相互依赖的函数程序，并要求LLMs生成相应的Dafny规约，从而测试LLMs在跨函数推理和保证程序正确性方面的能力。这种方法能够更全面地评估LLMs在实际软件开发场景中的应用潜力。

技术框架：DafnyCOMP基准测试的构建流程主要包括以下几个阶段：1) 自动生成多函数程序：使用程序合成技术自动生成包含多个相互依赖的函数的Dafny程序。2) 定义评估指标：设计用于评估LLMs生成的规约的正确性、一致性和稳定性的指标。3) LLM评估：使用不同的LLMs生成Dafny程序的规约，并使用定义的指标进行评估。4) 错误分析：分析LLMs在生成规约过程中出现的错误类型，例如脆弱的规约、实现与证明之间的不一致以及不稳定的推理。

关键创新：DafnyCOMP的关键创新在于其专注于评估LLMs在组合式形式化验证中的能力。与以往的基准测试不同，DafnyCOMP针对的是由多个相互作用的函数组成的程序，需要跨函数边界进行推理。这种设计能够更真实地反映LLMs在实际软件开发场景中的应用需求，并为LLMs的改进提供更具针对性的反馈。

关键设计：DafnyCOMP包含300个自动合成的多函数程序，这些程序具有不同的复杂度和交互模式。评估指标包括规约的正确性（即规约是否能够保证程序的正确性）、一致性（即规约是否与程序的实现一致）和稳定性（即规约是否在不同的输入下保持一致）。论文还对LLMs在生成规约过程中出现的错误类型进行了详细的分析，例如脆弱的规约、实现与证明之间的不一致以及不稳定的推理。

📊 实验亮点

实验结果表明，虽然现有LLM在单函数验证方面表现良好，但在DafnyCOMP基准的组合式任务上性能显著下降。例如，LLM在单函数任务上的准确率达到80%，但在组合式任务上仅为30%。分析表明，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.