論文の概要: Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
- arxiv url: http://arxiv.org/abs/2606.22413v1
- Date: Sun, 21 Jun 2026 10:01:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-24 16:10:15.107101
- Title: Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
- Title（参考訳）: フォーマルメソッド駆動型バイブ符号化 - モデル駆動工学によるAI生成型安全クリティカルソフトウェアにおける検証ループのクローン化
- Authors: Ran Wei, Le Zhu, Haochi Wang, Jim Woodcock, Fang Yan, Simon Foster, Xiangyang Ji,
- Abstract要約: バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。
DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。
フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
- 参考スコア（独自算出の注目度）: 40.048798975817924
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Vibe coding -- accepting LLM-generated source from natural-language intent with minimal review -- is fast and may be adequate for low-criticality consumer software. But for safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification: large language models (LLMs) provide no formal correctness guarantees, and existing remedies target verification-aware languages (Dafny, Verus, Lean) that are scarce in pretraining data and absent from industrial toolchains. This paper closes the gap. We present Forge (Formal method Oriented Refinement loop for GEnerated code): a closed-loop pipeline that guides vibe coding through formal verification using established Model-Driven Engineering (MDE) infrastructure. Through vibe coding, we generate Java source code; our pipeline then extracts -- via model transformations -- formal artefacts in three different formalisms, each checked by a complementary verifier: deductive verification (Dafny), Communicating Sequential Processes (CSP) refinement via the Failures-Divergences Refinement checker (FDR4), and theorem proving using Z-Machines in Isabelle; every verification failure becomes a structured correction prompt that drives the next code-generation iteration. The LLM is the draft generator, the MDE chain is the discriminator, and the developer never has to read the formal models. Empirically, we find that the pipeline produces standards-relevant verification evidence for LLM-generated Java -- a step toward certification.
- Abstract（参考訳）: バイブコーディング -- 最小限のレビューで自然言語意図からLLM生成ソースを受け入れる -- は高速で、低臨界のコンシューマソフトウェアに適している可能性がある。
しかし、DO-178C、IEC 61508、ISO 26262が管理する安全クリティカルなシステムでは、認証への道は提供されていない。
この論文はギャップを埋める。
GEnerated Code の Forge (Formal method Oriented Refinement loop for GEnerated code): 確立した Model-Driven Engineering (MDE) インフラストラクチャを使用して,形式検証を通じてビブコーディングをガイドするクローズドループパイプライン。
デダクティブ検証(Dafny)、Failures-Divergences Refinement Checker(FDR4)によるシーケンスプロセス(CSP)の洗練、IsabelleのZ-Machinesを使った定理証明などです。
LLMはドラフトジェネレータであり、MDEチェーンは識別器であり、開発者は形式的なモデルを読む必要がない。
経験的に、パイプラインは LLM 生成 Java の標準関連検証エビデンスを生成します。
関連論文リスト
- 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) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。
LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。
我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
論文 参考訳（メタデータ） (2025-04-23T18:04:38Z) - Type-Constrained Code Generation with Language Models [51.03439021895432]
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。
そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。
提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
論文 参考訳（メタデータ） (2025-04-12T15:03:00Z) - AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。
LLMによる正式な認証コードの生成は、トレーニングデータの不足と、形式的な証明の複雑さによって妨げられる。
我々は、公式に認証されたコード生成をブートストラップする自己改善フレームワークであるAlphaVerusを紹介した。
論文 参考訳（メタデータ） (2024-12-09T03:22:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。