EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning

• URL: http://arxiv.org/abs/2602.22609v1
• Date: Thu, 26 Feb 2026 04:32:07 GMT
• Title: EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
• Authors: Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang,
• Abstract summary: We introduce EvolveGen, a framework for generating hardware model checking benchmarks.<n>Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs.<n>Our experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats.
• Score: 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.

Related papers

• Scaling Up AI-Generated Image Detection via Generator-Aware Prototypes [15.99138549265524]
  Generator-Aware Prototype Learning (GAPL) is a framework that constrains representation with a structured learning paradigm.<n>GAPL achieves state-of-the-art performance, showing superior detection accuracy across a wide variety of GAN and diffusion-based generators.
  arXiv  Detail & Related papers  (2025-12-15T04:58:08Z)
• Dynamic Generation of Multi-LLM Agents Communication Topologies with Graph Diffusion Models [99.85131798240808]
  We introduce a novel generative framework called textitGuided Topology Diffusion (GTD)<n>Inspired by conditional discrete graph diffusion models, GTD formulates topology synthesis as an iterative construction process.<n>At each step, the generation is steered by a lightweight proxy model that predicts multi-objective rewards.<n>Experiments show that GTD can generate highly task-adaptive, sparse, and efficient communication topologies.
  arXiv  Detail & Related papers  (2025-10-09T05:28:28Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• VERIRL: Boosting the LLM-based Verilog Code Generation via Reinforcement Learning [32.974199255760944]
  We introduce a reinforcement learning framework tailored for Verilog code generation.<n>To tackle the problem of sparse and noisy reward signals, we propose a Trace-back based Rescore mechanism.<n>To mitigate catastrophic forgetting and overfitting during RL fine-tuning, we introduce a sample-balanced weighting strategy.
  arXiv  Detail & Related papers  (2025-08-25T20:20:44Z)
• STEPWISE-CODEX-Bench: Evaluating Complex Multi-Function Comprehension and Fine-Grained Execution Reasoning [6.282781900938977]
  We present STEPWISE-CODEX-Bench (SX-Bench), a novel benchmark for complex multi-function understanding and fine-grained execution reasoning.<n>SX-Bench is highly discriminative, even the state-of-the-art OpenAI-O3 achieves only 78.37 percent accuracy on Hard-Reasoning tasks.
  arXiv  Detail & Related papers  (2025-08-07T09:28:43Z)
• EALG: Evolutionary Adversarial Generation of Language Model-Guided Generators for Combinatorial Optimization [5.575239967310329]
  We introduce EALG (Evolutionary Adrial Generation of Language Model Generators), a novel framework that co-evolutione optimization problem instances and their corresponding solvers using large language models (LLMs)<n>EALG leverages a mutation-based approach that dynamically evolves instance generation procedures to create increasingly difficult problems, while simultaneously adaptive adversarial algorithms through interactions with LLMs guided by algorithmic structure.<n>This work explores a new paradigm for optimization that integrates instance generation with solver design, resulting in state-of-the-art performance.
  arXiv  Detail & Related papers  (2025-06-03T08:13:41Z)
• Satori-SWE: Evolutionary Test-Time Scaling for Sample-Efficient Software Engineering [51.7496756448709]
  Language models (LMs) perform well on coding benchmarks but struggle with real-world software engineering tasks.<n>Existing approaches rely on supervised fine-tuning with high-quality data, which is expensive to curate at scale.<n>We propose Test-Time Scaling (EvoScale), a sample-efficient method that treats generation as an evolutionary process.
  arXiv  Detail & Related papers  (2025-05-29T16:15:36Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  Recent advances in large language models (LLMs) have improved their performance on coding benchmarks.<n>However, improvement is plateauing due to the exhaustion of readily available high-quality data.<n>We propose Sol-Ver, a self-play solver-verifier framework that jointly improves a single model's code and test generation capacity.
  arXiv  Detail & Related papers  (2025-02-20T18:32:19Z)
• Alice in Wonderland: Simple Tasks Showing Complete Reasoning Breakdown in State-Of-the-Art Large Language Models [13.532180752491954]
  Large Language Models (LLMs) are often described as instances of foundation models that possess strong generalization obeying scaling laws.<n>We demonstrate here a dramatic breakdown of generalization and basic reasoning of all SOTA models claiming strong function.<n>We also observe strong overconfidence in the wrong solutions, expressed in form of plausible sounding explanation-like confabulations.
  arXiv  Detail & Related papers  (2024-06-04T07:43:33Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  We introduce a novel approach to directly optimize a reinforcement learning objective, maximizing an expected reward. We test our methodology on two tasks: generating molecules with user-defined properties and identifying short python expressions which evaluate to a given target value.
  arXiv  Detail & Related papers  (2020-10-05T20:03:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.