paperbot · PL 论文追踪

全部论文 待读 收藏

P0 SpecPylot: Python Specification Generation with Large Language Models

SpecPylot：基于大语言模型的 Python 规约生成
FSE Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering2026匹配度 8/10 · 论文属于“AI→PL”方向，用 LLM 生成 Python 规约（icontract）并借助 CrossHair 符号执行验证与反例迭代修正，直接契合用户关注的“利用 LLM/Agent 改进静态分析/形式化验证”这一核心问题，且涉及程序验证与符号执行的交叉。引用 1 inbox
Ragib Shahariar Ayon, Shibbir Ahmed
程序验证机器学习与程序语言
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：提出 SpecPylot，用 LLM 生成 icontract 规约，并借助 CrossHair 符号执行验证与反例驱动迭代修正。

手工编写形式规约成本高，而现有大语言模型生成的规约常因语法错误、约束过严或与程序行为不匹配而无法通过验证。SpecPylot 面向 Python 程序合成可执行的 icontract 注解：由 LLM 提议候选契约，再用 CrossHair 的符号执行进行验证；当发现具体反例时，只更新生成的契约，不修改原程序。该工具还能生成覆盖率驱动的 pytest 桩，并保留详细的执行工件以辅助调试。评估表明，SpecPylot 能为多数程序生成 CrossHair 兼容的契约，同时也揭示了有界符号探索和 LLM 行为差异带来的实际限制。

问题
如何降低形式规约编写成本，并解决 LLM 生成规约常因语法错误、约束过严或行为不匹配而无法通过验证的问题。
方法
SpecPylot 让 LLM 提出 icontract 候选契约，用 CrossHair 符号执行检查，并基于具体反例仅迭代更新契约；同时生成 pytest 桩和执行工件。
评估
在 Python 程序上评估其生成 CrossHair 兼容契约的能力，结果显示多数程序可生成，但也暴露有界符号执行与 LLM 行为差异的限制。
原文摘要（Abstract）

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.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{abs-2604-16560,
  title = {SpecPylot: Python Specification Generation with Large Language Models},
  author = {Ragib Shahariar Ayon and Shibbir Ahmed},
  booktitle = {FSE},
  year = {2026},
  doi = {10.1145/3803437.3806427}
}