Our model checker PSL up to 60 times faster using AI-tuned proof tactics

From more than two months down to less than two weeks, or six times faster. From almost two weeks down to just five hours, or sixty times faster! These are the kind of speed ups that we are now obtaining in PSL (Prover SL CE) by boosting our turbo-threads technology using AI-optimized proof tactics. Make sure you read our previous blog post back in September, we have been working hard and made very good progress since then. Thanks again to Vinnova, Sweden’s Innovation Agency, for partially funding this R&D project!

The current state of AI-powered PSL

We have a research branch of PSL that has been modified to enable AI-tuned tactics to guide the model-checker during proof search. These proof tactics are obtained by a specialized AI-guided fine-tuning procedure, and they are designed to speed up specific sets of properties. Obtaining one such tactic could, in some cases, keep our servers busy for more than a week. Yet, the obtained tactic can mean saving months of CPU time and faster delivery times for our customers. These proof tactics do not only speed up verification for the HLL model that is used for training, but also boost verification for subsequent versions of the same model. We can fine-tune a proof tactic today and benefit from it for years.

This technology could already be highly valuable to some users of PSL who have very high demands for performance. And you may be able to benefit from it relatively soon! Initially we plan to offer this as a service, that is, you send us an HLL model and we send you back a set of customized proof tactics. For the future we are considering integrating our AI-guided fine-tuner into a special front-end for PSL, so that training happens automatically every time you solve a property.

What is coming next

We are currently experimenting with the computation of features that can characterize and relate a set of safety properties, that is, their “DNA” equivalent. Using this “DNA” will allow us to automatically discover properties that would benefit from known proof tactics, and also compute new proof tactics faster. At the same time, we have also started to explore prediction models, based on deep learning, that could automatically suggest the best proof tactic for a previously unseen property. All this put together would mean that, one day, all PSL users could automatically benefit from these AI-powered speed ups.

Let’s keep working on the future of formal verification!