用大模型自动把自然语言断言转成可执行代码，准确率提升20点。
Faithful Autoformalization of Natural Language Assertions
- 通过一致性评分和测试验证筛选形式化结果，减少歧义。
- 在541个任务上平均精度提升20点，接近真实断言。
- 适合需要高可靠断言的软件测试与验证场景。
形式化合同对软件测试与验证至关重要，但编写过程耗时且易出错。大语言模型为自动化形式化提供了可能：从自然语言规范中生成可执行断言，弥合开发人员意图与形式化可执行规范之间的差距。我们提出 Monty：一种针对断言的自动化形式化框架，解决了断言有效性预期与自然语言模糊性挑战。其技术基于新颖的一致性评分指标及通过代码测试形式化断言获得的有效性评分进行筛选。我们在22个集合类Java类中提取的541个断言生成任务上评估该方法，结果表明，相比直接使用LLM翻译，本方法能更可靠地生成真实断言（平均精度提升最高达20点）。
原文摘要 · Abstract (English)
Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。