Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
作者: Shuvendu K. Lahiri
分类: cs.PL, cs.LG, cs.SE
发布日期: 2024-06-14 (更新: 2024-10-15)
备注: Proceedings of the 24th Conference on Formal Methods in Computer Aided Design (FMCAD 2024)
期刊: Proceedings of the 24th Conference on Formal Methods in Computer Aided Design (FMCAD 2024)
DOI: 10.34727/2024/isbn.978-3-85448-065-5_19
💡 一句话要点
提出一种基于符号测试的规约质量评估方法，用于验证感知语言的用户意图形式化。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化方法 验证感知语言 用户意图形式化 符号测试 规范质量评估
📋 核心要点
- 现有方法难以评估验证感知语言中用户意图的形式化，因为其规范包含量词和ghost变量，无法通过动态执行评估。
- 论文提出通过符号测试规范来评估规范质量，无需生成程序突变体，提供了一种更简单直观的评估指标。
- 实验表明，该自动化指标与人工标注的Dafny规范数据集高度吻合，并能发现人工标注的不足之处。
📝 摘要（中文）
验证感知编程语言（如Dafny和F*）提供了形式化地指定和证明程序属性的方法。虽然检查实现是否符合规范的问题可以通过机械方式定义，但没有算法方法可以确保程序的用户意图形式化的正确性，即用形式规范表达的意图。这是因为意图或需求是用自然语言非正式地表达的，而规范是一种形式化的产物。尽管如此，大型语言模型（LLM）的出现在弥合非正式意图和形式程序实现之间的差距方面取得了巨大进展，这在很大程度上得益于评估的基准和自动化指标。最近的工作提出了一个评估主流编程语言的用户意图形式化问题的框架。然而，这种方法不容易扩展到支持丰富规范（使用量词和ghost变量）的验证感知语言，这些规范无法通过动态执行进行评估。之前的工作还需要使用LLM生成程序突变体来创建基准。我们提倡一种替代的、可能更简单的方法，即符号测试规范，以提供一个直观的指标来评估验证感知语言的规范质量。我们证明了我们的自动化指标与人工标注的Dafny规范数据集（针对流行的MBPP代码生成基准）非常吻合，但也展示了人工标注并不完美的情况。我们还概述了需要解决的形式验证挑战，以便更广泛地应用该技术。我们相信我们的工作为建立用户意图形式化问题的基准和研究议程提供了一个垫脚石。
🔬 方法详解
问题定义：论文旨在解决验证感知语言中用户意图形式化规范的质量评估问题。现有方法，特别是针对主流编程语言的方法，无法直接应用于验证感知语言，因为这些语言的规范包含复杂的量词和ghost变量，难以通过动态执行进行评估。此外，以往工作依赖于使用LLM生成程序突变体来构建评估基准，这增加了复杂性。
核心思路：论文的核心思路是利用符号测试来评估规范的质量。符号测试通过使用符号值代替具体值来执行程序，从而可以探索程序的不同执行路径。通过符号测试规范，可以检查规范在不同输入条件下的行为，从而评估其是否准确地反映了用户意图。
技术框架：该方法主要包含以下几个阶段：1) 获取验证感知语言（如Dafny）的规范；2) 使用符号执行引擎对规范进行符号测试，生成符号执行路径和约束条件；3) 分析符号执行路径和约束条件，判断规范是否满足预期的行为；4) 基于分析结果，生成评估指标，用于衡量规范的质量。
关键创新：该方法的主要创新在于将符号测试应用于验证感知语言的规范质量评估。与以往依赖动态执行或程序突变的方法相比，符号测试能够更全面地探索规范的行为，并提供更准确的评估结果。此外，该方法无需生成程序突变体，降低了评估的复杂性。
关键设计：论文中没有明确提及具体的参数设置、损失函数或网络结构等技术细节。关键在于如何有效地利用符号执行引擎来生成符号执行路径和约束条件，以及如何设计合理的评估指标来衡量规范的质量。例如，可以根据符号执行路径的覆盖率、约束条件的可满足性等指标来评估规范的完整性和一致性。
📊 实验亮点
实验结果表明，该方法提出的自动化指标与人工标注的Dafny规范数据集高度吻合，验证了该方法的有效性。更重要的是，该方法能够发现人工标注的不足之处，表明其具有超越人工评估的能力。该研究为建立用户意图形式化问题的基准和研究议程奠定了基础。
🎯 应用场景
该研究成果可应用于验证感知软件的开发过程中，帮助开发者评估和改进规范的质量，从而提高软件的可靠性和安全性。此外，该方法还可以用于自动化测试和验证工具的开发，为软件质量保证提供更有效的手段。未来，该技术有望推广到更广泛的形式化方法应用领域。
📄 摘要（原文）
Verification-aware programming languages such as Dafny and F* provide means to formally specify and prove properties of a program. Although the problem of checking an implementation against a specification can be defined mechanically, there is no algorithmic way of ensuring the correctness of the {\it user-intent formalization for programs}, expressed as a formal specification. This is because intent or requirement is expressed {\it informally} in natural language and the specification is a formal artefact. Despite, the advent of large language models (LLMs) has made tremendous strides bridging the gap between informal intent and formal program implementations recently, driven in large parts by benchmarks and automated metrics for evaluation. Recent work has proposed a framework for evaluating the {\it user-intent formalization} problem for mainstream programming languages~\cite{endres-fse24}. However, such an approach does not readily extend to verification-aware languages that support rich specifications (using quantifiers and ghost variables) that cannot be evaluated through dynamic execution. Previous work also required generating program mutants using LLMs to create the benchmark. We advocate an alternate, perhaps simpler approach of {\it symbolically testing specifications} to provide an intuitive metric for evaluating the quality of specifications for verification-aware languages. We demonstrate that our automated metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark, yet demonstrates cases where the human labeling is not perfect. We also outline formal verification challenges that need to be addressed to apply the technique more widely. We believe our work provides a stepping stone to enable the establishment of a benchmark and research agenda for the problem of user-intent formalization for programs.