Research map / Learning theory and algorithms / Combinatorial and search optimization
Neural Model Checking
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes neural model checking: trains neural ranking functions as proof certificates for LTL hardware model checking from random simulation traces, then verifies them with quantised-network SMT encoding and Bitwuzla.
Problem
Hardware model checking of LTL specifications is computationally expensive with BDD and SAT-based symbolic methods, which often fail or time out on word-level arithmetic designs.
Approach
Represent fair-termination ranking functions for the product of the circuit and a Büchi automaton as small neural networks trained unsupervised on simulated executions, then formally check them with a quantised-network SMT encoding and one-step bounded model checking.
Key results
- Neural model checking completes 180 of 194 tasks versus 117 for nuXmv, 57 for ABC, and 156 for industry tool X.
- Under a 5-hour budget the method completes on average 60% more tasks than ABC, 34% more than nuXmv, and 11% more than the leading commercial tool.
- The method is faster than the academic tools on 67% of tasks and 10x faster on 34%; training succeeds on 93% of tasks, mostly within five minutes.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use neural ranking certificates with learning and SMT checking instead of conventional model checking | Neural model checking versus academic tools · 194 hardware verification tasks | completed tasks: 93% vs 29% (ABC); 93% vs 60% (nuXmv) | Helped |
| use neural ranking certificates with learning and SMT checking instead of the leading commercial model checker | Neural model checking versus Industry tool X · 194 hardware verification tasks | completed tasks: 93% vs 80% | Helped |
| use neural model checking rather than academic tools | Neural model checking · 194 hardware verification tasks | tasks completed faster: 67% of tasks; 10 times faster on 34%; 100 times faster on 4% | Helped |
| use the default (8, 5) hidden-layer configuration rather than (3, 2) (ablation) | Neural model checking · 194 hardware verification tasks | completed tasks: 25% -> 93% | Helped |
| use the default (8, 5) hidden-layer configuration rather than (5, 3) (ablation) | Neural model checking · 194 hardware verification tasks | completed tasks: 63% -> 93% | Helped |
| use the default (8, 5) hidden-layer configuration rather than (15, 8) (ablation) | Neural model checking · 194 hardware verification tasks | completed tasks: 74% -> 93% | Helped |
| use the default (8, 5) network instead of replacing element-wise multiplication with a fully connected layer (ablation) | Neural model checking · 194 hardware verification tasks | completed tasks: 24% -> 93% | Helped |
| use separate parameters per automaton state instead of a monolithic ranking function (ablation) | Neural model checking · 194 hardware verification tasks | completed tasks: 39% -> 93% | Helped |
| use the (3, 2) network rather than the default network on tasks it completes (ablation) | Neural model checking · completed tasks for the (3, 2) configuration | runtime: 57% | Mixed |
| use the (5, 3) network rather than the default network on tasks it completes (ablation) | Neural model checking · completed tasks for the (5, 3) configuration | runtime: 94% | Mixed |
| use the (5, 3) network rather than the (3, 2) network (ablation) | Neural model checking · tasks completed by the compared configurations | runtime: 56% | Mixed |
| use the default network rather than the (15, 8) network on tasks both complete (ablation) | Neural model checking · tasks completed by the (15, 8) configuration | runtime: 97% | Helped |
Surprising findings
- Verification via SMT takes most of the compute time, yet the approach still outperforms traditional symbolic checkers.
- Tiny networks with a few hidden neurons suffice; a larger network (15,8) is not uniformly better, and the monolithic variant fails on most tasks but succeeds on most VGA tasks.
Limitations
- Gradient descent can get trapped in local minima, failing to reach zero loss (e.g., VGA design).
- SMT checking times are long and dominate total runtime.
- Word-level numerical inputs limit applicability to bit-level netlists; slower on trivial designs like UARTt.
Experimental setup
Datasets: synthetic executions generated with Verilator from ten parameterised SystemVerilog hardware designs
Benchmarks: 194 hardware model checking tasks from ten parameterised SystemVerilog designs
Metrics: number of solved tasks runtime time-budget completion rate
Baselines: ABC nuXmv industry tool X industry tool Y
Builds on: ranking functions for fair termination Büchi automata bounded model checking Spot Verilator
Closest papers by meaning
- Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract) (AAAI 2025 · similarity 0.85)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.85)
- Certification from Examples is Hard for Circuits and Transformers under Minimal Overparametrization (NeurIPS 2026 · similarity 0.85)
- Neural Closure Certificates (AAAI 2024 · similarity 0.84)
- NN4SysBench: Characterizing Neural Network Verification for Computer Systems (NeurIPS 2024 · similarity 0.84)
- Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible (ICML 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.