論文の概要: Certified Program Synthesis with a Multi-Modal Verifier

• arxiv url: http://arxiv.org/abs/2604.16584v1
• Date: Fri, 17 Apr 2026 14:56:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-22 14:04:47.795681
• Title: Certified Program Synthesis with a Multi-Modal Verifier
• Title（参考訳）: マルチモーダル検証器による認定プログラム合成
• Abstract要約: LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。 動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。 我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
• 参考スコア（独自算出の注目度）: 5.998029529040967
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode -- auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) -- with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier -- a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget -- consistently across two frontier LLM backends.
• Abstract（参考訳）: 認定プログラム合成(Certified program synthesis、別名vericoding)は、プログラムを自動生成するプロセスであり、その形式仕様と、自然言語による記述からのアライメントの機械チェック可能な証明である。 2つの課題は、バリコーディングを難しくする。 第一に、自然言語から合成された仕様は、意味を持つには弱すぎるか、実装可能なには強すぎるが、既存のアプローチにはそのような欠陥を検出するための体系的な手段がない。 第二に、プログラム検証の状況は断片化されている。それぞれのツールは、自動化と表現性の間に独自のトレードオフを持つ、特定の推論モード -- 自動アクティブ(例:Dafny、Verus)、インタラクティブ(例:Coq、Lean) -- をサポートする。 これにより、すべての合成方法論を単一の検証パラダイムに調整し、効果的に扱えるタスクのクラスを制限せざるを得ない。 動的検証、自動証明、インタラクティブな証明スクリプティングをひとつの基盤フレームワークで組み合わせた単一のツールです。 このアイデアはLeetProofという,Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインで実現しています。 マルチモダリティにより、LeetProofは、コードが合成される前にランダム化されたプロパティベースのテストを通じて生成された仕様を検証し、その合成タスクを検証条件でガイドされたサブプロブレムに分解し、リーンに特化したフロンティアAIプロデューサに残余の証明義務を委譲する。 我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。 当社の仕様検証では,既存のリファレンスベンチマークの欠陥を明らかにしています。LeetProofのステージドパイプラインは,同じ予算で,単一モードのベースライン – 一貫して2つのフロンティアLMバックエンド – よりもはるかに高い,完全認定ソリューションの速度を実現しています。

関連論文リスト

• SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
  我々は、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであるSKILLFORGEを紹介する。 検証駆動ハーネスはこれらのスキルを編成する。 Dafny仕様のペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチよりも大幅に優れている。
  論文  参考訳（メタデータ） (2026-08-30T15:15:00Z)
• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。 微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。 SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。 Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
  論文  参考訳（メタデータ） (2026-07-22T06:20:36Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。 ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。 1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
  論文  参考訳（メタデータ） (2026-07-01T09:58:59Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  自動JML仕様合成における古典的手法と急進的手法を比較した。 提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。 本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
  論文  参考訳（メタデータ） (2026-03-31T22:12:15Z)
• Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
  LLMは、中間出力を伝搬しながら、正しい順序で複数の依存APIを呼び出す必要がある。 既存の環境は、シミュレーションデータを使った単純なターン毎の関数呼び出しとバイナリ報酬に重点を置いている。 まず、実APIレスポンスの大規模キャッシュを背景とした強化学習環境を構築し、有効なマルチステップオーケストレーショントレースをサンプリングするデータ合成パイプラインを実現する。 第二に、正当性を原子の妥当性とオーケストレーションに分解する、段階的な報酬設計を提案する。
  論文  参考訳（メタデータ） (2026-03-25T18:31:39Z)
• 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)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。 AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。 このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
  論文  参考訳（メタデータ） (2025-07-14T14:43:14Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)

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

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