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 strategies. 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-optimized strategies to guide the model-checker during proof search. These proof strategies are obtained by a specialized AI-guided optimization procedure, and they are designed to speed up specific sets of properties. Obtaining one such strategy could, in some cases, keep our servers busy for more than a week. Yet, the obtained strategy can mean saving months of CPU time and faster delivery times for our customers. These proof strategies 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 optimize a proof strategy 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 strategies. For the future we are considering integrating our AI-guided optimizer 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 strategies, and also compute new proof strategies faster. At the same time, we have also started to explore prediction models, based on deep learning, that could automatically suggest the best proof strategy 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!