评估面向验证感知语言的LLM驱动用户意图形式化
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
AI总结：
针对验证感知语言规范无法动态执行的问题，提出符号化测试规范方法评估LLM驱动的用户意图形式化，在MBPP的Dafny数据集上与人工标注高度一致，为建立该领域基准奠定基础。
摘要：
诸如 Dafny 和 F* 等验证感知编程语言提供了形式化指定和证明程序属性的手段。尽管检查实现是否符合规范的问题可以通过机械方式定义，但并没有算法方法能确保作为形式化规范表达的程序的用户意图形式化的正确性。这是因为意图或需求是以自然语言非形式化表达的，而规范是形式化产物。尽管如此，随着大语言模型（LLMs）的发展，近期在弥合非形式化意图与形式化程序实现之间的差距方面取得了巨大进展，这在很大程度上得益于基准测试和自动化评估指标。最近的研究提出了一个评估主流编程语言用户意图形式化问题的框架。然而，这种方法不能直接扩展到支持丰富规范（使用量词和幽灵变量）的验证感知语言，这些规范无法通过动态执行来评估。之前的工作还需要使用 LLMs 生成程序变异体以创建基准。我们提倡一种替代的、或许更简单的符号化测试规范方法，为评估验证感知语言的规范质量提供直观指标。我们证明，在流行的 MBPP 代码生成基准的 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
