用大模型进化生成可验证的C代码，错误少、成功率高。
AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
- 通过多个体初始化与协作交叉，避免单点迭代误差传播。
- 自省式变异机制挖掘隐含知识，提升代码正确率至90.36%。
- 适合需要高可靠性代码的开发者和形式化方法初学者。
从自然语言需求自动合成可验证代码，能保障软件正确性并降低形式化方法使用门槛。随着大语言模型（LLMs）的发展，自动化形式化工作迎来新突破。然而现有方法因领域预训练语料稀缺，常出现严重语法与语义错误，且难以有效形式化隐含知识。本文提出AutoICE，一种基于大模型进化的可验证C代码合成方法。它引入多样个体初始化与协同交叉机制，实现多样化迭代更新，有效缓解单智能体迭代中的误差传播问题；同时采用自省式变异机制，促进隐含知识发现。评估结果表明：AutoICE在标准数据集上成功验证率达90.36%，显著优于当前最优方法；在面向开发者的数据集变体上，验证成功率达88.33%，远超最优方法的65%。
原文摘要 · Abstract (English)
Automatically synthesizing verifiable code from natural language requirements ensures software correctness and reliability while significantly lowering the barrier to adopting the techniques of formal methods. With the rise of large language models (LLMs), long-standing efforts at autoformalization have gained new momentum. However, existing approaches suffer from severe syntactic and semantic errors due to the scarcity of domain-specific pre-training corpora and often fail to formalize implicit knowledge effectively. In this paper, we propose AutoICE, an LLM-driven evolutionary search for synthesizing verifiable C code. It introduces the diverse individual initialization and the collaborative crossover to enable diverse iterative updates, thereby mitigating error propagation inherent in single-agent iterations. Besides, it employs the self-reflective mutation to facilitate the discovery of implicit knowledge. Evaluation results demonstrate the effectiveness of AutoICE: it successfully verifies $90.36$\% of code, outperforming the state-of-the-art (SOTA) approach. Besides, on a developer-friendly dataset variant, AutoICE achieves a $88.33$\% verification success rate, significantly surpassing the $65$\% success rate of the SOTA approach.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。