用形式化验证提升对话式编程的可靠性，解决代码矛盾与技术债问题。
Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification
- 构建旁路系统自动形式化规范并验证代码一致性
- 通过可操作反馈减少代码返工与安全漏洞
- 适合关注代码质量与开发效率的工程师
对话式编程（vibe coding）——即通过与大语言模型反复交互来开发软件——在过去一年中迅速流行。然而开发者普遍反映存在技术债累积、安全隐患及频繁修改代码等问题。我们指出，根源在于大模型无法协调对话过程中不断积累的人类约束，且因优先响应用户指令而忽视代码一致性。鉴于大模型对形式化反馈具有高度敏感性，我们主张引入形式化方法以提升可靠性。但现有结合形式化与大模型的方法仍显不足。为此，我们提出在对话式编程全程部署一个旁路系统，实现：（1）自动将需求形式化为规范；（2）与目标进行一致性验证；（3）向大模型输出可执行反馈；（4）支持开发者直观调整规范，从而实现更稳健的协作开发。
原文摘要 · Abstract (English)
``Vibe coding'' -- the practice of developing software through iteratively conversing with a large language model (LLM) -- has exploded in popularity within the last year. However, developers report key limitations including the accumulation of technical debt, security issues, and code churn to achieve satisfactory results. We argue that these pitfalls result from LLMs' inability to reconcile accumulating human-imposed constraints during vibe coding, with developers inadvertently failing to resolve contradictions because LLMs prioritize user commands over code consistency. Given LLMs' receptiveness to verification-based feedback, we argue that formal methods can mitigate these pitfalls, making vibe coding more reliable. However, we posit that integrating formal methods must transcend existing approaches that combine formal methods and LLMs. We advocate for a side-car system throughout the vibe coding process which: (1) \emph{Autoformalizes} specifications (2) Validates against targets, (3) Delivers \emph{actionable} feedback to the LLM, and (4) Allows intuitive developer influence on specifications.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。