De zelfrijdende auto baseert er zijn rijgedrag op, en ook de autonome robot kan straks niet zonder. ‘Probabilistische’ computerprogramma’s krijgen een steeds belangrijker plaats in kunstmatige intelligentie. Deze software krijgt te maken met heel veel onzekere en ‘real-world’ data. Hoe kun je, bij al die onzekerheid, verifiëren of het goed werkt? Prof. Joost-Pieter Katoen, hoogleraar aan RWTH in Aken en de Universiteit Twente, gaat het onderzoeken en ontvangt hiervoor een Advanced Grant van 2,5 miljoen euro van de European Research Council.
De tools die programmeurs normaal gesproken tot hun beschikking hebben om de correcte werking van software aan te tonen, zijn niet toereikend voor probabilistische software. Dat ligt niet aan de complexiteit van deze software, maar wel aan het omgaan met onzekerheid. Gebruikelijke software heeft al oneindig veel toestanden waarin het programma kan verkeren. Het doorrekenen hiervan is vrijwel onmogelijk. Een hypermoderne computer heeft bijvoorbeeld moeite met het verifiëren van de elementaire vraag: “stopt het programma überhaupt?”
Formele programma verificatie– een set van regels om aan programma’s te rekenen – is een techniek die een programmeur goed helpt bij het vaststellen van de correcte werking. De groep Formal Methods and Tools van de UT heeft hiermee veel ervaring. Probabilistische programma’s zijn echter nog lastiger te doorgronden, omdat ze omgaan met onzekere data en real-world observaties. Hoe kun je nog een conclusie trekken over de correcte werking als je je moet baseren op statistische gegevens over deze onzekere data?
Veiligheid
Simulatietechnieken schieten uitgerekend tekort als het moeilijk wordt, in extreme situaties, aldus Joost-Pieter Katoen: je weet niet goed hoe lang je in zo’n geval moet doorgaan met simuleren, de simulaties geven bovendien geen harde garantie. Volgens hem is formele verificatie ook hier dé manier om deze tekortkomingen het hoofd te bieden. Dat is een drastisch andere benadering, maar wel hard nodig in een tijd dat probabilistische software steeds vaker bepalend gaat worden voor bijvoorbeeld onze dagelijkse veiligheid. De zelfrijdende auto baseert er straks zijn beslissingen op.
Toch voorspelbaar
Katoen wil de techniek van ‘programmaverificatie’ ook geschikt maken voor probabilistische software: deze techniek rekent aan software nog vóórdat het programma wordt uitgevoerd op een computer. Op die manier komen fouten en onverwacht gedrag aan het licht. Probabilistisch programmeren gaat nadrukkelijk niet over software die zich ‘random’ gedraagt, aldus Katoen: “Formele verificatie gaat het voorspelbaar maken”.
Joost-Pieter Katoen is als hoogleraar verbonden aan de Rheinisch-Westfälische Technische Hochschule (RWTH) in Aken en aan de groep Formele Methoden en Technieken van de Universiteit Twente. Voor zijn project ‘FRAPPANT - Formal Reasoning About Probabilistic Programs – Breaking New Ground for Automation’ ontvangt hij een Advanced Grant van de European Research Council.
Zie ook het nieuwsbericht van RWTH in Aken: 'Always Bug-Hunting'.
