H1：LLMs 在软件工程社区引发的动荡及相关思考

• H2：竞争范式与模型观点

  • 出现了不同程度人类干预和控制的竞争范式，如无人类参与的代理、“vibe 编码”、独立模块或功能的聊天机器人、预测用户需求的编码助手等。
  • 对模型的极限、有用性和潜力存在多种观点，有人认为模型会达到人类水平能力，有人则持怀疑态度。

• H2：关于正确性的讨论

  • 软件必须在某种正确性概念上是“正确的”，LLMs 可分担代码编写阶段，但验证过程不能外包。
  • 在不同应用和领域，正确性的重要性和验证机制不同，从“尝试”到专业测试人员的测试等。

• H2：LLMs 生成代码的可验证性

  • 虽然 LLM 能生成代码，但未考虑代码的可验证性，如 UI 编程易验证，而 Web 服务器应用验证较难。
  • “vibe 编码游戏”的兴起也源于验证方式，可验证性是使用 LLM 编程的瓶颈。

• H2：应对措施

  • 放弃无限强大和可扩展的软件代理理念，需要更好的验证工具和接口，如将生成的测试总结为可读格式，依赖声明式随机测试方法。
  • 增加关于正确性的词汇，全面理解和测量程序的各种质量。

• H2：预测

  • 起初认为 LLM 不是好的程序员，但其在竞赛编程中的成功改变了看法，现在认为 LLM 在有完美预言机的所有领域都能成功。
  • 完美预言机在现实中几乎不存在，即使是定理证明者也不是完美的，但希望 LLM 在自动化证明方面更出色，未来工作可能是创建新定理等。