# AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution

arXiv: https://arxiv.org/abs/2512.07501 · HTML: https://mlsanity.com/paper/2512.07501/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 47 of its 95 references that are in the map.
- First posted on arXiv 8 Dec 2025.

## Builds on (most cited first, 30 of 47)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [A Survey on Evaluation of Large Language Models](https://mlsanity.com/paper/2307.03109/) (2023)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [Tulu 3: Pushing Frontiers in Open Language Model Post-Training](https://mlsanity.com/paper/2411.15124/) (2024)
- [Enhancing Chat Language Models by Scaling High-quality Instructional Conversations](https://mlsanity.com/paper/2305.14233/) (2023)
- [CodeXGLUE: A Machine Learning Benchmark Dataset for Code Understanding and Generation](https://mlsanity.com/paper/2102.04664/) (2021)
- [Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm](https://mlsanity.com/paper/2102.07350/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [PromptSource: An Integrated Development Environment and Repository for Natural Language Prompts](https://mlsanity.com/paper/2202.01279/) (2022)
- [ReEvo: Large Language Models as Hyper-Heuristics with Reflective Evolution](https://mlsanity.com/paper/2402.01145/) (2024)
- [TextGrad: Automatic "Differentiation" via Text](https://mlsanity.com/paper/2406.07496/) (2024)
- [Evolution of Heuristics: Towards Efficient Automatic Algorithm Design Using Large Language Model](https://mlsanity.com/paper/2401.02051/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Making Large Language Models Better Reasoners with Step-Aware Verifier](https://mlsanity.com/paper/2206.02336/) (2022)
- [Design Guidelines for Prompt Engineering Text-to-Image Generative Models](https://mlsanity.com/paper/2109.06977/) (2021)
- [Take a Step Back: Evoking Reasoning via Abstraction in Large Language Models](https://mlsanity.com/paper/2310.06117/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Prompting Is Programming: A Query Language for Large Language Models](https://mlsanity.com/paper/2212.06094/) (2022)
- [HSEvo: Elevating Automatic Heuristic Design with Diversity-Driven Harmony Search and Genetic Algorithm Using LLMs](https://mlsanity.com/paper/2412.14995/) (2024)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [TIM: Teaching Large Language Models to Translate with Comparison](https://mlsanity.com/paper/2307.04408/) (2023)

## Abstract (arXiv)

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.