論文の概要: SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs
- arxiv url: http://arxiv.org/abs/2608.29841v1
- Date: Sun, 30 Aug 2026 15:15:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:31.088274
- Title: SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs
- Title（参考訳）: SkillForge: 形式的に検証されたダフニープログラムを生成するためのバリデーション・イン・ザ・ループによる構成スキル合成
- Abstract要約: 我々は、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであるSKILLFORGEを紹介する。
検証駆動ハーネスはこれらのスキルを編成する。
Dafny仕様のペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチよりも大幅に優れている。
- 参考スコア（独自算出の注目度）: 10.916179875278326
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Generating formally verified programs from natural language remains challenging: existing approaches either produce code in a single pass without recourse when verification fails, or rely on open-ended agentic reasoning that is non-deterministic and opaque. We introduce SKILLFORGE, a framework that decomposes formal code synthesis into a library of atomic, reusable skills, each targeting a specific subtask such as specification inference, body synthesis, invariant generation, error diagnosis, or targeted repair, and defined by a prompt template, tool binding, and decidable success criterion. A verification-driven harness orchestrates these skills: it submits candidates to the Dafny verifier, diagnoses failures into structured categories, deterministically routes to the appropriate repair skill, and iterates until formal correctness is proved or a budget is exhausted. On a curated benchmark of natural language to Dafny specification pairs, SKILLFORGE substantially outperforms both state-of-the-art agentic approaches (including ReAct-style agents, MCTS-based repair, and RL-guided verification) and traditional iterative baselines, while requiring fewer tokens and lower latency. Ablation studies confirm that every skill contributes measurably, and the harness converges rapidly with the majority of programs verified on the first attempt.
- Abstract（参考訳）: 既存のアプローチでは、検証が失敗しても、単一のパスでコードを生成するか、非決定論的で不透明なオープンなエージェント推論に依存している。
SKILLFORGEは、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであり、それぞれが仕様推論、ボディ合成、不変生成、エラー診断、ターゲット修復といった特定のサブタスクをターゲットにしており、プロンプトテンプレート、ツールバインディング、決定可能な成功基準によって定義されている。
検証駆動型ハーネスはこれらのスキルを編成する: ダフニー検証器に候補を提出し、故障を構造化されたカテゴリに診断し、決定的に適切な修理スキルにルートし、正式な正しさが証明されるまで反復する。
Dafny仕様ペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチ(ReActスタイルのエージェント、MCTSベースの修復、RL誘導検証など)と従来の反復ベースラインの両方を著しく上回り、トークンが少なく、レイテンシも低い。
アブレーション研究は、すべてのスキルが測定に寄与し、ハーネスは最初の試みで検証されたプログラムの大多数と急速に収束することを確認した。
関連論文リスト
- Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。
動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。
我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
論文 参考訳（メタデータ） (2026-04-17T14:56:45Z) - Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations [0.0]
本稿では,機械学習技術と形式検証を統合したLIFR(Learning-Infused Formal Reasoning)という研究ビジョンを概説する。
このフレームワークは、自然言語要求からの自動コントラクト合成、グラフマッチングと学習ベースの埋め込みを用いた検証アーティファクトのセマンティックリユース、および統一プログラミング理論(UTP)と制度理論に基づく数学的に基礎付けられたセマンティック基盤の3つの相補的な研究方向に焦点を当てている。
論文 参考訳（メタデータ） (2026-04-14T13:58:14Z) - VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
エージェントAIシステムは、驚くほどの頻度でコードを生成することができる。
生成されたコードが実際にユーザが意図した通りに動作するようにします。
論文 参考訳（メタデータ） (2026-03-17T21:28:59Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。
筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。
以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
論文 参考訳（メタデータ） (2025-10-07T13:19:05Z) - Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
Cacoは、高品質で検証可能な多様な命令-CoT推論データの合成を自動化する新しいフレームワークである。
我々の研究は、人間の介入なしに自己持続的で信頼できる推論システムを構築するためのパラダイムを確立します。
論文 参考訳（メタデータ） (2025-10-05T07:59:24Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。