論文の概要: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

• arxiv url: http://arxiv.org/abs/2605.23109v1
• Date: Fri, 22 May 2026 00:05:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-25 17:29:20.137556
• Title: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
• Title（参考訳）: インダクティブ・デダクティブ・シンセシス: 形式的に検証されたシステムを生成するAIの実現
• Authors: Shubham Agarwal, Alexander Krentsel, Shu Liu, Mert Cemri, Audrey Cheng, Rui Meng, Tomas Pfister, Chun-Liang Li, Sylvia Ratnasamy, Aditya Parameswaran, Matei Zaharia, Ion Stoica, Mohsen Lesani,
• Abstract要約: 本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。 IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。 IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
• 参考スコア（独自算出の注目度）: 100.24694338574402
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
• Abstract（参考訳）: AIエージェントは、コードの生成、テスト、精製にますます長けている。 しかし、彼らはテストだけでは提供できない完全なカバレッジの正式な保証を必要とするタスクに不足している。 読み取りと書き込み間の一貫性のようなプロパティは、イベントのインターリーブ可能なすべての条件で保持されなければならない。 機械化された正式な検証はそのような正確性を保証することができるが、通常、数ヶ月から数年の専門的な努力を必要とする。 証拠として、SOTAのコーディングエージェント(GPT-5.4のCodexとOpus 4.6のClaude Code)でさえ、2/7の分散キーバリューストア仕様でしか成功していない。 本稿では,このギャップに対処する最初の効果的な手法であるインダクティブ・デダクティブ・シンセシス(IDS)について述べる。 エージェントLLMシステムとして構築されたIDSは、平均で約6.8時間106ドル、専門家の努力の約200倍、SOTAエージェントの約17%のコストで7/7を達成している。 IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。

関連論文リスト

• From I/O to Code with Discovery Agent [103.88427301265669]
  IO2Codeの発見エージェントであるDIO-Agentを提案する。 本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。 大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
  論文  参考訳（メタデータ） (2026-05-14T18:57:32Z)
• The Productivity-Reliability Paradox: Specification-Driven Governance for AI-Augmented Software Development [0.0]
  コントロールされた研究によると、よくスコープされたタスクで生産性が20～56%向上し、最も厳格なRCT文書は経験豊富な開発者にとって19%の減速を報告している。 10,000人以上の開発者を対象としたテレメトリでは、プルリクエストが98%増加したが、フラットなデリバリメトリクスによるレビュー時間が91%長かった。 本稿では,非決定論的コードジェネレータから生じる系統的な現象と,仕様の不十分な規律であるProductivity-Reliability Paradox(PRP)について論じる。
  論文  参考訳（メタデータ） (2026-05-01T23:37:50Z)
• Towards Multi-Agent Autonomous Reasoning in Hydrodynamics [0.06999740786886537]
  本稿では,多エージェントをレイヤ実行グラフ(LEG)を介して協調させる,流体力学のためのマルチエージェントシステム(MAS)のプロトタイプを提案する。 プランナーエージェントは、ドメイン知識を厳密な制御ロジックとしてハードコーディングすることなく、自然言語ルーティングからクエリ固有の実行トポロジを構築する。 レポーターエージェントが最終応答を合成し、ランタイムが監査性をサポートするためのツール呼び出し毎に証明をログする。
  論文  参考訳（メタデータ） (2026-05-01T21:17:55Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoderはエージェントコード検証フレームワークである。 コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
  論文  参考訳（メタデータ） (2026-03-31T00:06:44Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  コード検証は、LLMベースのコード生成の検証後において重要な役割を果たす。 既存の教師付き微調整手法は、データの不足、高い失敗率、推論効率の低下に悩まされている。 機能的な報酬しか持たない単純RLは、難しいブランチやサンプルに対して効果的な単体テストを生成することができないことを示す。
  論文  参考訳（メタデータ） (2026-01-30T10:33:29Z)
• AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution [20.91584024250844]
  AutoICEは、検証可能なCコードの合成のための進化的検索である。 90.36$%のコードを検証し、最先端のSOTA(State-of-the-art)アプローチを上回った。
  論文  参考訳（メタデータ） (2025-12-08T12:35:10Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• CoopetitiveV: Leveraging LLM-powered Coopetitive Multi-Agent Prompting for High-quality Verilog Generation [7.2267316594130095]
  既存のアプローチでは、LLM支援のシングルエージェントプロンプトまたは協調のみのマルチエージェント学習が使用されている。 エージェント同士が協調して生成パイプラインを形成することのできない,LLMに基づく協調型マルチエージェントプロンプトフレームワークを提案する。 実験結果から, コーペティティブ・マルチエージェント・フレームワークは, 劣化リスクを効果的に軽減し, エラー伝播を低減できることが示唆された。
  論文  参考訳（メタデータ） (2024-12-15T01:58:10Z)
• DS-Agent: Automated Data Science by Empowering Large Language Models with Case-Based Reasoning [56.887047551101574]
  大規模言語モデル(LLM)エージェントとケースベース推論(CBR)を利用した新しいフレームワークであるDS-Agentを提案する。 開発段階では、DS-AgentはCBRフレームワークに従い、自動イテレーションパイプラインを構築する。 デプロイメントの段階では、DS-Agentは、シンプルなCBRパラダイムで低リソースのデプロイメントステージを実装し、LCMの基本能力に対する需要を大幅に削減する。
  論文  参考訳（メタデータ） (2024-02-27T12:26:07Z)

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

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