A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking Xiaofeng Zhou⋆1 , Guangyu Hu⋆1 , Hongce Zhang2 , and Wei Zhang1 The Hong Kong University of Science and Technology The Hong Kong University of Science and Technology (Guangzhou) 1
arXiv:2604.21688v1 [cs.LO] 23 Apr 2026
2
Abstract. The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process—a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learningbased framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29. Keywords: Hardware Formal Verification · Model Checking · Inductive Generalization · Machine Learning.
1
Introduction
As the scale and complexity of modern RTL (register transfer level) designs continue to increase, simulation-based verification alone has become insufficient ⋆
Both authors contributed equally to this work.
2
X. Zhou and G. Hu et al.
for uncovering subtle design bugs. Hardware model checking provides a formal and exhaustive means of verifying safety properties by exploring all reachable states. Among SAT-based techniques such as BMC (bounded model checking) [1], k-induction [11], and IC3/PDR [4,5], IC3 has emerged as a state-of-the-art algorithm due to its robustness and its ability to incrementally construct inductive invariants without explicit unrolling. A key determinant of IC3’s efficiency is the inductive generalization step, in which a CTI counterexample to induction is generalized into a clause that blocks a larger set of unreachable states. Techniques such as CtgDown [6] and its extensions (e.g., stronger ICP/IC3 generalization [18] and EXCTG [15]) significantly improve generalization by performing more powerful reasoning about CTGs (counterexamples to generalization). These works show that better generalization, in terms of the width and depth of blocked state space, can substantially accelerate IC3. However, they still depend on fixed or manually tuned strategies: the trade-off between generalization strength and computational overhead is decided once and for all, or adjusted only by handcrafted rules. For example, EXCTG further proposes DynAMic [15], which dynamically switches between several predefined strategies based on the difficulty of blocking states, but the switching policy itself is static and hard-coded. In practice, CTIs are generated under highly diverse circumstances: frame levels, clause densities, and proof-obligation queues all evolve throughout the run of IC3. Overly aggressive generalization may produce clauses that cannot be propagated, while overly conservative generalization may fail to block meaningful regions of the state space, leading to slow convergence. The effectiveness of a generalization strategy is therefore highly context-dependent. Moreover, each generalization affects future CTIs, frame saturation, and clause propagation. From this perspective, inductive generalization is not an isolated subroutine, but part of a sequential, non-stationary decision process that unfolds over the entire proof. Recent learning-based verification approaches operate at different points in this design space. NeuroPDR [8] integrates neural networks into PDR to guide the proof search, and DeepIC3 [7] uses a graph neural network to predict promising clauses for IC3. These methods demonstrate that machine learning can improve SAT/SMT-based model checking, but they rely on offline training, heavy models, and non-trivial inference cost. They are therefore not well-suited to be invoked millions of times inside IC3’s inner inductive generalization loop. What is missing is a lightweight, online mechanism that can adaptively select generalization strategies based on the evolving proof state, without requiring pre-collected datasets or expensive training. Our approach. In this work, we introduce A-IC3, a lightweight, learning-guided framework that adaptively selects inductive generalization strategies inside IC3. Rather than relying on a global fixed strategy or manually designed switching rules, A-IC3 models generalization as a contextual multi-armed bandit problem. Before each generalization, the framework extracts a proof-aware context vector from IC3’s internal state, including CTI characteristics (e.g., cube size, depth,
Title Suppressed Due to Excessive Length
3
activity) and global proof information (e.g., frame level, frame saturation, proofobligation queue growth). A Proof-Aware LinUCB (PA-LinUCB) agent then selects among several predefined generalization strategies of varying aggressiveness. After generalization and intermediate clause propagation, the agent receives a reward that reflects the usefulness of the resulting clause, combining size reduction and push success, and updates its parameters online. Over time, A-IC3 learns which strategies work best in which proof contexts, without any offline training. Why contextual bandits and LinUCB? Strategy selection in IC3 is inherently discrete, must incur negligible overhead, and must cope with non-stationary proof dynamics. Contextual bandits provide exactly this combination of (i) online learning without pre-collected training data, (ii) low computational cost, and (iii) the ability to condition decisions on rich context. We adopt the LinUCB algorithm [10] as our decision agent: its linear value model matches the low-dimensional, structured features available in IC3, and its updates are simple enough to be integrated into industrial-scale model checking runs. The novelty of this work therefore does not lie in modifying LinUCB itself, but in identifying a proof-aware context and reward design, and an integration architecture, that allow a contextual bandit to operate effectively inside the recursive IC3 generalization loop. This work makes the following contributions: – We formulate inductive generalization in IC3 as a contextual decision-making problem and propose A-IC33 , the first learning-based adaptive controller for generalization strategy selection in IC3. – We design a proof-aware context representation and a push-aware reward function that jointly capture the local difficulty of generalizing a CTI and the global progress of the proof, enabling a standard LinUCB agent to provide meaningful guidance with negligible overhead. – We integrate our controller into the state-of-the-art IC3 implementation, rIC3 [14], and evaluate the method on 914 benchmark instances from HWMCC. Our results show improvements in solved instances and PAR-2 scores over multiple baselines, demonstrating the practical benefit of learning-guided, context-aware generalization. By elevating inductive generalization from a static heuristic to an adaptive, learning-guided process, A-IC3 complements existing generalization techniques such as CTG/EXCTG and opens a new direction for integrating lightweight machine learning techniques into symbolic model checking. The remainder of this paper is organized as follows. Section 2 introduces the background of IC3 and the multi-armed bandit method. Section 3 presents the proposed A-IC3 framework and the proof-aware contextual bandit formulation. Section 4 reports our experimental results on rIC3 over the HWMCC’20, HWMCC’24 and HWMCC’25 benchmark suite. Section 5 discusses related work, and Section 6 concludes the paper. 3
Upon acceptance, we will open-source our implementation.
4
X. Zhou and G. Hu et al.
2
Preliminaries
2.1
Transition Systems and IC3/PDR
We model a hardware system as a Boolean transition system ⟨V, T (V, V ′ ), I(V )⟩, where V is a finite set of state variables, V ′ denotes the corresponding next-state variables, I(V ) characterizes the initial states, and T (V, V ′ ) is the transition relation. A literal l is a variable v ∈ V or its negation ¬v. A clause c is a disjunction of literals, and its negation is a cube s, representing a conjunction of literals. We write P (V ) for the safety property to be verified; states violating P are called unsafe.
Algorithm 1 The IC3 Algorithm (A simplified version with details omitted) 1: Input: Transition function T , initial states I, property P 2: Output: The proving result of P 3: Initialize frames Fi for i ≥ 0 such that F0 = I, k ← 1 4: a ← GENERALIZATION_STRATEGY 5: while True do 6: while SAT(Fk ∧ ¬P ) do 7: s ← GetModel() 8: if ¬ Block(s, k, a) then 9: return UNSAFE 10: for 1 ≤ i < k do 11: if Propagate(Fi , Fi+1 ) = CONVERGED then 12: return SAFE 13: k ←k+1 14: procedure Block(s, k, a) 15: if k = 0 then 16: return False ▷ Find a trace to unsafe 17: while SAT(Fk ∧ ¬s ∧ T ∧ s′ ) do 18: sp ←GetModel() 19: if ¬ Block(sp , k − 1, a) then 20: return False ▷ Failed to block on frame k 21: c ← Generalize(s, a) 22: Fi ← Fi ∧ c for 1 ≤ i ≤ k 23: return True
IC3/PDR [4,5] decides whether unsafe states are reachable by constructing an inductive invariant INV (V ) that satisfies: I(V ) → INV (V ), INV (V ) ∧ T (V, V ′ ) → INV (V ′ ),
(1)
INV (V ) → P (V ). If such an INV exists, it over-approximates the set of reachable states while excluding all unsafe states, thereby proving safety.
Title Suppressed Due to Excessive Length
5
In the implementation of IC3, it maintains a sequence of frames F0 , F1 , . . . , FN , where each frame Fi is a conjunction of clauses: Fi = c1 ∧ c2 ∧ · · · ∧ cni . F0 is initialized to I(V ), and the frames satisfy: F0 (V ) → I(V ), Fi (V ) → Fi+1 (V )
for all i < N,
′
Fi (V ) ∧ T (V, V ) → Fi+1 (V ′ ) Fi (V ) → P (V )
for all i < N,
(2)
for all i.
Intuitively, Fi over-approximates the set of states reachable from I in at most i steps, and the sequence becomes progressively less restrictive, i.e., F0 ⇒ F1 ⇒ · · · ⇒ FN . When two adjacent frames coincide, Fk ≡ Fk+1 , the conjunction Fk is an inductive invariant that satisfies (1), and the property is proved. Algorithm 1 presents the pseudocode of the IC3 procedure. At a high level, IC3 iteratively searches for counterexamples and refines the frames by learning clauses. Block: given a candidate bad predecessor, IC3 derives a generalized clause to exclude it and adds the clause to the corresponding frame(s). Propagate: IC3 then pushes learned clauses to higher frames whenever possible, which accelerates convergence. If a SAT query discovers a state s that reaches an unsafe state within i steps while s |= Fi , s is a CTI at frame Fi . IC3 then tries to block s by finding a clause c such that c excludes s, is inductive relative to Fi−1 , and can be pushed forward to higher frames. This blocking step is performed recursively on predecessor states and generates proof obligations (cubes) that must be blocked at lower frames. Figure 2 illustrates the IC3 frame structure together with the local (CTI-related) and global (frame-related) quantities introduced above. These quantities will later serve as the building blocks of our proof-aware context vector in Section 3. 2.2
Inductive Generalization and CTG-Based Methods
The clause used to block a CTI is typically obtained by generalizing the CTI cube s with respect to the current frame. Generalization seeks to drop literals from s while preserving inductiveness relative to Fi−1 . The resulting clause determines how many states are blocked and how easily it can be propagated to higher frames. Two failure modes are well known in the IC3 literature [6]: – Over-generalization: dropping too many literals yields a strong clause that is not valid at higher frames and therefore cannot be pushed, inflating the queue of proof obligations that must be blocked. – Under-generalization: keeping too many literals yields a very weak clause that blocks only a tiny neighbourhood of the CTI, resulting in many similar CTIs and slow convergence.
6
X. Zhou and G. Hu et al.
CtgDown [6] improves generalization by introducing CTGs: when a literal dropping attempt fails, the model returned by the SAT solver is treated as a CTG whose predecessors are explored to search for more general clauses. EXCTG [15] further strengthens this idea by exploring CTGs recursively and carefully tuning the recursion depth, the number of CTGs considered, and the number of literaldropping attempts. These methods demonstrate that better generalization—in terms of both width (states blocked) and depth (frames reached)—can substantially accelerate IC3, but they still rely on fixed or manually tuned settings for these parameters. In this work, we build upon CTG-based generalization and treat the configuration of these parameters (e.g., recursion depth, CTG budget, literal-dropping effort) as a strategy whose strength varies from conservative to aggressive. Our goal is to adaptively select such strategies according to the current proof context, rather than use a single fixed configuration throughout the run. 2.3
Multi-Armed Bandits and LinUCB
The multi-armed bandit (MAB) problem models an agent that repeatedly chooses an arm a from a finite set A and receives a stochastic reward r. The objective is to maximize the cumulative reward (or equivalently, to minimize regret) by balancing exploration of different arms and exploitation of arms known to perform well. In contextual bandits, the agent additionally observes a feature vector xt at each round t, representing the current context, and selects an arm based on both the context and past observations. Among many contextual bandit algorithms, LinUCB (Linear Upper Confidence Bound) [10] assumes that the expected reward of each arm is a linear function of the context. For each arm a ∈ A, LinUCB maintains a parameter vector and a (regularized) covariance matrix, and selects arms using an upperconfidence-bound rule that trades off estimated reward and uncertainty. Its perround update cost is low and depends only on the dimension of the context vector, making it attractive for settings such as IC3, where decisions are made extremely frequently, and overhead must be tightly controlled. In A-IC3, we instantiate the contextual bandit with LinUCB and view each generalization configuration as an arm. The formal bandit formulation, the design of the proof-aware context vector, and the LinUCB integration into IC3’s blocking loop are given in Section 3.
3
Method
3.1
Overview of A-IC3
Current IC3 implementations face a fundamental limitation in generalization strategy selection: fixed strategies cannot adapt to the highly dynamic nature of proof contexts. This rigidity leads to systematic inefficiencies—over-generalization wastes computational resources on unpushable clauses, while under-generalization
Title Suppressed Due to Excessive Length Arm1 Arm2 Arm3 Arm4 Step 1
0.2
0.5
Decision-making in Inductive Generalization Update Solving Progress
Agent
0.4
1.6
7
Context
𝒂(𝟏)
PA-LinUCB
Step 2
1.5
Step 3
2.4
Step 4
3.1
3.7
1.4
5.3
𝒂(𝟐) 4.2
2.6
3.2
𝐺𝑒𝑛𝑒𝑟𝑎𝑙𝑖𝑧𝑒 𝑐𝑙𝑎𝑢𝑠𝑒
𝒂(𝟑) 1.5
Local feature Global feature
Best Arm
0.8
4.1
𝒂(𝟒) Generalization strengthening
𝐹𝑖−1 ∧ 𝑇 ∧ 𝑠 ′ ∧ ¬𝑠 ? 𝑈𝑁𝑆𝐴𝑇
Add to Frame Proof strengthened
Sanity check
Hardware Model Checker
Fig. 1: Overview of A-IC3.
fails to discover sufficiently broad blocking clauses, severely hindering proof convergence. A-IC3 overcomes this limitation by treating generalization strategy selection as a contextual multi-armed bandit problem, as illustrated in Figure 1. The left side of the figure demonstrates the multi-armed bandit framework in action: at each step, our PA-LinUCB agent, which is inspired by LinUCB [10] and tailored for the environment of the IC3 algorithm observes the current proof context and selects among different generalization strategies (represented as arms with varying reward values). The agent continuously learns from the outcomes—for instance, in Step 1, Arm3 with the best score 1.6 is selected and marked with a(1) , the corresponding strategy will be used in the next generalization in the IC3-based hardware model checker. In the next step, similarly, after the agent is updated, we observe that Arm4 achieves the highest score of 5.3, indicating that it will be better to use a more aggressive generalization. The Arm4 is then selected and marked with a(2) . The agent will progressively refine selections that select different arms in subsequent steps according to the solving progress. The right side of Figure 1 shows our decision-making pipeline for inductive generalization. The agent leverages both local and global features from the solving progress context to make informed strategy selections. Each generalization strategy is encoded as a bandit arm, collectively orchestrated by our PA-LinUCB agent that adapts its choices based on real-time verification context inside the hardware model checker. Following each generalization-and-propagation iteration, the agent evaluates the quality of the generated clause through internal metrics of IC3 and computes a reward based on this evaluation. This feedback enables adaptive learning over time, allowing the agent to refine its strategy selection policy in response to evolving proof dynamics, as demonstrated by the iterative improvement in arm selection across the four steps shown in Figure 1.
8
3.2
X. Zhou and G. Hu et al.
Contextual MAB formulation
As stated earlier, we formulate the generalization strategy selection problem as a contextual MAB problem with the context from IC3. In order for the agent to make informed selections, we need to convey the real-time statistical proving information to the agent. This information is encoded as a context vector. In this setting, at the t-th call of the generalization procedure, we provide the agent with a context vector xt ∈ Rd that encodes the current state of the IC3 proof process, selects an arm (strategy) at from a finite set of arms {a1 , a2 , . . . , aK }, and receives a reward rt based on the effectiveness of the chosen strategy on generalization.
F0
F1
v1, v2, v7, v10
F2
CTI depth = 3 Cube size = 4 Activity score = 0.85 PO queue length = 2
Frame level = 2 Frontier frame level = 4 Frame saturation = 4
Local Features
Global Features
¬P F3
F4
v1, v2, v3 v1, v4, ¬v5, ¬v6 v2, v7 v8, ¬v9 2
F
Successor CTI Predecessor CTI CTI
Fig. 2: Context vector extraction from IC3 proof state. The figure illustrates IC3’s frame structure where each frame Fi contains clauses (e.g., “v1, v2, v3” represents one clause) that over-approximate reachable states at step i. The purple circle represents a CTI at frame F2 with cube content v1 , v2 , v7 , v10 . The arrows show predecessor-successor relationships. The context vector combines local features (CTI depth, cube size, activity score) with global features (frame levels, frame saturation, proof obligation queue length) to guide MAB strategy selection. Context Vector Design. The context vector xt ∈ Rd encodes the current proof state through carefully selected features. Figure 2 shows how A-IC3 extracts context before the generalization procedure. This context design balances local proof characteristics with global progression indicators (indicated by “local features” and “global features” in Figure 2), incorporating both absolute metrics (for global positioning) and relative metrics (for adaptive scaling). The local context component captures information that is directly tied to the current CTI and its immediate blocking workload, including the depth, cube size, activity score, and the PO-queue length when the CTI is encountered. The activity score, defined in [15], is a normalized measure of how frequently the CTI under generalization is encountered during proof search; we denote it as x̂a .
Title Suppressed Due to Excessive Length
9
The cube size is the number of literals in the cube to be generalized. The depth is the recursion depth of the Block call stack (Algorithm 1) at which the CTI is discovered. The PO-queue length indicates how many proof obligations are pending alongside the current CTI, reflecting the local blocking pressure at the moment of generalization. Together, these features characterize the difficulty of handling the current CTI. For example, a shallow CTI with a high activity score often suggests a complex and still-uncovered predecessor region, where a strategy with more generalization effort may be beneficial. In Figure 2, when blocking the purple CTI on frame F2 (cube size = 4), the proof-obligation queue already contains two successor obligations from higher frames F3 and F4 , indicating a PO-queue length of 2. Moreover, the current CTI is three transitions away from the bad states ¬P , so the Block call-stack depth is 3. For normalization, we scale the depth by the relative frame index with respect to the frame where the PO queue is established, denoted as x̂d , normalize the cube size by the running average cube size observed so far, denoted as x̂c , and normalize the PO-queue length by its maximum observed value, denoted as x̂q . The global context component summarizes the overall proof progress, including the current frame level, the frontier frame level, the frame saturation, and the growth rate of the PO queue. We define frame saturation as the number of clauses in the current frame (later normalized for learning). In Figure 2, we generalize a CTI at frame F2 , the frontier is F4 , and frame F2 contains 4 clauses; thus the corresponding global features are: current frame level = 2, frontier level = 4, and (raw) frame saturation = 4. The growth rate of the PO queue reflects the recent global trend of the search: whether proof obligations are being discharged effectively (queue shrinking) or accumulating (queue growing). For normalization, we represent the current frame level as a ratio to the frontier, denoted as x̂cf , normalize frame saturation by dividing it by 100, denoted as x̂s , and normalize the PO-queue growth rate by its maximum observed value, denoted as x̂qr . In summary, we define the context vector xt ∈ R7 of A-IC3 at time t as xt = [x̂d , x̂c , x̂q , x̂cf , x̂s , x̂qr , b], we set b = 1.0. Such a multi-faceted representation enables the MAB agent to distinguish between scenarios favoring aggressive versus conservative generalization. The level-related information can inform the agent of a rough progress of proving, and frame saturation indicates whether the current frame is overloaded by clauses, in which case the frame will be difficult to accept strong clauses. A long proof obligation queue or a rapid increase in its length may indicate a backlog of unresolved proof obligations. In such cases, adopting a more aggressive generalization strategy can help reduce the generation of new CTIs and CTGs. A higher saturation level means that the frame is highly restricted, possibly requiring the agent to pick up a strategy with less effort to prevent computational effort. It should be noted that, to better fuse the IC3 context information into the MAB agent, we perform normalization before loading the components into the context vector, and a bias term b for flexibility is attached at the end.
10
X. Zhou and G. Hu et al.
Strategic Arm Configuration. Our framework employs a spectrum of generalization strategies that differ in the aggressiveness of searching for clauses, including Basic, Conservative, Balanced, and Aggressive. These strategies are built upon the CtgDown generalization approach [6]. Each strategy controls the intensity of the generalization process through different configurations of CTG attempt counts, recursion depths, and literal-dropping constraints. The four strategic arms employ progressively more aggressive parameter configurations: – Basic is selected for low-activity proof obligations at constrained frames where minimal generalization is preferred. It disables CTG exploration entirely (setting attempt count and recursion depth to 0) while allowing extensive literal dropping trials to avoid wasting computation on simple cases. – Conservative applies cautious exploration suitable for early proof stages. It uses limited CTG attempts (1-3 attempts) with shallow recursion depths (1-2 levels) while permitting substantial literal dropping trials to balance exploration with efficiency. – Balanced represents standard generalization for typical verification scenarios. It employs moderate CTG attempts (1-5 attempts) with expanded recursion depths (1-4 levels) and generous literal dropping allowances for comprehensive but controlled exploration. – Aggressive enables extensive exploration for high-activity proof obligations at advanced frames, utilizing substantial CTG attempts (2-4 attempts) with deep recursion levels (up to 8 levels), while maintaining flexible literal dropping policies to maximize generalization potential. These tiered configurations enable adaptive generalization across diverse verification contexts, allowing the framework to dynamically find the strategy of appropriate exploration depth and width based on the proof obligation and the global environment of IC3 proving. Note that the ranges above describe the overall strategy design space; in A-IC3, we discretize this space into a finite set of arms by instantiating each conservative/balanced/aggressive family with concrete settings. 3.3
PA-LinUCB Algorithm for Strategy Selection
As discussed in Section 3.1, we develop PA-LinUCB (Proof-Aware LinUCB) as our decision agent, specifically tailored for IC3’s generalization context. Unlike standard LinUCB applications, PA-LinUCB deeply integrates with IC3’s proof structure, leveraging proof-specific contextual information to guide generalization strategy selection. This integration enables the agent to understand the dynamic proof environment and adapt its decisions based on the current proof state, frame structure, and clause characteristics. PA-LinUCB maintains a linear model for each generalization strategy, assuming that the expected reward can be expressed as a linear combination of proof-aware features. This assumption aligns well with IC3’s structured proof
Title Suppressed Due to Excessive Length
11
Algorithm 2 MAB-based IC3 generalization 1: Global: MAB agent A, Frames {Fi }, Time stamp t. 2: Initialize: A.Aai = I, A.bai = 0 for 1 ≤ i ≤ K, t = 1. 3: procedure Block(s, k) 4: if k = 0 then 5: return False ▷ Find a trace to unsafe 6: while SAT(Fk ∧ ¬s ∧ T ∧ s′ ) do 7: sp ←GetModel() 8: if ¬ Block(sp , k − 1) then 9: return False ▷ Failed to block on frame k 10: xt ← ExtractContext(s, {Fi }) ▷ Context extraction 11: at ← A.SelectArm(xt ) ▷ PA-LinUCB selection 12: c ← Generalize(s, at ) 13: pushed_frame ← PushClause(c, k) ▷ Intermediate push 14: rt ← ComputeReward(c, pushed_frame, {Fi }) 15: A.UpdateArm(at , xt , rt ) ▷ LinUCB update 16: return True
process, where generalization effectiveness often correlates linearly with specific proof characteristics such as clause size, frame depth, and propagation potential according to our observations. At each generalization step, PA-LinUCB computes the upper confidence bound for each strategy a: q PA-LinUCBa (xt ) = θ Ta xt + α xTt A−1 (3) a xt where xt represents the proof-aware context vector extracted from the current IC3 state, θ a captures the strategy’s learned parameters, Aa denotes the regularized covariance matrix associated with strategy a, and α controls the exploration level. The strategy with the highest score is selected as: at = arg max PA-LinUCBa (xt ) a∈A
(4)
After observing the generalization result, PA-LinUCB updates the selected strategy’s parameters to incorporate the proof-specific feedback: Aat ← Aat + xt xTt
(5)
bat ← bat + rt xt
(6)
θ at ← A−1 at bat
(7)
The reward rt captures both immediate generalization effects and long-term proof progress, enabling PA-LinUCB to learn from IC3’s complex feedback signals. The design of the reward rt will be discussed in detail in Section 3.4. bat is the weighted reward vector after performing the action at , and is derived via scaling rt by their corresponding context vectors.
12
X. Zhou and G. Hu et al.
Algorithm 2 presents the deep integration of PA-LinUCB with IC3’s blocking procedure. The key innovation is around lines 10-15, where proof-aware context extraction (Line 10), strategy selection (Line 11), and parameter updates (Line 15) are seamlessly embedded within IC3’s core block and generalization process. An intermediate push is conducted via the function PushClause, pushing the generalized clause into higher frames during the block of the current frame, in order to derive the effect of the generalized clause (Line 13). This tight integration ensures that PA-LinUCB operates with full awareness of IC3’s proof state and can adapt its strategy selection based on the evolving proof context. 3.4
Reward Function Design
The reward function serves as the critical feedback mechanism that guides our MAB agent toward effective generalization strategies. As introduced in earlier sections, fixed-strategy generalization often results in over-generalization and under-generalization. Our design explicitly addresses this generalization strength balancing problem in the reward calculation part. A-IC3 uses a multi-component reward structure. We decompose the reward into the following complementary components that capture different aspects of generalization quality. – Size reduction quality Rs directly reflects the clause simplification effectiveness, indicating the ability of state refinement of the generalized clause. It is calculated as the proportion of clause size reduction relative to the original size. If the size increases after generalization, we pose a penalty factor β > 1. – Push quality Rp evaluates the propagation success of clause. It is calculated in two conditions: if the clause is pushed to higher frames successfully, Rp equals the ratio of the push distance and the maximum possible push distance (the distance between the frame of proof obligation and the frontier frame); If the clause cannot be pushed to another frame at all, we set a constant penalty to Rp = pp . – Bonus Rb highlights extreme outcomes of a generalization step in a reward signal (e.g., a clause reaches the frontier or exhibits over-generalization). The bonus helps the agent react quickly by discouraging consistently unproductive arms and reinforcing promising ones. Each event has a polarity si ∈ {+1, −1} (bonus/penalty) and an importance level ℓ(i) ∈ {H, M, L}. We use qualitative magnitudes satisfying γH > γM > γL > 0 and define X Rb = si γℓ(i) I[Ei ], (8) i
where I[Ei ] ∈ {0, 1} indicates whether event Ei is triggered. The events are summarized in Table 1. When multiple events are triggered, their contributions are accumulated. We set Efront to High because pushing a clause to the current frontier is a decisive success signal: such a clause does not hinder subsequent clause propagation toward the proof frontier, and it can effectively constrain the
Title Suppressed Due to Excessive Length
13
Table 1: Events used in the bonus term Rb . Tag Event si ℓ(i) Efront Frontier push: Clause is pushed to frame Fk . +1 High Esize1 Complete generalization: clause size is 1 (one literal). +1 Medium Ehigh High-level push: the clause is pushed to a frame k′ > 0.7k +1 Low (where k is the frontier frame). Eideal Ideal generalization: Rs > 0.5 and Rp > 0.3. +1 Medium Eover Over-generalization: Rs > 0.7 and Rp < 0.1. −1 Medium
state space by strengthening the reachable frames. We set Esize1 to Medium since a size-1 clause is often very strong, yet aggressive size reduction may occasionally introduce over-generalization and lead to adverse effects, so we avoid over-rewarding this signal. We treat Ehigh as a weaker variant of Efront : pushing to a relatively high frame indicates progress but is less conclusive and occurs more frequently than reaching the frontier, hence it receives a Low importance. We set Eideal to Medium because it captures a well-balanced outcome: the generalization produces a clause that is both strong and sufficiently pushable, even if it is not the most extreme along either dimension. Empirically, repeatedly triggering Eideal indicates that the selected arm constitutes a consistently feasible and effective strategy under the current proving context, and thus deserves a moderate importance weight. Eover captures over-generalization: although the derived clause is strong, it is barely pushable to higher frames. This outcome suggests that the current strategy is mismatched to the present proving context. Finally, we can derive the overall reward, where ws and wp are weights for balancing the size reduction and push quality: rt = ws Rs + wp Rp + Rb .
4
Evaluation
4.1
Experimental Setup
(9)
All experiments were conducted on a high-performance computing cluster consisting of twenty nodes. Each node is equipped with 64 CPU cores, specifically Intel Xeon Gold 6338 CPUs operating at 2.00GHz. The system runs Red Hat Enterprise Linux Server version 7.9 and provides 1007GB of memory per node. Each invocation of the model checker was executed with one dedicated CPU and memory resources allocated by the scheduler to ensure consistency and reproducibility. The model checker is executed in a single thread, and no portfolio is included. The weights ws and wp in Equation 9 are set to 0.65 and 0.35, respectively. We emphasize more on the size reduction term here because bonuses in Table 1 consider more on push quality. The qualitative magnitudes used in the bonus term are set to: γH = 0.4, γM = 0.2, and γL = 0.1. The exploration
14
X. Zhou and G. Hu et al.
level α = 1.0. The penalty factor in size reduction is β = 1.5. The penalty in push quality pp = 0.1. All reward- and bandit-related hyperparameters are fixed globally across the entire benchmark suite to keep a consistent reward scale. The benchmark suite comprises a total of 914 model checking problems. These include instances from HWMCC’20, HWMCC’24, and HWMCC’25 [2,13,12]. To demonstrate the generality of the proposed method, experiments were conducted using rIC3 [14] (v1.3.6). rIC3 is the champion of both bit-level track and word-level track: bit-vectors in HWMCC’24 and HWMCC’25 [3,13]. The baselines in our experiments are the default rIC3 setting (denoted as rIC3-Standard), the rIC3 implementation of CtgDown [6] (denoted as rIC3CtgDown), and the rIC3 DynAMic setting [15] (denoted as rIC3-DynAMic). The PA-LinUCB implementation utilizes the Rust crate nalgebra for linear algebra operations, ensuring efficient matrix computations across both platforms. The timeout limit for each model checking problem is 3600 seconds in wall-clock time. 4.2
MAB Configuration
The configuration of the A-IC3 is derived from extensions of the rIC3-DynAMic strategy. Arm Design. An arm instantiates a concrete setting of three CTG-related parameters: ctgMax (maximum CTG attempts), ctgDepth (CTG recursion depth), and exctgBudget (number of EXCTG block operations). We use one basic static arm, three static arms with fixed settings, and three activity-aware dynamic arms. Our dynamic arms are extended from the activity-based parameterization in DynAMic [15]: We keep the same piecewise structure, use the original mapping as the balanced dynamic arm, and add two variants. (aggressive/conservative) by lowering/raising the activity thresholds and adjusting the scaling factors. Table 2 summarizes all arms used in our experiments.
Table 2: Arms configurations for A-IC3 and baselines.
Configuration Arm Type ctgMax ctgDepth exctgBudget Basic static 0 0 0 Conservative static 1 3 1 Balanced static 2 5 1 A-IC3 (Ours) Aggressive static 8 4 1 Conservative dynamic fcons (a) (Equation 12) Balanced dynamic fbala (a) (Equation 10) Aggressive dynamic faggr (a) (Equation 11) rIC3-Standard — static 0 0 0 rIC3-CtgDown — static 1 3 0 rIC3-DynAMic — dynamic fbala (a) (Equation 10)
Dynamic arms. Following DynAMic [15], an activity score a is used to characterize the difficulty of blocking the current CTI (higher a indicates that
Title Suppressed Due to Excessive Length
15
stronger generalization is needed). Based on a, DynAMic [15] defines an activityaware mapping to produce (ctgMax, ctgDepth, exctgBudget); we adopt this mapping as our balanced dynamic arm. In addition, we introduce aggressive and conservative variants that keep the same three-regime (low/medium/high activity) form, but use lower/higher thresholds and scaling to encourage/discourage stronger generalization, respectively: a < 10, (0, 0, 0), fbala (a) = (⌊(a − 10)/10⌋ + 2, 1, 1), (10) 10 ≤ a < 40, 0.3 (5, 1, round((a − 40) · 2 + 5)), a ≥ 40, a < 5, (1, 1, 1), faggr (a) = (⌊(a − 5)/8⌋ + 3, 1, 2), (11) 5 ≤ a < 25, 0.3 (6, 1, round((a − 25) · 2.5 + 6)), a ≥ 25, a < 15, (0, 0, 0), fcons (a) = (min(⌊(a − 15)/12⌋ + 1, 3), 0, 1), 15 ≤ a < 50, (12) (3, 1, min(round((a − 50)0.3 · 1.5 + 4), 6)), a ≥ 50. 4.3
Results
Table 3: Summary of results. Configuration #Solved Safe Unsafe ∆ ∆s ∆u PAR-2 PAR-2† Average† rIC3-Standard 603 464 139 0 0 0 2541.05 5214.20 2953.17 rIC3-CtgDown 629 478 151 +26 +14 +12 2336.71 4794.40 2848.64 rIC3-DynAMic 627 479 148 +24 +15 +9 2346.48 4815.32 2783.76 A-IC3 (Ours) 653 499 154 +50 +35 +15 2151.76 4413.68 2755.06 † Calculated for non-trivial cases (cases unsolvable within 100 seconds).
Table 3 summarizes the experimental results on rIC3 model checker under four generalization configurations: rIC3-Standard, rIC3-CtgDown [6], rIC3DynAMic [15], and our A-IC3. The table reports the number of solved instances (#Solved), broken down into Safe and Unsafe, as well as the improvement over the baseline (∆, ∆s , ∆u ) for the whole benchmark suite. We also report PAR-2, and for non-trivial cases (instances not solvable within 100 seconds), the corresponding PAR-2† and average runtime† . The PAR-2 score is a commonly used metric in competitions. It is calculated as the average time taken to solve the instances, with the timeout cases counted as twice the time limit. A lower PAR-2 score indicates better performance. Overall, A-IC3 achieves the best performance: it solves 653 instances in total (+50 over Standard, with +35 Safe and +15 Unsafe), and it also yields the lowest PAR-2 and PAR-2† scores together with the lowest average runtime on non-trivial cases, outperforming both rIC3CtgDown and rIC3-DynAMic across all reported metrics.
16
X. Zhou and G. Hu et al.
Notably, A-IC3 yields a more pronounced improvement on Safe instances than the other two IC3 variants, suggesting that our method can better incorporate the proving context to guide generalization and thus accelerate convergence on safety proofs. In particular, considering that rIC3 was the champion of the latest HWMCC [3,13], the fact that our method can deliver further improvements is especially noteworthy. Figure 3 illustrates the performance comparison on the benchmark suite when running rIC3 with and without MAB. We observe a cluster of instances in the green region. These cases are effectively intractable for the baseline configurations within the time limit, yet become solvable once MAB is enabled. This indicates that adaptively selecting a context-appropriate generalization strategy can unlock substantial speedups, sometimes by orders of magnitude, on originally hard instances. Meanwhile, on moderately hard cases where multiple strategies are already viable, A-IC3 closely tracks the baseline runtime, suggesting that the additional exploration introduced by MAB incurs little overhead in practice.
Safe/Proof Unsafe/CEX Unknown
103
A-IC3 CPU Time (s)
A-IC3 CPU Time (s)
A-IC3 CPU Time (s)
103
102
102
101
0 1010 0
Safe/Proof Unsafe/CEX Unknown
Safe/Proof Unsafe/CEX Unknown
103
102
101
101
102
rIC3-CtgDown CPU Time (s)
(a)
103
0 1010 0
101
101
102
rIC3-DynAMic CPU Time (s)
(b)
103
0 1010 0
101
102
rIC3-Standard CPU Time (s)
103
(c)
Fig. 3: Performance comparison of rIC3 with and without MAB: A-IC3 (with MAB) vs. non-MAB baselines. (a) A-IC3 vs. rIC3-CtgDown; (b) A-IC3 vs. rIC3DynAMic; (c) A-IC3 vs. rIC3-Standard. Green regions indicate hard instances where the baseline struggled, but A-IC3 achieved better results.
Figure 4 shows the number of cases solved over time. The MAB-enhanced method consistently dominates the other configurations across the entire time range. Beyond the final number of solved instances, the cactus curves also highlight how MAB improves the efficiency of proof construction. The MAB curve rises faster in the early and middle time budgets, indicating that it reduces time spent on unpromising generalization choices and reaches effective proof trajectories sooner. As the timeout threshold increases, the gap remains and even expands for harder instances, suggesting that adaptive strategy selection continues to pay off when the proof search becomes more sensitive to generalization quality. At the same time, the curve does not exhibit a noticeable slowdown on easier and moderately hard cases, which supports our claim that the exploration
Title Suppressed Due to Excessive Length
17
overhead is well controlled and does not negate the gains from selecting better strategies.
Number of Cases Solved
650 600 550 500 450 400
0
600
1200
1800
2400
Time Threshold (s)
rIC3-Standard rIC3-CtgDown rIC3-DynAMic rIC3-DynAMic-MAB 3000 3600
Fig. 4: Cactus plots comparing solver performance.
Figure 5 compares the termination level count (the index/number of frames when the solver terminates, either by reaching an inductive invariant or by finding a counterexample) of A-IC3 against the baselines. Marker × denotes instances where the MAB-enhanced solver performs worse than the baseline, while + denotes instances where it performs better. It can be observed that a higher termination level generally indicates poorer performance. Across all three comparisons in Figure 5, the overwhelming majority of points lie on or below the diagonal, and the level-count ratios are mostly below 1, indicating that MAB typically terminates at a lower level than the baselines, rather than improving only a small set of outliers. Since a lower convergence level in IC3 usually means fewer frames are needed to make the proof inductive or to expose a counterexample, this trend suggests that MAB accelerates solving by improving the proof trajectory itself. This observation also echoes our earlier claim that no single generalization heuristic is uniformly optimal: by adapting the strategy to the current proving context, MAB tends to derive clauses that are more “pushable” and better aligned with the proof frontier, which helps close the inductive gap earlier. Cases where MAB increases the termination level do exist, but they are relatively sparse and often close to the diagonal.
5
Related Work
Heuristic-Based Generalization. A key line of research focuses on heuristics for improving clause quality. The seminal CTG [6] method enhances generalization by blocking states that impede the process (CTGs). Its extension, EXCTG [15], further improves generalization by recursively blocking predecessors of CTGs. While effective, these methods rely on fixed or reactive heuristics (e.g., DynAMic in [15]), which may not adapt to the global proof state. A-IC3 is more proactive, using a richer context to anticipate the optimal strategy.
18
X. Zhou and G. Hu et al.
104
104
Better performance Worse performance Equal performance
103
A-IC3 Level Count
102
102
101
101
101
100
Worse Better 10 2
102
103
rIC3-CtgDown Level Count
10 1
100
101
102
Level count ratio (A-IC3 / rIC3-CtgDown)
(a)
104
103
100
Better performance Worse performance Equal performance
103
A-IC3 Level Count
A-IC3 Level Count
103
102
100
104
Better performance Worse performance Equal performance
101
101
100
Worse Better 10 2
102
103
rIC3-DynAMic Level Count
10 1
100
101
102
Level count ratio (A-IC3 / rIC3-DynAMic)
(b)
104
103
100
101
100
Worse Better 10 2
102
103
rIC3-Standard Level Count
10 1
100
101
102
Level count ratio (A-IC3 / rIC3-Standard)
104
103
(c)
Fig. 5: Comparison of the termination level count. (a) A-IC3 vs. rIC3-CtgDown; (b) A-IC3 vs. rIC3-DynAMic; (c) A-IC3 vs. rIC3-Standard.
Global Guidance in Model Checking. Another direction complements local generalization with global guidance. GSPACER [16] uses theory-agnostic rules (Subsume, Concretize, Conjecture) to steer the search based on the global set of lemmas, mitigating issues like myopic generalization. GSPACER-BV [17] extends this to bit-vectors, using global guidance as a substitute for unavailable interpolation methods. These works focus on what to generalize. In contrast, A-IC3 is orthogonal and focuses on how to generalize by adaptively selecting the best procedure. Data-Driven and Learning-Based Approaches. Machine learning has also been applied to guide generalization. ROPEY [9] uses a recurrent network to predict which literals to keep, while NeuroPDR [8] and DeepIC3 [7] employ Graph Neural Networks (GNNs) to predict effective clauses from the circuit structure. Although powerful, these supervised methods require extensive offline training and can introduce significant runtime overhead. A-IC3 sidesteps these issues with an MAB formulation that learns online with minimal overhead and no pre-existing data. It acts as a lightweight, adaptive control layer, making it more dynamic than fixed heuristics and more practical for hardware model checking than heavyweight deep learning approaches.
6
Conclusion
In this work, we presented a lightweight, learning-guided framework for adaptive generalization in IC3. By modeling strategy selection as a contextual multiarmed bandit problem, our method dynamically adjusts generalization to the proof context, overcoming static heuristic limitations. Experiments demonstrated improvements over baseline strategies on extensive benchmarks. These results highlight the potential of integrating machine learning into formal verification for more efficient model checking. Future work includes deeper integration with other verification phases and advanced reinforcement learning methods.
Title Suppressed Due to Excessive Length
19
References 1. Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds. In: Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361). pp. 317–320 (1999). https://doi.org/10.1109/ DAC.1999.781333 2. Biere, A., Froleyks, N., Preiner, M.: HWMCC’20 Benchmarks (2020), https: //fmv.jku.at/hwmcc20/hwmcc20benchmarks.tar.xz, benchmark archive for the Hardware Model Checking Competition 2020 (BTOR2 and bit-blasted AIGER formats) 3. Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: 2024 Formal Methods in Computer-Aided Design (FMCAD). pp. 1–1 (2024). https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_6 4. Bradley, A.R.: Sat-based model checking without unrolling. In: International Workshop on Verification, Model Checking, and Abstract Interpretation. pp. 70–87. Springer (2011) 5. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: 2011 Formal Methods in Computer-Aided Design (FMCAD). pp. 125–134 (2011) 6. Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in ic3. In: 2013 Formal Methods in Computer-Aided Design. pp. 157–164 (2013). https://doi.org/10. 1109/FMCAD.2013.6679405 7. Hu, G., Tang, J., Yu, C., Zhang, W., Zhang, H.: Deepic3: Guiding ic3 algorithms by graph neural network clause prediction. In: 2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC). pp. 262–268 (2024). https://doi. org/10.1109/ASP-DAC58780.2024.10473807 8. Hu, G., Zhang, W., Zhang, H.: Neuropdr: Integrating neural networks in the pdr algorithm for hardware model checking. In: 2023 ACM/IEEE 5th Workshop on Machine Learning for CAD (MLCAD). pp. 1–6 (2023). https://doi.org/10.1109/ MLCAD58807.2023.10299875 9. Le, N., Si, X., Gurfinkel, A.: Data-driven optimization of inductive generalization. In: FMCAD. pp. 86–95 (2021) 10. Li, L., Chu, W., Langford, J., Schapire, R.E.: A contextual-bandit approach to personalized news article recommendation. In: Proceedings of the 19th international conference on World wide web. pp. 661–670. ACM (2010) 11. McMillan, K.L.: Interpolation and sat-based model checking. In: Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings 15. pp. 1–13. Springer (2003) 12. Preiner, M., Froleyks, N., Biere, A.: Hwmcc’24 benchmarks and results. https: //doi.org/10.5281/zenodo.14156844, https://zenodo.org/records/14156844 13. Preiner, M., Froleyks, N., Biere, A.: HWMCC’25 Benchmarks and Results (2025). https://doi.org/10.5281/zenodo.17428464, https://zenodo.org/ records/17428464, dataset, version v1, published 2025-10-23 14. Su, Y., Yang, Q., Ci, Y., Bu, T., Huang, Z.: The ric3 hardware model checker (2025), https://arxiv.org/abs/2502.13605 15. Su, Y., Yang, Q., Ci, Y., Huang, Z.: Extended ctg generalization and dynamic adjustment of generalization strategies in ic3 (2025), https://arxiv.org/abs/ 2501.02480 16. Vediramana Krishnan, H.G., Chen, Y., Shoham, S., Gurfinkel, A.: Global guidance for local generalization in model checking. Formal Methods in System Design 63(1), 81–109 (2024)
20
X. Zhou and G. Hu et al.
17. VK, H.G., Fedyukovich, G., Gurfinkel, A.: Word level property directed reachability. In: 2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD). pp. 1–9. IEEE (2020) 18. Winterer, F., Seufert, T., Scheibler, K., Teige, T., Scholl, C., Becker, B.: Icp and ic3 with stronger generalization. In: MBMV 2021; 24th Workshop. pp. 1–12. VDE (2021)