来源笔记
From Helpful to Trustworthy: LLM Agents for Pair Programming
摘要
本文提出一种面向 LLM 的多智能体结对编程流程，目标是把意图转成明确的规格，并用确定性工具检查输出，从而提高代码生成的可信度。这是一份博士研究计划，作者先前的规格生成系统提供了早期结果支持。
问题
- 基于 LLM 的编码智能体可以生成看起来合理的代码、测试和文档，但这些内容可能不符合开发者意图。
- 自由形式的智能体评审难以审计，所以在真实项目里，开发者仍然需要仔细检查输出。
- 软件会在重构、 API 迁移和文档更新中不断变化，而现有智能体流程很难提供足够证据证明行为仍然正确。
方法
- 使用驱动智能体提出工件，使用导航智能体在结对编程循环中进行评审，二者分工不同，并共享项目上下文。
- 约束导航智能体输出可机器检查的契约和形式化规格，而不是开放式判断。
- 用确定性验证器和 SMT 支持的反例来验证这些规格以及后续的代码和测试修改，让评审依赖外部证据，而不是一个模型评判另一个模型。
- 研究三个阶段：把非正式问题陈述转成符合标准的需求和形式化规格，用自动反馈改进测试和实现，以及在保留已验证行为的前提下处理维护任务。
- 通过具体信号衡量可信度，例如通过率、无法判定的结果、失败的可复现性，以及维护过程中的回归预防。
结果
- 这篇论文本身是一份研究提案，还没有报告完整结对编程流程的端到端结果。
- 文中引用了 AutoReSpec 在 72 个程序基准上的初步结果：67 个程序通过验证、58.2% 成功概率、69.2% 完整性，以及比先前方法低 26.89% 的平均评估时间。
- 文中引用了 AutoJML 在 120 个程序基准上的初步结果：109 个程序通过验证，平均完整性为 79.3%。
- AutoJML 在更难的控制流场景上也给出了较好结果：多路径循环的完整性为 81.48%，嵌套循环为 85.71%，与当前最优基线相比更高，但摘录中没有给出基线的具体数值。
- 作者主张的进展是一个以证据为基础的结对编程设置，其中需求、规格、测试和求解器反馈都可以作为可审计的代码生成和维护工件。