When software artifacts are generated by AI models ("vibe coding"), human engineers assume responsibility for validating them. Ideally, this validation would be done through the creation of a formal proof of correctness. However, this is infeasible for many real-world vibe coding scenarios, especially when requirements for the AI-generated artifacts resist formalization. This extended abstract describes ongoing work towards the extraction of analyzable, semi-formal rationales for the adequacy of vibe-coded artifacts. Rather than deciding correctness directly, our framework produces a set of conditions under which the generated code can be considered adequate. We describe current efforts towards implementing our framework and anticipated research opportunities.

翻译：当软件制品由AI模型生成（"氛围编码"）时，人类工程师需承担验证责任。理想情况下，这种验证应通过构建形式化的正确性证明来完成。然而，对于许多现实世界的氛围编码场景而言，这并不可行，特别是当AI生成制品的需求难以形式化时。本扩展摘要阐述了当前正在开展的研究工作：旨在为氛围编码制品的充分性提取可分析的半形式化理论依据。我们的框架并非直接判定正确性，而是生成一组条件，在这些条件下所生成的代码可被视为充分。我们描述了当前实现该框架的工作进展以及预期的研究机遇。