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

• URL: http://arxiv.org/abs/2512.07501v1
• Date: Mon, 08 Dec 2025 12:35:10 GMT
• Title: AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
• Authors: Weilin Luo, Xueyi Liang, Haotian Deng, Yanan Liu, Hai Wan,
• Abstract summary: AutoICE is an evolutionary search for synthesizing verifiable C code.<n>It successfully verifies $90.36$% of code, outperforming the state-of-the-art (SOTA) approach.
• Score: 20.91584024250844
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Autonomous Chain-of-Thought Distillation for Graph-Based Fraud Detection [73.9189065770752]
  Graph-based fraud detection on text-attributed graphs (TAGs) requires jointly modeling rich textual semantics and relational dependencies.<n>We propose FraudCoT, a unified framework that advances TAG-based fraud detection through autonomous, graph-aware chain-of-thought (CoT) reasoning and scalable LLM-GNN co-training.
  arXiv  Detail & Related papers  (2026-01-30T13:12:12Z)
• MulVul: Retrieval-augmented Multi-Agent Code Vulnerability Detection via Cross-Model Prompt Evolution [28.062506040151153]
  Large Language Models (LLMs) struggle to automate real-world vulnerability detection due to two key limitations.<n>The heterogeneity of vulnerability patterns undermines the effectiveness of a single unified model, and manual prompt engineering for massive weakness categories is unscalable.<n>We propose textbfMulVul, a retrieval-augmented multi-agent framework for precise and broad-coverage vulnerability detection.
  arXiv  Detail & Related papers  (2026-01-26T12:43:10Z)
• LLMs in Code Vulnerability Analysis: A Proof of Concept [0.3441021278275805]
  Traditional software security analysis methods struggle to keep pace with the scale and complexity of moderns.<n>This paper explores the incorporation of code-specific and general-purpose Large Language Models to automate critical software security tasks.
  arXiv  Detail & Related papers  (2026-01-13T16:16:11Z)
• Automatic Syntax Error Repair for Discrete Controller Synthesis using Large Language Model [8.741815980649667]
  This paper presents an automated approach that leverages Large Language Models (LLMs) to repair syntax errors in DCS models.<n>It equips the LLM with DCS-specific domain knowledge, including formal grammar rules and illustrative examples, to guide accurate corrections.<n>It achieves a speedup of 3.46 times compared to human developers.
  arXiv  Detail & Related papers  (2025-12-08T07:57:15Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Semantic Voting: A Self-Evaluation-Free Approach for Efficient LLM Self-Improvement on Unverifiable Open-ended Tasks [38.058215007885096]
  Self-evaluation for large language models (LLMs) incurs high computational overhead and introduces overconfidence issues due to intrinsic biases.<n>We propose a novel self-evaluation-free approach for unverifiable tasks, designed for lightweight yet effective self-improvement.
  arXiv  Detail & Related papers  (2025-09-27T02:44:05Z)
• AutoMind: Adaptive Knowledgeable Agent for Automated Data Science [70.33796196103499]
  Large Language Model (LLM) agents have shown great potential in addressing real-world data science problems.<n>Existing frameworks depend on rigid, pre-defined and inflexible coding strategies.<n>We introduce AutoMind, an adaptive, knowledgeable LLM-agent framework.
  arXiv  Detail & Related papers  (2025-06-12T17:59:32Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Semantic-Preserving Adversarial Attacks on LLMs: An Adaptive Greedy Binary Search Approach [15.658579092368981]
  Large Language Models (LLMs) increasingly rely on automatic prompt engineering in graphical user interfaces (GUIs) to refine user inputs and enhance response accuracy.<n>We propose the Adaptive Greedy Binary Search (AGBS) method, which simulates common prompt optimization mechanisms while preserving semantic stability.
  arXiv  Detail & Related papers  (2025-05-26T15:41:06Z)
• UniErase: Towards Balanced and Precise Unlearning in Language Models [69.04923022755547]
  Large language models (LLMs) require iterative updates to address the outdated information problem.<n>UniErase is a novel unlearning framework that demonstrates precision and balanced performances between knowledge unlearning and ability retaining.
  arXiv  Detail & Related papers  (2025-05-21T15:53:28Z)
• Enhancing LLM Reliability via Explicit Knowledge Boundary Modeling [41.19330514054401]
  Large language models (LLMs) are prone to hallucination stemming from misaligned self-awareness.<n>We propose the Explicit Knowledge Boundary Modeling framework to integrate fast and slow reasoning systems to harmonize reliability and usability.
  arXiv  Detail & Related papers  (2025-03-04T03:16:02Z)
• AutoDetect: Towards a Unified Framework for Automated Weakness Detection in Large Language Models [95.09157454599605]
  Large Language Models (LLMs) are becoming increasingly powerful, but they still exhibit significant but subtle weaknesses.<n>Traditional benchmarking approaches cannot thoroughly pinpoint specific model deficiencies.<n>We introduce a unified framework, AutoDetect, to automatically expose weaknesses in LLMs across various tasks.
  arXiv  Detail & Related papers  (2024-06-24T15:16:45Z)
• It's Never Too Late: Fusing Acoustic Information into Large Language Models for Automatic Speech Recognition [70.77292069313154]
  Large language models (LLMs) can be successfully used for generative error correction (GER) on top of the automatic speech recognition (ASR) output. In this work, we aim to overcome such a limitation by infusing acoustic information before generating the predicted transcription through a novel late fusion solution termed Uncertainty-Aware Dynamic Fusion (UADF)
  arXiv  Detail & Related papers  (2024-02-08T07:21:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.