論文の概要: From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications

• arxiv url: http://arxiv.org/abs/2610.30725v1
• Date: Thu, 22 Oct 2026 04:48:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.214321
• Title: From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications
• Title（参考訳）: 自然言語から検証Cへ:ACSL仕様による検証ガイド生成
• Abstract要約: 本稿では,CプログラムとACSL仕様を自然言語要求から合成するための形式的検証に適したフレームワークであるVeriGen-Cを紹介する。 コード生成と修復は、証明関連状態の公開、推論検証のための制御フローの合理化、自動証明探索の妨げとなる実装パターンの排除に制約される。
• 参考スコア（独自算出の注目度）: 13.473192257235732
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: AI-assisted code generation amplifies the demand for automated formal verification. Generated programs must not only be executable but also accompanied by machine-checkable evidence of correctness. Existing approaches can synthesize functionally plausible code or plausible-looking specifications from natural-language prompts; however, they do not explicitly co-design the implementation and specification as a unified artifact optimized for verification. Consequently, automated verifiers often fail to discharge proof obligations. Typical failure modes include missing or implicit proof anchors, program structures that are hostile to automated reasoning, and inconsistencies between code-level state and specification-level requirement facts arising from the independent generation of code and specifications. Even when verification succeeds, it may only establish weak specifications that omit requirement-critical behavior. This paper introduces VeriGen-C, a formal-verification-friendly framework for the joint synthesis of C programs and ACSL specifications from natural-language requirements. Code generation and repair are constrained to expose proof-relevant state, to streamline control flow for deductive verification, and to eliminate implementation patterns that hinder automated proof search. Specification generation and refinement are similarly constrained to mitigate verification timeouts and to ensure alignment with the user requirements. Empirical evaluations on HumanEval-X, FM-Bench, and LiveCodeBench Lite demonstrate that VeriGen-C substantially improves the rate of verified and requirement-aligned solutions relative to an interface-compatible baseline, from 5.5% to 44.5%, from 44.3% to 80.0%, and from 6.5% to 58.7%, respectively.
• Abstract（参考訳）: AI支援コード生成は、自動形式検証の需要を増幅する。 生成プログラムは実行可能なだけでなく、マシンチェック可能な正しさの証拠も伴わなければならない。 既存のアプローチでは、自然言語のプロンプトから機能的にもっともらしいコードや可視的な仕様を合成することができるが、検証に最適化された統一されたアーティファクトとして実装と仕様を明示的に設計するわけではない。 その結果、自動検証器は証明義務を負うことができないことが多い。 典型的な障害モードには、欠落または暗黙の証明アンカー、自動推論に敵対するプログラム構造、コードレベルの状態とコードと仕様の独立した生成から生じる仕様レベルの要件事実の矛盾が含まれる。 検証が成功したとしても、要件クリティカルな振る舞いを省略する弱い仕様のみを確立することができる。 本稿では,CプログラムとACSL仕様を自然言語要求から合成するための形式的検証に適したフレームワークであるVeriGen-Cを紹介する。 コード生成と修復は、証明関連状態の公開、推論検証のための制御フローの合理化、自動証明探索の妨げとなる実装パターンの排除に制約される。 仕様の生成と改善も同様に、検証タイムアウトを緩和し、ユーザ要求との整合性を確保するために制約されている。 HumanEval-X、FM-Bench、LiveCodeBench Liteの実証的な評価では、VeriGen-Cはインターフェース互換のベースラインに対して、それぞれ5.5%から44.5%、44.3%から80.0%、そして6.5%から58.7%に、検証されたソリューションと要求に沿ったソリューションの速度を大幅に改善している。

関連論文リスト

• SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications [6.938883655442837]
  SpecAgentは現実世界のCプログラムの高品質な仕様を合成するためのエージェントフレームワークである。 14の現実世界リポジトリから50のプログラムで、SpecAgent with DeepSeek-V4は96.82%の精度と88.95%のリコールを正確かつ強力な仕様で達成している。
  論文  参考訳（メタデータ） (2026-10-04T11:24:28Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。 VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。 我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
  論文  参考訳（メタデータ） (2026-04-12T00:52:27Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  自動JML仕様合成における古典的手法と急進的手法を比較した。 提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。 本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
  論文  参考訳（メタデータ） (2026-03-31T22:12:15Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
  論文  参考訳（メタデータ） (2025-07-07T10:30:05Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。