Time to start offering AI-tuned proof tactics to the world!

The time is ripe for “productifying” our work on AI-tuned proof tactics. Few weeks ago we made the first release of our AI-guided fine-tuning toolset, also known as PSL fine-tuner, for broader internal use. Our ambition is that fine-tuning of PSL proof tactics could be offered as part of Prover Cloud Apps in the near future. In fact, we have already contacted some customers to establish collaborations in order to shape this potential new service.

AI-tuned proof tactics are part of the R&D project on AI-Powered Formal Verification that we started back in Spring 2019, and that is being generously partially funded by Vinnova (Sweden’s Innovation Agency). Make sure you read the first and second blog posts of these series.

Back in March we reported astonishing speed ups of up to 60x, but in the mean time we have found cases were induction proofs become even 100x faster after fine-tuning! Literally, an otherwise 4-day run becomes an 1-hour run using the right proof tactic.

We obtain such specialized proof tactics by learning from smaller versions of properties, and we then expect the tactics to generalize to the actual (larger) properties of interest. We have observed that these “smaller versions” can be obtained in different ways. In particular, for CBTC systems that are divided into multiple zone controllers (ZC), it is possible to train on the smaller ZC and the obtained proof tactics typically work well for the larger ones. We have also confirmed experimentally that proof tactics continue to work after successive iterations of the same system.

This may be of special interest to those of you developing CBTC systems. If you use our AI-tuning technology early in the development phase, you could benefit from significantly faster proving times for the years to come.

For bounded model checking (BMC) we have managed to take this a step further, and we don’t require offline training on smaller versions of properties. We are able to fine-tune the BMC of a property on-the-fly. The BMC completes faster (up to 10x faster in our experience so far), and you also get the tuned proof tactic to use for subsequent regression runs.

Let us know if you have a hard verification problem that you would like us to try this technology on!