Dr. Bart Bogaerts, hoogleraar aan de Vrije Universiteit Brussel (VUB), wil de correctheid van combinatorische optimalisatie-algoritmes opvoeren tot honderd procent. Voor zijn zogeheten Certifox-project (Certified First-Order Model Expansion) ontvangt hij een European Research Council (ERC) Grant ter waarde van twee miljoen euro.
Combinatorische optimalisatie gaat om het zoeken van een optimale oplossing uit een zeer grote verzameling van mogelijke oplossingen. Het kan dan gaan over praktische problemen zoals het zoeken van een uurrooster waarin zo weinig mogelijk overlap is of het zoeken naar routes voor verschillende koeriers om in zo kort mogelijke tijd alle pakketjes ter plaatse te brengen. Soms gaat het ook over levensnoodzakelijke beslissingen zoals het koppelen van orgaandonoren aan patiënten waarbij zo veel mogelijk transplantaties kunnen plaatsvinden.
De technologie die naar dergelijke oplossingen zoekt is de laatste decennia enorm geëvolueerd. Inmiddels zijn met gemak vele problemen op te lossen, waarbij er vaak miljarden mogelijke opties zijn. Bogaerts: ‘Maar toch ben je nooit helemaal zeker of de machine je de juiste oplossing heeft aangedragen.’ Daarom werkt de VUB-professor met zijn Certifox-project aan een systeem waarbij die onzekerheden verdwijnen.
Hij verduidelijkt: ‘Het centrale doel van mijn project is om methodologieën en hulpmiddelen te ontwikkelen waarmee we met honderd procent zekerheid kunnen garanderen dat het juiste probleem correct is opgelost. Omdat er bij complexe problemen soms vele mogelijke oplossingen zijn en je niet altijd kan controleren hoe een algoritme tot een bepaalde uitkomst is gekomen, willen we voortbouwen op recente doorbraken in het zogenaamde proof logging, waarbij algoritmes niet enkel een antwoord geven, maar ook een bewijs of certificaat van correctheid meeleveren.’
Twijfel
Een beperking van de huidige technieken is dat de correctheid niet wordt bewezen in een voor ons begrijpelijke taal. Er komt een low-level-vertaling in computertaal, waardoor er nog altijd twijfel blijft bestaan over de correctheid van de geleverde oplossing. Bogaerts wil in plaats hiervan een logische taal gebruiken die zowel voor mens als machine te volgen is. Volgens hem garandeert dit dat het correctheidscertificaat uitgedrukt wordt in input van hoog niveau.
