paperbot · PL 论文追踪

全部论文 待读 收藏

Trust the Delta: Rethinking Software Validation in the AI Era (Keynote)

信任 Delta:重思 AI 时代的软件验证(主旨报告)
ASE Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering2026引用 0 inbox
Michael Pradel
crossref: 2026-10-09

AI 速览

一句话:提出以行为差异(delta)为中心的变更验证范式,将验证目标从绝对正确性转为确认变更符合意图。

生成式 AI 让软件变更的生产成本急剧下降,开发瓶颈从实现转向验证。该主旨报告指出,软件变更是一类特别可处理的正确性验证场景:变更已有被广泛接受的既有实现,且常伴随自然语言描述的目标意图,二者共同构成一种强大的部分规约——默认应保留既有行为,仅在明确意图允许处发生差异。由此,oracle 问题被重构为验证行为 delta:哪些行为改变、哪些保持稳定、观测差异是否与预期变更一致。通过结合自然语言意图与跨程序版本的执行,AI 技术可为变更正确性构建越来越强的证据。报告认为,随着编码智能体能力增强,AI4SE 的核心挑战将从生成补丁转向为补丁提供正当性;未来系统不仅应产出代码变更,还应产出可执行证据,证明预期变更且仅有预期变更确实发生。

问题
生成式 AI 使代码变更极易生成,验证成为新瓶颈;传统 oracle 问题要求判定程序绝对正确,对快速迭代的软件变更而言过于困难且不必要。
方法
将变更视为具有部分规约的验证对象:以既有行为默认保留、自然语言意图界定允许差异,结合跨版本执行与 AI 技术来分析和验证行为 delta。
评估
该文为主旨报告,主要给出概念框架与论证,未报告具体实验评估;提出未来系统应生成可执行证据以证明变更符合意图。
原文摘要(Abstract)

Generative AI is making software changes increasingly cheap to produce, shifting the bottleneck from implementation to validation. This keynote argues that software changes offer a uniquely tractable setting for establishing correctness. Unlike an arbitrary program, a change comes with an existing implementation whose behavior is largely accepted and, often, a natural-language description of what is intended to change. Together, these provide a powerful partial specification in which existing behavior should be preserved by default, except where the stated intent justifies a difference. This reframes the oracle problem from determining absolute correctness to validating a behavioral delta by asking which behaviors changed, which remained stable, and whether the observed differences match the intended change. By combining natural-language intent with execution across program versions, AI-based techniques can construct increasingly strong evidence about the correctness of a change. As coding agents become more capable, the central challenge for AI4SE therefore shifts from generating patches to justifying them. Future systems should produce not only code changes, but executable evidence that the intended change, and only the intended change, actually occurred.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot12234,
  title = {Trust the Delta: Rethinking Software Validation in the AI Era (Keynote)},
  author = {Michael Pradel},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3857283}
}