意图形式化：面向 AI 代理时代可靠编程的大挑战

Agentic AI 系统已能够以惊人的流畅度生成代码，但仍有一个根本问题：生成的代码是否真正实现了用户的意图？在非正式自然语言需求与精确程序行为之间的差距——即“意图差距”——一直是软件工程中的痛点，但 AI 生成的代码将其放大到了前所未有的规模。本文认为，意图形式化——即将非正式的用户意图翻译为可检查的形式规范的过程——是决定 AI 是否使软件更可靠而非仅更丰富的关键挑战。意图形式化提供了适用于不同可靠性需求的权衡谱系：从轻量级测试以消除可能的误解，到完整的功能规范用于形式化验证，再到特定领域的语言从而自动合成正确代码。核心瓶颈是“验证规范的正确性”：由于没有其他关于规范正确性的神谕，除了用户之外，我们需要半自动化的度量标准，可在有或没有代码的情况下，通过轻量级用户交互和代理构件（如测试）来评估规范的质量。我们调查了早期研究，展示了该方法的潜力：交互式测试驱动的形式化可提高程序正确性、AI 生成的后置条件捕获了先前方法遗漏的真实世界错误，以及从非正式规范生成可形式化证明正确代码的端到端管道。我们概述了开放的研究挑战——超越基准的规模化、对变更的组合性、用于验证规范的度量标准、处理复杂逻辑、设计人机规范交互——这些挑战定义了一个跨越 AI、编程语言、形式方法和人机交互的研究议程。