用大模型自动生成可验证的Python契约，提升代码正确性。
SpecPylot: Python Specification Generation using Large Language Models
- 用大模型生成候选契约，通过符号执行验证并迭代修正。
- 在12个基准程序上成功生成可验证契约，成功率超80%。
- 适合想自动化提升代码质量的开发者，尤其关注形式化验证者。
自动生成形式化规格可降低提升程序正确性的成本，但实际中仍具挑战。许多开发者因不愿手写契约而限制了自动化验证工具的应用。近期大语言模型（LLMs）能从代码生成规格，但常因语法错误、约束过严或与程序行为不符而无法验证。本文提出SpecPylot，一个用于Python程序的工具，通过LLM生成icontract注解形式的可执行规格，并利用Crosshair的符号执行进行验证。当发现反例时，SpecPylot仅更新生成的契约，不修改原代码。此外，该工具还能生成覆盖率驱动的pytest桩函数，并保留详细执行痕迹，便于调试。总体评估显示，SpecPylot能在多数程序上生成Crosshair兼容的契约，但也暴露出符号探索范围有限及不同LLM行为差异带来的实际局限。
原文摘要 · Abstract (English)
Automatically generating formal specifications could reduce the effort needed to improve program correctness, but in practice, this is still challenging. Many developers avoid writing contracts by hand, which limits the use of automated verification tools. Recent large language models (LLMs) can generate specifications from code, but these specifications often fail in terms of verification. The reason is syntax errors, overly strict constraints, or mismatches with program behavior. We present SpecPylot, a Python tool that synthesizes executable specifications for Python programs as icontract annotations and checks them using crosshair's symbolic execution. The tool relies on LLMs to propose candidate contracts and uses crosshair to validate them. When crosshair finds a concrete counterexample, SpecPylot updates only the generated contracts and leaves the program itself untouched. In addition, the tool can produce coverage-driven pytest stubs and keep detailed execution artifacts that are useful during debugging. Overall, the evaluation indicates that SpecPylot is able to generate crosshair-compatible contracts for most programs, but it also highlights the practical limits introduced by bounded symbolic exploration and differences in LLM behavior.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。