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