論文の概要: Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning

• arxiv url: http://arxiv.org/abs/2509.06239v1
• Date: Sun, 07 Sep 2025 23:04:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-09 14:07:03.918164
• Title: Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning
• Title（参考訳）: Proof2Silicon: 強化学習による検証済みコードとハードウェア生成のプロンプト修復
• Authors: Manvi Jha, Jiaxin Wan, Deming Chen,
• Abstract要約: この研究は、新しいエンドツーエンド合成フレームワークであるProof2Siliconを提示する。 以前提案されたPreFACEフローを組み込んで、自然言語仕様から直接、正確性バイコンストラクションハードウェアを生成する。
• 参考スコア（独自算出の注目度）: 7.574481956683386
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) have demonstrated impressive capabilities in automated code generation but frequently produce code that fails formal verification, an essential requirement for hardware and safety-critical domains. To overcome this fundamental limitation, we previously proposed PREFACE, a model-agnostic framework based on reinforcement learning (RL) that iteratively repairs the prompts provided to frozen LLMs, systematically steering them toward generating formally verifiable Dafny code without costly fine-tuning. This work presents Proof2Silicon, a novel end-to-end synthesis framework that embeds the previously proposed PREFACE flow to enable the generation of correctness-by-construction hardware directly from natural language specifications. Proof2Silicon operates by: (1) leveraging PREFACE's verifier-driven RL agent to optimize prompt generation iteratively, ensuring Dafny code correctness; (2) automatically translating verified Dafny programs into synthesizable high-level C using Dafny's Python backend and PyLog; and (3) employing Vivado HLS to produce RTL implementations. Evaluated rigorously on a challenging 100-task benchmark, PREFACE's RL-guided prompt optimization consistently improved Dafny verification success rates across diverse LLMs by up to 21%. Crucially, Proof2Silicon achieved an end-to-end hardware synthesis success rate of up to 72%, generating RTL designs through Vivado HLS synthesis flows. These results demonstrate a robust, scalable, and automated pipeline for LLM-driven, formally verified hardware synthesis, bridging natural-language specification and silicon realization.
• Abstract（参考訳）: LLM(Large Language Models)は、自動コード生成において印象的な機能を示しているが、ハードウェアとセーフティクリティカルドメインの必須要件である正式な検証に失敗するコードを生成することが多い。 この基本的な制限を克服するために、我々は以前、強化学習(RL)に基づくモデルに依存しないフレームワークであるPreFACEを提案しました。 本稿ではProof2Siliconについて紹介する。Proof2Siliconは従来提案されていたPreFACEフローを組み込んだ新しいエンドツーエンド合成フレームワークで,自然言語仕様から直接の正確性バイコンストラクションハードウェアの生成を可能にする。 Proof2Silicon は,(1) PreFACE の検証器駆動 RL エージェントを活用して迅速な生成を最適化し,Dafny のコード正しさを保証する,(2) Dafny プログラムを Dafny の Python バックエンドと PyLog を使って,合成可能な高レベル C に変換する,(3) Vivado HLS を使用して RTL 実装を生成する,といった操作を行う。 挑戦的な100タスクのベンチマークに基づいて厳格に評価され、PreFACEのRL誘導の即時最適化により、様々なLLMのダフニー検証成功率を最大21%改善した。 Proof2Siliconは、Vivado HLS合成フローを通じてRTLの設計を生成するため、エンドツーエンドのハードウェア合成の成功率は最大72%に達した。 これらの結果は、LLM駆動で正式に検証されたハードウェア合成、自然言語仕様のブリッジング、シリコン実現のための堅牢でスケーラブルで自動化されたパイプラインを示す。

関連論文リスト

• Compiling Prompts, Not Crafting Them: A Reproducible Workflow for AI-Assisted Evidence Synthesis [1.624454100511275]
  大規模言語モデル(LLM)は、体系的な文献レビューを加速する大きな可能性を秘めている。 現在のアプローチは、しばしば信頼性と厳密さを損なう、不安定で手作業によるプロンプトに依存している。 本研究では、タスク宣言、テストスイート、自動プロンプトチューニングを再現可能なSLRに組み込む、構造化されたドメイン固有フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-08-22T21:37:49Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• ChipSeek-R1: Generating Human-Surpassing RTL with LLM via Hierarchical Reward-Driven Reinforcement Learning [32.11086992218369]
  ChipSeek-R1は、大規模な言語モデルのための階層的な報酬駆動強化学習フレームワークである。 関数的正当性とPPA最適化の両方のRTLコードを生成する。 RTLLMのベンチマークでは、ChipSeek-R1はオリジナルの人間の書いたコードのPPAメトリクスを超える27のRTL設計を作成した。
  論文  参考訳（メタデータ） (2025-07-07T08:08:20Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• TuRTLe: A Unified Evaluation of LLMs for RTL Generation [0.6010802600885173]
  本研究では,主要なRTL生成タスク間でLLMを評価するための統合評価フレームワークTuRTLeを提案する。 オープンLLMの多様なセットをベンチマークし、EDA固有のタスクの長所と短所を分析します。 以上の結果から,DeepSeek R1のような推論モデルの方が,複数の評価基準で常に優れていたことが示唆された。
  論文  参考訳（メタデータ） (2025-03-31T07:43:12Z)
• HDLCoRe: A Training-Free Framework for Mitigating Hallucinations in LLM-Generated HDL [8.078194378107936]
  HDLCoReは、大規模言語モデルのHDL生成能力を向上する、トレーニング不要のフレームワークである。 本フレームワークはRTLLM2.0ベンチマークにおいて優れた性能を発揮する。
  論文  参考訳（メタデータ） (2025-03-18T07:09:39Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• AIvril: AI-Driven RTL Generation With Verification In-The-Loop [0.7831852829409273]
  LLM(Large Language Models)は、複雑な自然言語処理タスクを実行できる計算モデルである。 本稿では,RTL対応LLMの精度と信頼性を高めるためのフレームワークであるAIvrilを紹介する。
  論文  参考訳（メタデータ） (2024-09-03T15:07:11Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  2つの主要コンポーネントからなるコード生成の新しいフレームワークであるStepCoderを紹介します。 CCCSは、長いシーケンスのコード生成タスクをCurriculum of Code Completion Subtaskに分割することで、探索課題に対処する。 FGOは、未実行のコードセグメントをマスクすることでのみモデルを最適化し、Fine-Grained Optimizationを提供する。 提案手法は,出力空間を探索し,対応するベンチマークにおいて最先端の手法より優れた性能を発揮する。
  論文  参考訳（メタデータ） (2024-02-02T13:14:31Z)

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

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