論文の概要: EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning

• arxiv url: http://arxiv.org/abs/2602.22609v1
• Date: Thu, 26 Feb 2026 04:32:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-27 18:41:22.52532
• Title: EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
• Title（参考訳）: EvolveGen: 強化学習によるベンチマーク生成をチェックするアルゴリズムレベルのハードウェアモデル
• Authors: Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang,
• Abstract要約: ハードウェアモデルチェックベンチマークを生成するフレームワークであるEvolveGenを紹介する。 提案手法は、RLエージェントが計算グラフを構築することを学習するアルゴリズム的な抽象レベルで機能する。 実験の結果,EvolveGenは標準フォーマットの多様なベンチマークセットを効率的に作成できることがわかった。
• 参考スコア（独自算出の注目度）: 4.8941849720433686
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number, often distributed only in representations such as BTOR2 without access to the originating register-transfer-level (RTL) designs, and biased toward extreme difficulty where instances are either trivial or intractable. These limitations hinder rigorous evaluation of new verification techniques and encourage overfitting of solver heuristics to a narrow set of problems. To address this, we introduce EvolveGen, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs. By compiling these graphs under different synthesis directives, we produce pairs of functionally equivalent but structurally distinct hardware designs, inducing challenging model checking instances. Solver runtime is used as the reward signal, enabling the agent to autonomously discover and generate small-but-hard instances that expose solver-specific weaknesses. Experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats (e.g., AIGER and BTOR2) and effectively reveals performance bottlenecks in state-of-the-art model checkers.
• Abstract（参考訳）: ハードウェアモデル検査の進歩は、高品質なベンチマークに大きく依存する。 しかし、コミュニティは重要なベンチマークのギャップに直面している: 既存のスイートは数に限られており、しばしばBTOR2のような表現でのみ配布され、元のレジスタ・トランスファー・レベル(RTL)設計にアクセスできない。 これらの制限は、新しい検証手法の厳密な評価を妨げ、より狭い問題に対する解法ヒューリスティックスの過度な適合を奨励する。 そこで本稿では,強化学習(RL)と高レベル合成(HLS)を組み合わせることにより,ハードウェアモデルチェックベンチマークを生成するフレームワークであるEvolveGenを紹介する。 提案手法は、RLエージェントが計算グラフを構築することを学習するアルゴリズム的な抽象レベルで機能する。 これらのグラフを異なる合成指示の下でコンパイルすることにより、機能的に等価だが構造的に異なるハードウェア設計のペアを生成し、困難なモデルチェックインスタンスを誘導する。 ソルバーランタイムは報酬信号として使用され、エージェントは、ソルバー固有の弱点を露呈する小さながハードなインスタンスを自律的に発見し、生成することができる。 実験によると、EvolveGenは標準フォーマット(例えば、AIGERとBTOR2)の様々なベンチマークセットを効率的に作成し、最先端のモデルチェッカーのパフォーマンスボトルネックを効果的に明らかにしている。

関連論文リスト

• Scaling Up AI-Generated Image Detection via Generator-Aware Prototypes [15.99138549265524]
  GAPL(Generator-Aware Prototype Learning)は、構造化学習パラダイムで表現を制約するフレームワークである。 GAPLは最先端の性能を達成し、多様なGANおよび拡散型ジェネレータにおいて優れた検出精度を示す。
  論文  参考訳（メタデータ） (2025-12-15T04:58:08Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  言語モデルの生成能力をプロセス検証器と組み合わせたテストタイムアルゴリズムは、新しい推論能力を引き出すための有望なレバーを提供する。 提案手法は, 理論的に根拠付きバックトラックを用いて, 検証誤差に対して, 確実な堅牢性を実現するための新しいプロセス誘導型テスト時間サンプリングアルゴリズムであるVGBを導入する。
  論文  参考訳（メタデータ） (2025-10-03T16:21:14Z)
• VERIRL: Boosting the LLM-based Verilog Code Generation via Reinforcement Learning [32.974199255760944]
  本稿では,Verilogコード生成に適した強化学習フレームワークを提案する。 スパース信号と雑音信号に対処するために,トレースバックに基づくRescore機構を提案する。 RL微調整中の破滅的忘れと過適合を軽減するため,サンプルバランスの重み付け戦略を導入する。
  論文  参考訳（メタデータ） (2025-08-25T20:20:44Z)
• STEPWISE-CODEX-Bench: Evaluating Complex Multi-Function Comprehension and Fine-Grained Execution Reasoning [6.282781900938977]
  複雑な多機能理解と細粒度実行推論のための新しいベンチマークであるSTEPWISE-CODEX-Bench(SX-Bench)を提案する。 SX-Benchは非常に差別的であり、最先端のOpenAI-O3でさえハード推論タスクでは78.7%の精度しか達成していない。
  論文  参考訳（メタデータ） (2025-08-07T09:28:43Z)
• EALG: Evolutionary Adversarial Generation of Language Model-Guided Generators for Combinatorial Optimization [5.575239967310329]
  EALG(Evolutionary Adrial Generation of Language Model Generators)は,大規模言語モデル(LLM)を用いた最適化問題インスタンスとその対応解法を共進化させる新しいフレームワークである。 EALGは、動的にインスタンス生成手順を進化させ、ますます難しい問題を生み出すとともに、アルゴリズム構造によって導かれるLLMとの相互作用を通じて、対向アルゴリズムを同時に適応させる。 この研究は、インスタンス生成とソルバ設計を統合した最適化のための新しいパラダイムを探求し、その結果、最先端のパフォーマンスを実現した。
  論文  参考訳（メタデータ） (2025-06-03T08:13:41Z)
• Satori-SWE: Evolutionary Test-Time Scaling for Sample-Efficient Software Engineering [51.7496756448709]
  言語モデル(LM)は、コーディングベンチマークではうまく機能するが、現実のソフトウェア工学のタスクでは苦労する。 既存のアプローチは、高品質なデータによる教師付き微調整に依存している。 本研究では, 生成を進化過程として扱うサンプル効率の高い手法であるテスト時間スケーリング(EvoScale)を提案する。
  論文  参考訳（メタデータ） (2025-05-29T16:15:36Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。 しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。 本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
  論文  参考訳（メタデータ） (2025-02-20T18:32:19Z)
• Alice in Wonderland: Simple Tasks Showing Complete Reasoning Breakdown in State-Of-the-Art Large Language Models [13.532180752491954]
  大規模言語モデル(LLM)は、しばしばスケーリング法則に従う強力な一般化を持つ基礎モデルの例として記述される。 ここでは、強い関数を主張する全てのSOTAモデルの一般化と基本的推論の劇的な分解を示す。 また、間違った解法において強い過信感を観察し、妥当な音響的説明のような折り畳みの形で表現する。
  論文  参考訳（メタデータ） (2024-06-04T07:43:33Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  本稿では,強化学習目標を直接最適化し,期待される報酬を最大化するための新しいアプローチを提案する。 提案手法は、ユーザ定義プロパティを持つ分子の生成と、所定の目標値を評価する短いピソン表現の同定という2つのタスクで検証する。
  論文  参考訳（メタデータ） (2020-10-05T20:03:13Z)

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

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