‘Onzekere’ software toch voorspelbaar maken

Software die rekening houdt met allerlei risico’s en onzekerheden wordt steeds belangrijker in de wereld van kunstmatige intelligentie, waartoe ook zelfrijdende auto’s behoren. Professor Joost-Pieter Katoen van de Universiteit Twente gaat onderzoeken hoe je kunt nagaan of die software, met al die onzekerheid, toch goed werkt. Aan het onderzoek is een beurs van 2,5 miljoen euro toegekend.

Katoen is verbonden aan zowel de RWTH in Aken als de Universiteit Twente. Zijn onderzoek zal zich richten op probabilistische computerprogramma’s: software die te maken krijgt met heel veel onzekere en ‘real world’-data. De zelfrijdende auto baseert zijn rijgedrag op zulke software en de autonome robot kan straks ook niet zonder. Maar hoe kun je, bij al die onzekerheid, verifiëren of de software ook goed werkt? Daar zal het onderzoek van Katoen zich op richten.

Oneindig veel toestanden

De instrumenten die programmeurs normaal gesproken voor die verificatie kunnen gebruiken, volstaan niet bij probabilistische computerprogramma’s. Dat ligt aan het omgaan met onzekerheid. Gebruikelijke software heeft al oneindig veel toestanden waarin het programma kan verkeren. Het doorrekenen hiervan is vrijwel onmogelijk.

Formele programma verificatie is een een techniek die een programmeur helpt bij het vaststellen van de correcte werking. Probabilistische programma’s zijn echter nog lastiger te doorgronden, omdat ze omgaan met onzekere data en real-world observaties. Het is eigenlijk niet mogelijk om een conclusie trekken over de correcte werking als dat is gebaseerd op statistische gegevens over deze onzekere data.

Drastisch andere benadering

Simulatietechnieken schieten te kort als het moeilijk wordt. Onderzoekers weten in zo’n geval niet hoe lang ze door moeten gaan met simuleren en de situaties geven geen harde garantie, aldus Katoen. 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 omdat probabilistische software steeds vaker bepalend gaat worden voor bijvoorbeeld onze dagelijkse veiligheid. De zelfrijdende auto baseert er straks zijn beslissingen op.

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.”

Auteur: Vincent Krabbendam

Vincent Krabbendam is redacteur van Zelfrijdend Vervoer, TaxiPro en het tijdschrift Nederlands Vervoer.

Reageer ook

Nog maximaal tekens

Log in via een van de volgende social media partners om je reactie achter te laten.