Machine-learning-based model checker performance prediction

doi:10.3969/j.issn.1000-5641.2024.04.002

Abstract

Abstract:

An and-inverter graph (AIG) is a representation of electrical circuits typically passed as input into a model checker. In this paper, we propose an AIG structural encoding that we use to extract the features of AIGs and construct a portfolio-based model checker called Liquid. The underlying concept of the proposed structural encoding is the enumeration of all possible AIG substructures, with the frequency of each substructure encoded as a feature vector for use in subsequent machine-learning processes. Because the performance of model-checking algorithms varies across different AIGs, Liquid combines multiple such algorithms and selects the algorithm appropriate for a given AIG via machine learning. In our experiments, Liquid outperformed all state-of-the-art model checkers in the portfolio, achieving a high prediction accuracy. We further studied the effectiveness of Liquid from several perspectives.

Key words: model checking, and-inverter graph, portfolio-based model checker

CLC Number:

TP311

Chengyu ZHANG, Jiayi ZHU, Yihao HUANG, Di YANG, Jianwen LI, Weikai MIAO, Di YAN, Bin GU, Naijun ZHAN, Geguang PU. Machine-learning-based model checker performance prediction[J]. Journal of East China Normal University(Natural Science), 2024, 2024(4): 18-29.

Figures/Tables 7

Fig.1

Fig.2

Fig.3

Fig.4

Table 1

Fig.5

Fig.6

References 34

1	林梦香, 吴国仕.. 程序模型检查器综述. 计算机软件及计算机应用, 2009, 36 (4): 12- 15.
2	CLARKE E M, EMERSON E A, SIFAKIS J.. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52 (11): 74- 84.
3	MCMILLAN K L. Interpolation and SAT-based model checking [C]// Computer Aided Verification, CAV 2003. 2003: 1-13.
4	GOEL A, SAKALLAH K. Empirical evaluation of IC3-based model checking techniques on Verilog RTL designs [C]// 2019 Design, Automation & Test in Europe Conference & Exhibition. 2019: 618-621.
5	BRAYTON R, MISHCHENKO A. ABC: An academic industrial-strength verification tool [C]// Proceedings of the 22nd International Conference on Computer Aided Verification. 2010: 24-40.
6	BIRER A, DIJK T V, HELJANKO K. Hardware model checking competition [C]// Proceedings of the 17th Formal Methods in Computer-Aided Design. 2017: 9.
7	CABODI G, PALENA M, PASINI P. Interpolation with guided refinement: Revisiting incrementality in sat-base unbounded model checking [C]// Proceedings of the 14th Formal Methods in Computer-Aided Design. 2014: 43-50.
8	LI J W, DUREJA R, PU G G, et al. SimpleCAR: An efficient bug-finding tool based on approximate reachability [C]// Proceedings of the 30th International Conference on Computer Aided Verification. 2018: 37-44.
9	HUBERMAN B A, LUKOSE R M, HOGG T.. An economics approach to hard computational problems. Science, 1997, 275 (5296): 51- 54.
10	XU L, HUTTER F, HOOS H H, et al. SATzilla: Portfolio-based algorithm selection for SAT [J]. Journal of Artificial Intelligence Research, 2008, 32: 565-606.
11	SAT Competition. The SAT 2007 Competition [R/OL]. [2023-03-04]. http://www.satcompetition.org/2007.
12	CABODI G, NOCCO S, QUER S.. Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods in System Design, 2011, 39 (2): 205- 227.
13	BIRER A. The AIGER and-inverter graph (AIG) format version 20071012 [R]. Linz, Austria: Johannes Kepler University, 2007.
14	HASSAN Z, BRADLEY A R, SOMENZI F. Incremental, inductive CTL model checking [C]// Proceedings of the 22nd International Conference on Computer Aided Verification. 2012: 532-547.
15	BRADLEY A R. SAT-based model checking without unrolling [C]// Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation. 2011: 70-87.
16	RICE J R.. The algorithm selection problem. Advances in Computers, 1976, 15, 65- 118.
17	KOTTHOFF L. Algorithm selection for combinatorial search problems: A survey [C]// Data Mining and Constraint Programming. 2016: 149-190.
18	HUTTER F, BABIC D, HOOS H H, et al. Boosting verification by automatic tuning of decision procedures [C]// Proceedings of the 7th Formal Methods in Computer-Aided Design. 2007: 27-34.
19	BALUNOVIC M, BIELIK P, VECHEV M. Learning to solve SMT [C]// Proceedings of the 32nd Conference on Neural Information Processing Systems. 2018: 10338-10349.
20	SCARSELLI F, GORI M, TSOI A C, et al. The graph neural network model [J]. IEEE Transactions on Neural Networks, 2008, 20(1): 61-80.
21	LI Y J, TARLOW D, BROCKSCHMIDT M, et al. Gated graph sequence neural networks [EB/OL]. (2017-09-22) [2023-06-20]. https://arxiv.org/pdf/1511.05493.pdf.
22	SHUAI B, ZOU Z, WANG B, et al. Gag-recurrent neural networks for scene labeling [C]// Proceedings of the Conference on Computer Vision and Pattern Recognition. 2016: 3620-3629.
23	AMIZADEH S, MATUSEVYCH S, WEIMER M. Learning to solve circuit-SAT: An unsupervised differentiable approach [C]// Proceedings of the 6th International Conference on Learning Representations. 2019: 1-14.
24	BRYANT R E.. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986, 100 (8): 677- 691.
25	BIERE A, CIMATTI A, CLARKE E, et al. Symbolic model checking without BDDs [C]// Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1999: 193-207.
26	EEN N, MISHCHENKO A, BRAYTON R. Efficient implementation of property directed reachability [C]// Proceedings of the 11th Formal Methods in Computer-Aided Design. 2011: 125-134.
27	VIZEL Y, GURFINKEL A. Interpolating property directed reachability [C]// Proceedings of the 26th International Conference on Computer Aided Verification. 2014: 260-276.
28	VIZEL Y, WEISSENBACHER G, MALIK S. Boolean satisfiability solvers and their applications in model checking [C]// Proceedings of the IEEE. 2015: 2021-2035.
29	BREIMAN L. Machine Learning [M]. Cambridge, Massachusetts: Massachusetts Institute of Technology Press, 2021.
30	LECUN Y, BENGIO Y, HINTON G. Deep learning [J]. Nature, 2015, 521(7553): 436-444.
31	PEDREGOSA F, VAROQUAUX G, GRAMFORT A, et al. Scikit-learn: Machine learning in Python [J]. Journal of Machine Learning Research, 2011, 12: 2825-2830.
32	MAATEN L V D, HINTON G. Visualizing data using t-SNE [J]. Journal of Machine Learning Research, 2008(9): 2579-2605.
33	BRUMMAYER R, BIERE A, LONSING F. BTOR: Bit-precise modelling of word-level problems for model checking [C]// Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. 2008: 33-38.
34	NIEMETZ A, PREINER M, WOLF C, et al. Btor2, btormc and boolector 3.0 [C]// Proceedings of the 30th International Conference on Computer Aided Verification. 2018: 587-595.

模型	准确度/%		${\Delta _{\rm{avg}}/{\rm{s}} }$
模型	top-1	top-2	top-1	top-2
0-深度编码	0.54	0.83	87.07	13.42
1-深度编码	0.55	0.84	78.89	15.70
2-深度编码	0.55	0.83	65.59	11.24
随机策略	0.26	0.52	450.67	108.98

[1]	Jie CHEN, Wenyi SHEN, Wenyu WU, Jiali MAO. Method for improving the quality of trajectory data for riding-map inference [J]. Journal of East China Normal University(Natural Science), 2023, 2023(6): 14-27.
[2]	Zhaoyang WU, Jiali MAO. Research on travel time prediction based on neural network [J]. Journal of East China Normal University(Natural Science), 2023, 2023(2): 106-118.
[3]	Yiming YU, Yuchen HONG, Ye WANG, Qiwen DONG. Design of experimental data governance module for chemical material formulation [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 1-13.
[4]	Jiling LI, Baolin LI, Songru YAN. Research on user behavior portrait and subject mining in the express logistics field during Coronavirus epidemic [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 100-114.
[5]	Xiao PAN, Dongna LU, Shuhai WANG. Capacitated route planning for supermarket distribution based on order splitting [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 147-164.
[6]	Xiaobian MIAO, Jiajun LIAO, Huajie MEI, Chong FENG, Jiali MAO. Truck capacity prediction based on self-attention mechanism in the bulk logistic industry [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 165-183.
[7]	Tao ZOU, Rongtao QIAN, Jiali MAO. Indexing and query technology for steel logistic data [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 195-207.
[8]	Qing SUN, Guanyu LIANG, Yanjun WU, Bin WU, Chunqi TIAN, Wei WANG. Data-driven open source software supply chain maintenance risk analysis method [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 90-99.
[9]	Xin GONG, Lihua XU, Liang DOU, Ruixiang ZHAO. Redundancy measurement and reduction of automated tests in financial technology [J]. Journal of East China Normal University(Natural Science), 2022, 2022(4): 43-55.
[10]	Ping YU, Huiqi HU, Weining QIAN. Research on multi-objective cargo allocation based on an improved genetic algorithm [J]. Journal of East China Normal University(Natural Science), 2021, 2021(5): 185-198.
[11]	Xiaoqin MA, Xiaohe GUO, Yufeng XUE, Lin YANG, Yuanzhe CHEN. Data augmentation technology for named entity recognition [J]. Journal of East China Normal University(Natural Science), 2021, 2021(5): 14-23.
[12]	JI Yu, HE Yi-xuan, WU Guo-qun, WU Min. On evaluation of Bessel functions of the first kind via Prony-like methods [J]. Journal of East China Normal University(Natural Sc, 2019, 2019(6): 42-60.
[13]	XIE Qing-cheng, MAO Jia-li, LIU Ting. Dynamic scheduling strategy for bicycle-sharing in cities [J]. Journal of East China Normal University(Natural Sc, 2019, 2019(6): 88-102.
[14]	SHEN Hang-jie, JU Sheng-gen, SUN Jie-ping. Performance prediction based on fuzzy clustering and support vector regression [J]. Journal of East China Normal University(Natural Sc, 2019, 2019(5): 66-73,84.
[15]	JIANG Qun, DAI Ge-nan, ZHANG Sen, GE You-ming, LIU Yu-bao. Optimal route search based on user preferences [J]. Journal of East China Normal University(Natural Sc, 2019, 2019(5): 100-112.