論文の概要: AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
- arxiv url: http://arxiv.org/abs/2512.07501v1
- Date: Mon, 08 Dec 2025 12:35:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-09 22:03:54.886139
- Title: AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
- Title（参考訳）: AutoICE: LLM駆動進化による検証可能なCコードの自動合成
- Authors: Weilin Luo, Xueyi Liang, Haotian Deng, Yanan Liu, Hai Wan,
- Abstract要約: AutoICEは、検証可能なCコードの合成のための進化的検索である。
90.36$%のコードを検証し、最先端のSOTA(State-of-the-art)アプローチを上回った。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 検証可能なコードを自然言語要求から自動で合成することで、ソフトウェアの正しさと信頼性が保証されると同時に、形式的な手法を採用する際の障壁を著しく低くする。
大規模言語モデル (LLMs) の台頭に伴い, オートフォーマル化への長年の取り組みが新たな勢いを増している。
しかし、既存のアプローチでは、ドメイン固有の事前学習コーパスが不足しているため、厳密な構文的および意味的誤りに悩まされ、暗黙の知識を効果的に形式化できないことが多い。
本稿では,LLMによる検証可能なCコードの合成のための進化的探索であるAutoICEを提案する。
多様な個別初期化とコラボレーティブ・クロスオーバーを導入し、多様な反復的な更新を可能にすることにより、単一エージェントのイテレーションに固有のエラーの伝播を緩和する。
さらに、暗黙の知識の発見を促進するために自己反射突然変異を用いる。
評価結果はAutoICEの有効性を示し、90.36$\%のコードの検証に成功し、最先端(SOTA)アプローチを上回った。
さらに、開発者フレンドリーなデータセットの亜種であるAutoICEは、88.33$\%の検証成功率を達成し、SOTAアプローチの65$\%の成功率を大幅に上回っている。
関連論文リスト
- Automatic Syntax Error Repair for Discrete Controller Synthesis using Large Language Model [8.741815980649667]
本稿では,Large Language Models (LLMs) を利用してDCSモデルの構文誤りを修復する自動手法を提案する。
LLMには形式文法規則やイラストレーション例を含むDCS固有のドメイン知識が備わっており、正確な修正を導く。
人間の開発者に比べて3.46倍のスピードアップを実現している。
論文 参考訳（メタデータ） (2025-12-08T07:57:15Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Semantic Voting: A Self-Evaluation-Free Approach for Efficient LLM Self-Improvement on Unverifiable Open-ended Tasks [38.058215007885096]
大規模言語モデル(LLM)の自己評価は高い計算オーバーヘッドをもたらし、本質的なバイアスによる過信問題を引き起こす。
本稿では、軽量で効果的な自己改善を目的とした、検証不能なタスクに対する新しい自己評価自由アプローチを提案する。
論文 参考訳（メタデータ） (2025-09-27T02:44:05Z) - AutoMind: Adaptive Knowledgeable Agent for Automated Data Science [70.33796196103499]
LLM(Large Language Model)エージェントは、現実世界のデータサイエンス問題に対処する大きな可能性を示している。
既存のフレームワークは、厳格で、事前定義された、柔軟性のないコーディング戦略に依存している。
適応的で知識のあるLLMエージェントフレームワークであるAutoMindを紹介する。
論文 参考訳（メタデータ） (2025-06-12T17:59:32Z) - Semantic-Preserving Adversarial Attacks on LLMs: An Adaptive Greedy Binary Search Approach [15.658579092368981]
大規模言語モデル(LLM)は、ユーザ入力を洗練させ、応答精度を向上させるために、グラフィカルユーザインタフェース(GUI)における自動プロンプト工学に依存している。
本稿では, セマンティック安定性を維持しつつ, 共通的なプロンプト最適化機構をシミュレートするアダプティブ・グレディ・バイナリ・サーチ(AGBS)手法を提案する。
論文 参考訳（メタデータ） (2025-05-26T15:41:06Z) - UniErase: Towards Balanced and Precise Unlearning in Language Models [69.04923022755547]
大規模言語モデル(LLM)は、古い情報問題に対処するために反復的な更新を必要とする。
UniEraseは、知識の未学習と能力保持の間の精度とバランスの取れたパフォーマンスを示す、新しいアンラーニングフレームワークである。
論文 参考訳（メタデータ） (2025-05-21T15:53:28Z) - Enhancing LLM Reliability via Explicit Knowledge Boundary Modeling [41.19330514054401]
大規模言語モデル(LLM)は、不一致の自己認識に起因する幻覚の傾向にある。
本稿では,高速かつ低速な推論システムを統合し,信頼性とユーザビリティを調和させる明示的知識境界モデリングフレームワークを提案する。
論文 参考訳（メタデータ） (2025-03-04T03:16:02Z) - AutoDetect: Towards a Unified Framework for Automated Weakness Detection in Large Language Models [95.09157454599605]
大規模言語モデル(LLM)はますます強力になってきていますが、それでも顕著ですが微妙な弱点があります。
従来のベンチマークアプローチでは、特定のモデルの欠陥を徹底的に特定することはできない。
さまざまなタスクにまたがるLLMの弱点を自動的に露呈する統合フレームワークであるAutoDetectを導入する。
論文 参考訳（メタデータ） (2024-06-24T15:16:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。