---
source: arxiv
url: http://arxiv.org/abs/2604.10300v1
published_at: '2026-04-11T17:39:57'
authors:
- Ragib Shahariar Ayon
topics:
- llm-agents
- pair-programming
- formal-specification
- software-verification
- code-intelligence
relevance_score: 0.95
run_id: materialize-outputs
language_code: zh-CN
---

# From Helpful to Trustworthy: LLM Agents for Pair Programming

## Summary
## 摘要
本文提出一种面向 LLM 的多智能体结对编程流程，目标是把意图转成明确的规格，并用确定性工具检查输出，从而提高代码生成的可信度。这是一份博士研究计划，作者先前的规格生成系统提供了早期结果支持。

## 问题
- 基于 LLM 的编码智能体可以生成看起来合理的代码、测试和文档，但这些内容可能不符合开发者意图。
- 自由形式的智能体评审难以审计，所以在真实项目里，开发者仍然需要仔细检查输出。
- 软件会在重构、 API 迁移和文档更新中不断变化，而现有智能体流程很难提供足够证据证明行为仍然正确。

## 方法
- 使用驱动智能体提出工件，使用导航智能体在结对编程循环中进行评审，二者分工不同，并共享项目上下文。
- 约束导航智能体输出可机器检查的契约和形式化规格，而不是开放式判断。
- 用确定性验证器和 SMT 支持的反例来验证这些规格以及后续的代码和测试修改，让评审依赖外部证据，而不是一个模型评判另一个模型。
- 研究三个阶段：把非正式问题陈述转成符合标准的需求和形式化规格，用自动反馈改进测试和实现，以及在保留已验证行为的前提下处理维护任务。
- 通过具体信号衡量可信度，例如通过率、无法判定的结果、失败的可复现性，以及维护过程中的回归预防。

## 结果
- 这篇论文本身是一份研究提案，还没有报告完整结对编程流程的端到端结果。
- 文中引用了 **AutoReSpec** 在 **72 个程序**基准上的初步结果：**67 个程序通过验证**、**58.2%** 成功概率、**69.2%** 完整性，以及比先前方法**低 26.89%** 的平均评估时间。
- 文中引用了 **AutoJML** 在 **120 个程序**基准上的初步结果：**109 个程序通过验证**，平均完整性为 **79.3%**。
- AutoJML 在更难的控制流场景上也给出了较好结果：**多路径循环**的完整性为 **81.48%**，**嵌套循环**为 **85.71%**，与当前最优基线相比更高，但摘录中没有给出基线的具体数值。
- 作者主张的进展是一个以证据为基础的结对编程设置，其中需求、规格、测试和求解器反馈都可以作为可审计的代码生成和维护工件。

## Problem

## Approach

## Results

## Link
- [http://arxiv.org/abs/2604.10300v1](http://arxiv.org/abs/2604.10300v1)