The self-driving car will rely on it for its driving behaviour, the autonomous robot can’t do without. ‘Probabilistic’ computer programmes are getting more and more important in artificial intelligence. This type of software deals with many uncertainties and real-world data. Is it possible to verify correct operations, given this level of uncertainty? Joost-Pieter Katoen, Professor at the RWTH Aachen and the University of Twente, proposes a new approach, and he receives an Advanced Grant of the European Research Council (ERC) for this.
The tools that are currently available for proving correct software operations, will not be sufficient in the case of probabilistic programmes. This is not because the software in itself is so complex, but because it deals with a lot of uncertainty. ‘Regular’ software already has to deal with an almost infinite number of possible states. Calculating the response to all of these, is virtually impossible. Even hypermodern computers will have difficulties answering the basic question: 'will the programme stop at some point?'. Formal programme verification – a set of calculation rules – is a powerful technique for dealing with this complexity. The Formal Methods and Tools group of the University of Twente has an excellent track record in developing these tools. For probabilistic software, however, things get even more complicated. They deal with uncertain data and real-world observations. How can you draw conclusions in the case of dealing with statistics?
One possible approach is using simulation techniques. According to Joost-Pieter Katoen, these won’t work well enough. You simply don’t know when to stop simulating, and especially under extreme conditions the simulations can not guarantee correct operations. Although formal verification may seem impossible, Katoen is convinced that it is the way to do it. Solid verification methods are necessary, because the software will influence our daily safety, when installed in self-driving cars, for example.
The verification technique Katoen will develop, will be able to calculate the effects of software before it is actually executed on a computer. This is a way to trace unpredicted behaviour and errors. Probabilistic programmes do not behave in a random way, as is sometimes assumed. Formal verification will even make them predictable, is Katoen’s conviction.
Joost-Pieter Katoen is a Professor at both Aachen University (RWTH) in Germany and at the Formal Methods and Tools group at the University of Twente in The Netherlands. For his project ‘FRAPPANT – Formal Reasoning About Probabilistic Programms – Breaking New Ground for Automation’, he now receives an Advanced Grant of the European Research Council.
RWTH also issued a news story on this: 'Always Bug-Hunting'.