The time is ripe for “productifying” our work on AI-tuned proof tactics. A 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.
Up to 100x faster induction proofs
Back in March we reported astonishing speed ups of up to 60x, but in the meantime we have found cases where induction proofs become even 100x faster after fine-tuning! An otherwise 4-day run becomes a 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.
On-the-fly fine-tuning of BMC
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!
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Do you have experience in leading strategic and complex customer projects? Are you looking for an opportunity to leverage your experience throughout our company? Then this role might be right for you! We are now recruiting to a new position as a Commercial Project Management (PM) Lead.
Prover uses formal methods to make railway signaling provably safe. Our solutions build safe, reliable, and cost-efficient systems that move and protect millions of passengers every day. Through our Open Signaling Initiative, we're reshaping how the industry builds and maintains signaling systems across Europe and beyond. Now we're looking for someone to join us and bring AI, LLMs, and agentic workflows into the heart of how we work and what we build.
Meet Prover at RailTech Europe in Utrecht, March 4–5. Visit Booth 2.509 and join our workshop on migration of signaling systems to PLC-based SIL 4 solutions.
