AI-powered proof tactics pay off

Our model checker Prover SL CE (PSL) is getting a lot faster thanks to artificial intelligence techniques (AI)! We are now able to solve some of the hardest benchmarks in our suite in half the time, and in some cases even 10 times faster! In fact, we are not only getting faster but also more efficient, using less computer resources, in some cases only 8% of the previous ones.

How do we do that?

Well, each system is unique and can benefit from a (sometimes radically) different proof tactic. In practice, though, finding the best proof tactic can be as hard as proving the property itself. So model checkers typically ship a few pre-cooked proof tactics that work reasonably well for most problems. Our “secret sauce” is rather to learn the best proof tactic for a specific system using AI, thereby making the search process much more efficient.

These are just the first results of a significant R&D project on AI that we started in the Spring. Of course, there is still much work to do. Our goal is to develop deep-learning models that automatically propose a good proof tactic by recognizing the high-level patterns in our customers’ HLL models.

We have been following the latest achievements in the AI field with great interest, and after having been awarded R&D funds by Vinnova, Sweden’s Innovation Agency, we finally took the decision to move forward with the future of formal verification. AI is playing an increasingly important role in our society and life. Soon AI may be driving our cars and who knows what more… perhaps proving our safety properties in the blink of an eye?