Neural Model Checking

Summary

The paper introduces a novel approach to hardware model checking using neural networks as proof certificates for linear temporal logic (LTL) specifications. Traditional model checking in electronic design automation (EDA) relies on symbolic techniques like SAT solvers, which are computationally intensive. In contrast, the proposed method leverages machine learning to generate neural certificates from random system executions, which are then verified symbolically for validity. The neural network acts as a ranking function ensuring compliance with the LTL specification, trained on synthetic data. Experimental results demonstrate the method's scalability and efficiency, outperforming academic tools in completion time across diverse hardware designs in SystemVerilog, and performing competitively with leading commercial tools.

Strengths

- This approach enhance verification in complex hardware designs efficiently through unsupervised machine learning techniques integrated with symbolic reasoning. - The paper is well organized and well written.

Weaknesses

- The classic algorithm has a guarantee for the verification. I do not know how the use of deep neural network can still have such guarantee. - If we transform the problem to the SMT solver with same difficulty, it seems the SMT solver will still take a huge amount of time for verification.

Questions

Can the proposed method provide any formal guarantee over the evaluated program?

Rating

5

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

The author discussed the limitation of this work about the heavy reliance on the SMT solver and the extensibility of application to Computational Tree Logic.

Summary

This paper addresses the problem of hardware model checking with respect to LTL specifications. Although this a well-studied problem, hardware model checking can still suffer from scalability issues. A general automata-theoretic approach to model checking is to check if intersection of the formal languages corresponding to the system and to the complement of the specification is empty. One strategy for conducting this emptiness check is to construct a ranking function that can serve as an emptiness certificate. The main idea of the paper is to use neural networks to represent and learn these ranking functions. The functions are learned using traces of the system composed with the complement of the specification. It is then checked (using an SMT solver) if the learned function satisfies the required constraints of a ranking function. If not, the counterexamples are used to further train the function but if yes, then we have a proof that the system satisfies its spec. The proposed approach is evaluated on 9 hardware designs and with respect to 123 verification tasks. The presented approach outperforms state-of-the-art baselines on these verification tasks.

Strengths

The paper is largely well-written and, for the chosen benchmarks, the results are quite impressive. The use of neural networks to represent ranking functions has been proposed before (citation [44] in the paper), but the setting in the prior work in slightly different (termination analysis of programs in [44] vs model checking of hardware ciruits with respect to LTL specifications here). It is interesting to see that neural ranking functions can be effective in the setting of hardware model checking as well. It is particularly striking that the learned ranking function is frequently correct in the first attempt and does not need any further training.

Weaknesses

I have a number of concerns with the paper. 1. Given the prior work on neural termination analysis, I find the technical contribution to be quite incremental. The core of the technical approach is almost the same as in [44]. 2. While the empirical results are quite impressive, I wonder how the benchmarks were chosen. Why not choose the benchmarks from HWMCC'20? Also, why not compare against the best performing tool from HWMCC'20, i.e., AVR? Why set the time limit to 5 hours in particular? All these points make me a little concerned about the results. When is this approach not applicable? Can it be applied to all hardware model checking problems? Can it be applied to software model checking problems? 4. The paper may not be easily accessible to readers not familiar with formal methods. In particular, there are a number of approaches for model checking with respect to LTL functions and using ranking functions for the purpose is not that common. I could only find two citations [A,B]. The paper should at least include these citations if not more for the ranking function based LTL model checking approach. [A] Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., & Vardi, M. Y. (2007). Proving that programs eventually do something good. ACM SIGPLAN Notices, 42(1), 265-276. [B] Dietsch, D., Heizmann, M., Langenfeld, V., & Podelski, A. (2015). Fairness modulo theory: A new approach to LTL software model checking. In Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I 27 (pp. 49-66). Springer International Publishing. 5. I find the title to overclaim a bit. The paper focuses on hardware model checking but the title suggests that any model checking problem is within scope. Moreover, there might be other ways in which neural networks could be used to aid model checking. Is it a claim of the paper that the only way in which neural networks can aid model checking is as ranking functions? I also think that a formal methods conference might be a better fit for the paper.

Questions

In addition to the questions above, I have the following questions and comments: 1. What if system does not meet its specification? In that case, no ranking function would exist. Is the proposed approach able to handle such scenarios and generate counterexamples when the system violates it spec? 2. The paper frequently refers to word-level but it is never clarified what this means. 3. Fig 1 needs more description. It is a little mysterious at present. 4. Line 101: Is the language L_M defined over sequences of observed states of M or over sequences of atomic propositions about observed states of M. If it is the former, then the language inclusion does not make sense. 5. Line 106: "inputs and observables being equal to obs X" --> this is a little hard to follow 6. Line 161: "normalizes these inputs through element-wise multiplication ..." --> please expand a bit on this 7. Equation 4: The indicator function seems to be incorrectly used. Should the term "- 1_F(q)" instead be "- \epsilon. \neg 1_F(q)" 8. Line 226: Since there are only 9 designs and 123 verification tasks, are there multiple specs per design? 9. Line 238: "network is quantized and translated into SystemVerilog" --> please provide some more details about this 10. Figure 4: I am confused by the figure. How is the state space size and logic gate count different across the same design? 11. Line 288: "Of the 11 tasks that were not trained to zero loss, ..." --> Are these tasks considered as timed out? Are they plotted in Fig 5b? 12. Fig 5b: What are the tasks where x is almost 0 but y has large values? 13. Line 306: Why is different hardware used for experiments with the industrial tools? This makes the head-to-head comparison unfair.

Rating

5

Confidence

4

Soundness

3

Presentation

3

Contribution

2

Limitations

Yes, the paper includes a discussion about limitations. I do not see any potential negative societal impact of this work..

Summary

The paper presents a novel application of machine learning to hardware model checking. The model checking problem is given as a design written in SystemVerilog and a temporal logic property in linear-time temporal logic (LTL). Similar to many classical model checking approaches the authors first construct the synchronous composition of the system model and the negation of the LTL property. The model checking problem then corresponds to checking whether the composition is empty (under some fairness condition). This emptiness can be witnessed by a ranking function on the states of the synchronous composition. The authors propose to learn this ranking function by representing it as a neural network and training the neural network with trajectories sampled from the composition. After training, a symbolic ranking function is extracted from the neural network using post-training quantization and checked with an SMT solver to be valid. On a set of benchmarks from the literature the authors impressively demonstrate that their approach often outperforms state-of-the-art academic model checkers and is competitive with industrial-grade model checkers.

Strengths

- The model checking problem is a fundamental problem in formal verification and is of great importance in industry. The paper contributes a novel neuro-symbolic approach to this fundamental problem. To the best of my knowledge, it is the first successful application of neural networks to the LTL model checking problem. - With designs being expressed in a hardware description language and properties being expressed in LTL, the approach is evaluated similarly to a real-world workflow. - The prototype implementation is already competitive with established tools. The authors compare with nuXmv and ABC which are state-of-the-art solvers in academia and the result of many years of engineering and research. The prototype outperforms those tools on 7 out of 9 benchmarks. Impressively, the authors show that their prototype is also competitive with industrial-grade solvers. - The results are also interesting for its use of ranking functions in the hardware model checking problem.

Weaknesses

- When being familiar with the LTL model checking problem, Section 2 of the paper gives a helpful description of the problem. However, I expect it to be hard to follow for someone less familiar with the problem. - The approach requires some tuning when being applied to a specific problem instance (with respect to trajectory sampling and the neural network architecture). I assume that in the evaluation the academic and industrial tools didn’t need to be tuned to the instances. - The presented approach can only be used to establish that a system satisfies a formal guarantee but not a violation. Model checkers such as ABC and nuXmv establish both. This limitation is not immediately clear from the paper.

Questions

- In theory, the LTL model checking is decidable and has been extensively studied with respect to its computational complexity. Do you expect that any completeness or computational complexity results can be established for the presented approach? - I am confused about industry tool Y. It is reported even though it does not solve a single instance. Has industry tool Y been developed for these kinds of verification problems? - Do all benchmarks in the experimental evaluation include a fairness condition? - I do not understand the relationship that is drawn to reinforcement learning. How is the presented approach related? For example, what would be the MDP?

Rating

7

Confidence

4

Soundness

3

Presentation

3

Contribution

4

Limitations

- The paper is transparent about the SMT checks being a bottleneck of the approach. - The tuning of the approach to individual benchmarks could be discussed in more detail in the limitations section. - I agree with the authors that no negative societal impacts are expected.

Summary

This work incorporates neural networks into the model checking process. Specifically, it learns a neural ranking function on random trajectories of the formal model. The ranking function first achieves zero loss on the training set and then is verified for soundness symbolically using SMT solvers. Evaluated on nine different hardware designs, the proposed approach shows significant improvement over prior works.

Strengths

The paper is easy-to-follow with illustrative examples and well motivated. The domain of hardware verification is very important. Moreover, the approach not only provides significant benefits as demonstrated in the experiments but also maintains the soundness guarantee.

Weaknesses

My main concerns are the following. ### 1. Choice of neural architecture The architecture and some of the layers in Figure 2 seem carefully designed. What are the reasons for choosing these layers? Did you incorporate knowledge of the evaluated tasks into the design of the neural network? ### 2. Size of evaluated tasks How do the chosen tasks reflect real-world usages? As the paper suggests, increasing the network size would slow SMT check (Do other approaches have the same limitation?). If the size of the evaluated tasks is too small compared to real-world usages, the practical effectiveness of the proposed approach would be rather limited. ### 3. Comparison The evaluation compares the neural model checker with other checkers as a whole. While this comparison is valuable, there are many differing factors that can influence the results. I suggest adding ablation studies where different algorithms for constructing the ranking functions while keeping the overall system consistent. This would provide a clearer understanding of the algorithmic contribution of the paper. ### 4. Other smaller issues - At Line 130, the signature of the network contains the parameters of the network. However, at Line 160, the signature does not. I suggest keeping this consistent. - The tool Industry Y failed on all tasks. What is the reason for this?

Questions

Please consider addressing the points raised in the “Weakness” section.

Rating

5

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

The paper has sufficiently addressed the points concerning limitations and societal impact.

Thanks for the rebuttal

Thanks for submitting the rebuttal. I have read it and will keep the score. I hope the authors incorporate the reviews and the rebuttal into the next version of the paper.

reply

Thanks for the detailed reply. I'm happy to improve my score from 4 to 5.