用AI降低形式化规范门槛，让非专家也能高效写出正确代码。
Enhancing Formal Software Specification with Artificial Intelligence
- 用自然语言+轻量数学符号做中间表示，AI辅助修正后生成代码。
- 在组织知识增长模拟中实现首次即正确，提前验证并明确不变式。
- 适合需要高可靠性但缺乏形式化经验的开发团队使用。
形式化软件规范虽能早期发现错误并明确不变式，但因符号开销大、需专业技能，工业界应用有限。本文通过案例研究证明，人工智能进展使保留形式化优势的同时大幅降低使用成本成为可能。文章强调区分哪些部分需系统分析师严格控制（受益于形式化严谨性），哪些无需。采用自然语言结合轻量数学符号，并以LaTeX书写作为中间规范语言，由AI在生成代码前进行评审与优化。应用于一个非平凡的组织知识增长仿真中，该方法实现了早期验证、显式不变式和设计即正确，显著减少开发工作量，并在首次尝试即产出正确实现。
原文摘要 · Abstract (English)
Formal software specification is known to enable early error detection and explicit invariants, yet it has seen limited industrial adoption due to its high notation overhead and the expertise required to use traditional formal languages. This paper presents a case study showing that recent advances in artificial intelligence make it possible to retain many of the benefits of formal specification while substantially reducing these costs. The necessity of a clear distinction between what is controlled by the system analyst and can highly benefits from the rigor of formal specification and what need not be controlled is demonstrated. We use natural language augmented with lightweight mathematical notation and written in \LaTeX\ as an intermediate specification language, which is reviewed and refined by AI prior to code generation. Applied to a nontrivial simulation of organizational knowledge growth, this approach enables early validation, explicit invariants, and correctness by design, while significantly reducing development effort and producing a correct implementation on the first attempt.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。