VUB-prof wil de correctheid van combinatorische optimalisatiealgoritmes opvoeren tot 100 procent
Combinatorische optimalisatie gaat om het zoeken van een optimale (zo goed mogelijke) oplossing uit een zeer grote verzameling van mogelijke oplossingen. Het kan dan bijvoorbeeld gaan over praktische problemen zoals het zoeken van een uurrooster waarin zo weinig mogelijk overlap is, het zoeken naar routes voor verschillende postbodes om op zo kort mogelijke tijd alle pakketjes ter plaatse te brengen, soms 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 en kan ondertussen met gemak vele problemen oplossen, waarbij er vaak miljarden mogelijke opties zijn. Maar toch ben je nooit helemaal zeker of de machine je de juiste oplossing heeft aangedragen. VUB-professor dr. Bart Bogaerts wil met zijn CertiFOX-project (Certified First-Order Model Expansion) een systeem uitdokteren waarbij die onzekerheden verdwijnen. Hij krijgt voor zijn onderzoek een ERC Consolidator Grant van Europa ter waarden van twee miljoen euro.
“Het centrale doel van mijn ERC-project is om methodologieën en hulpmiddelen te ontwikkelen waarmee we met honderd procent zekerheid kunnen garanderen dat het juiste probleem correct is opgelost”, zegt Bogaerts. “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.”
Een belangrijke beperking van de huidige technieken is dat de correctheid niet wordt bewezen in een voor ons begrijpbare taal, maar mits een low-level vertaling in computertaal, waardoor er nog altijd twijfel blijft bestaan over de correctheid van de geleverde oplossing. “In mijn project zullen we end-to-end garanties van correctheid onderzoeken”, aldus Bogaerts. “We willen hiervoor een hoog-niveau logische taal gebruiken die zowel voor mens als machine begrijpbaar is en garanderen dat het correctheidscertificaat uitgedrukt wordt in functie van input op dat hoge niveau. Als het lukt, zal het een grote invloed hebben op de manier waarop combinatorische optimalisatie-software ontwikkeld, geëvalueerd en gebruikt wordt: de bewijzen die geproduceerd worden zullen niet enkel debugging mogelijk maken, omdat bewijzen gedetailleerde informatie bevatten over waar bugs zijn opgetreden, maar evengoed de controleerbaarheid ten goede komen, omdat bewijzen opgeslagen en gecontroleerd kunnen worden door een onafhankelijke derde partij. Tot slot zal het uitmonden in een nauwkeurige evaluatie van algoritmische verbeteringen.”
Meer info:
Bart Bogaerts +32 2 629 37 06
https://bartbogaerts.eu/projects/CertiFOX/
