用形式化方法让AI编程既聪明又可靠
AI for software engineering: from probable to provable
- 融合AI创造力与形式化规范，提升代码正确性
- 借助现代证明工具实现程序可验证，降低幻觉风险
- 适合关注AI辅助开发可信性的工程师与研究者
AI编程（vibe coding）虽受瞩目，却面临两大挑战：目标难以准确描述（提示工程本质是需求工程，软件工程中最难的环节之一）；以及模型幻觉问题。程序只有在正确或接近正确时才有价值。解决方案是结合人工智能的创造性、形式化规范方法的严谨性，以及现代证明工具支持下的程序形式化验证，从而实现从可能到可证明的可靠编程。
原文摘要 · Abstract (English)
Vibe coding, the much-touted use of AI techniques for programming, faces two overwhelming obstacles: the difficulty of specifying goals ("prompt engineering" is a form of requirements engineering, one of the toughest disciplines of software engineering); and the hallucination phenomenon. Programs are only useful if they are correct or very close to correct. The solution? Combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification, supported by modern proof tools.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。