Panel：Agent 软件工程的理论基础与工程实践

音频围绕面向 agent 的软件以及形式化验证展开，邀请了复旦大学彭鑫老师、南京大学彭鑫老师、上海交大林云老师等多位专家进行讨论，探讨了形式化验证、软件智能体、编程语言、操作系统、具身智能和软件工厂等多个领域在 AI 时代的发展和面临的问题，内容如下：

• 形式化验证在 AI agent 时代的角色与限制
• 形式化方法进入主流的机会：董金松老师认为，形式化方法此前未进入软件工程主流，因其对编写形式化规范和进行形式化验证要求较高。但现在 AI 可生成形式化规范，许多证明过程也能自动化，这为推动形式化方法进入软件工程主流带来机会。
• 面临的挑战：传统挑战依然存在，如形式化规范可能与用户真实意图或需求不符。例如在 format agent 工作中，需求变化时规范也需相应改变，需用 agent 自动化应对复杂性。
• 软件智能体解决软件复杂性问题的能力
• 两个正交维度：彭鑫老师提出，软件智能体在解决软件复杂性问题上有一定价值，它能解决人的原能力问题，如工具使用、问题根源查找、记忆管理等，这些能力与特定系统无关。但它无法解决特定项目的复杂系统知识问题，如系统的独特性、历史决策结果、奇怪的相互作用等。
• 系统复杂性的度量与应对：系统复杂性可通过可驾驭性来度量。在系统复杂性间隙中存在机会，如技术支撑的小程序、高保真原型、扁平化软件以及专家拆分复杂系统等情况，AI 可发挥作用。
• 可加益性的方面：可加益性包括问题能讲清且结果明确、能为 agent 提供环境操控能力、充分解耦等方面。微服务架构是解耦的良好方式，它将架构显示化，解决了传统软件架构不清晰的问题。
• 智能体时代编程语言的变化
• 新形态带来的机会：冯新宇老师表示，编程语言一直在演进，但外界看来变革性进展不大。符号和神经融合的新形态为编程语言带来机会，计算模型和编程范式可能会有所变化。
• 传统语言的演进方向：传统语言若更多给大模型使用，隐式类型推断等让程序更简洁、易理解的因素可能降低，而可靠性会更受重视，会增加更多规则指导程序优化，Rust 是这方面的代表。
• 智能体的操作系统与传统操作系统的区别及可靠性保证
• 与传统操作系统的关系：陈宇老师认为，面向 agent 的操作系统是在已有操作系统基础上的增量，需应对 agent 带来的不确定性、潜在风险和性能等问题。
• 可靠性保证的挑战：保证操作系统安全可靠面临挑战，当前大模型生成代码能力增强，但开发者能力未跟上，需新方法解决问题。
• 自动编程和软件工程能力在具身智能赛道的作用
• 模型不是最大瓶颈：王彦志老师指出，在具身智能赛道，模型能力已有所提升，不是最大瓶颈，软硬件配合问题更为严重，如找不到最佳软件和硬件，存在各种不匹配情况。
• 自动编程的重要性：自动编程在具身智能中不可或缺，没有它很多项目无法开展。未来 3 - 5 年，模型和数据能力有望完善，但软硬件配合问题在产业链层面仍难以解决。
• 面临的挑战：具身智能还面临机器人设计和操作带来的危险、AI coding 易导致 hack 等安全和软件工程挑战。
• AI 时代软件工厂的新意义
• 从弱到强的转变：林云老师认为，软件工厂从弱走向强，原因是大模型实现了知识自动化，需要用技能引导出正确答案，在知识空间中进行采样。
• 未来发展模式：未来软件工程希望实现流水线化生产，人从操作转为监控和干预，在箱子掉落等情况时进行处理，更好地进行管理、驾驭和监控。
• 后续工作计划
• 模型研究与部署：王彦志老师团队将继续研究大 Coding 模型，如 GLM 的 5.2 等，进行端侧平台或端云结合平台的部署，以及 trainC2Rust 的 27B 级别的模型研究，希望开源后为 agent 软件工程提供助力。
• 场景合作与问题解决：彭鑫老师实验室将继续与智源合作相关场景，运用工程化、系统化方法解决 AI 应用中的问题，如机器人相互配合、异常处理等。