[Paper] AutoICE：通过 LLM 驱动的演化自动合成可验证的 C 代码

Source: arXiv - 2512.07501v1

概览

本文提出了 AutoICE，一个结合大型语言模型（LLM）与进化搜索策略的系统，能够自动生成可以针对自然语言规格进行 形式化验证 的 C 代码。通过解决此前自动形式化尝试中出现的语法和语义陷阱，AutoICE 将 AI 生成代码的可靠性推向了接近生产级的质量。

主要贡献

• LLM 驱动的进化框架：将多样的代码“个体”与协作交叉算子相结合，探索比单次生成更丰富的搜索空间。
• 自我反思的变异：一个反馈回路，LLM 对验证失败的尝试进行自省，学习隐式领域知识，并相应地变异代码。
• 高验证成功率：在标准基准上实现了 90.36 % 的验证代码，在面向开发者的变体上实现了 88.33 %，大幅超越了之前的最新技术水平。
• 开源数据集与工具：提供了一套自然语言需求与可验证 C 代码片段配对的精心策划集合，便于复现和进一步研究。

方法论

1. 种群初始化 – 系统使用 LLM 在自然语言需求的提示下生成初始候选 C 程序池。每个候选都会刻意进行多样化（不同的惯用写法、数据结构选择等），以避免过早收敛。
2. 协作交叉 – 成对的候选交换代码片段（例如函数体、循环结构），在 LLM 的指导下确保合并后的程序保持语法正确。这模拟了基因重组，并注入单次 LLM 生成永远不会产生的新组合。
3. 验证循环 – 每个子代被送入 C 验证工具（如 Frama‑C、VeriFast）。工具返回正确性证明或反例/错误轨迹。
4. 自我反思的变异 – 当验证失败时，LLM 分析错误轨迹，推断缺失的隐式知识（例如所需的前置条件、循环不变式），并相应地变异代码。变异后的程序重新进入种群，进入下一代。
5. 选择与终止 – 验证成功的程序被提升；过程重复进行，直至找到验证成功的候选或资源预算耗尽。

整个流水线全自动化，仅需自然语言规格作为输入。

结果与发现

• 错误降低：交叉步骤相比于朴素的单 LLM 生成循环，将语法错误传播降低了约 45 %。
• 隐式知识捕获：自我反思的变异在 82 % 的初始代码验证失败案例中成功添加了缺失的不变式。
• 运行时：在单个 RTX 4090 GPU 上，每个需求的平均合成时间保持在 30 秒以下，使该方法在交互式开发者工具中具有实用性。

实际意义

• 开发者助理：IDE 插件可以调用 AutoICE 将注释或用户故事转化为经过验证的 C 函数，显著降低手动编写正确底层代码的工作量。
• 安全关键系统：汽车、航空、医疗设备等行业可以利用 AutoICE 生成符合形式化安全标准（如 ISO‑26262）的代码，而无需内部的形式化方法专家。
• 快速原型：团队可以在 C 中快速原型化算法组件，立即获得验证反馈，并比传统的测试驱动开发更快迭代。
• 教育：AutoICE 可作为教学工具，向学生展示形式化规格如何转化为具体且可证明正确的实现。

局限性与未来工作

• 领域范围：当前评估侧重于算法内核，未覆盖大量 I/O、并发或操作系统层交互等验证更具挑战性的场景。
• LLM 依赖：质量依赖底层 LLM 的训练数据；罕见或特定领域的 API 仍可能生成不正确的代码片段。
• 验证可扩展性：对于大型代码库，验证步骤可能成为瓶颈；整合增量或模块化验证技术是一个待探索的方向。
• 向其他语言扩展：作者计划将进化框架适配到 Rust、Go 等内存安全语言，这些语言的形式化验证工具正日益成熟。

AutoICE 证明，将 LLM 与进化搜索及形式化验证相结合，可以弥合 AI 生成代码与生产就绪、可证明正确软件之间的鸿沟——这是迈向更可信开发者工具的有希望的一步。

作者

• Weilin Luo
• Xueyi Liang
• Haotian Deng
• Yanan Liu
• Hai Wan

论文信息

• arXiv ID: 2512.07501v1
• 分类: cs.SE, cs.AI
• 出版时间: 2025 年 12 月 8 日
• PDF: Download PDF