Moderne machines nemen steeds vaker hun eigen beslissingen in de echte wereld, van zelfrijdende auto's die door drukke straten navigeren tot drones die pakketjes bezorgen. Deze systemen vertrouwen vaak op complexe computerprogramma's, inclusief kunstmatige intelligentie, die fungeren als "black boxes". We weten dat ze werken, maar we kunnen niet altijd precies zien hoe ze denken of elke mogelijke beweging die ze kunnen maken voorspellen. Om te garanderen dat deze machines veilig zijn, gebruiken ingenieurs een techniek genaamd abstractie. Ze vervangen de ingewikkelde, continue realiteit van een bewegend object door een eenvoudiger, stapsgewijs model gemaakt van duidelijke blokken. Dit stelt hen in staat om te controleren of de machine zal crashen of falen voordat deze de laboratoriumomgeving ooit verlaat. Er zit echter een addertje onder het gras. Om veilig te zijn, moeten deze vereenvoudigde modellen conservatief zijn; ze moeten uitgaan van het slechtste scenario voor elke beweging. Als ze te conservatief zijn, raken ze overvol met onmogelijke, imaginaire gevaren die in werkelijkheid nooit voorkomen. Dit "vals alarm"-probleem maakt de modellen zo groot en rommelig dat computers ze niet op tijd kunnen analyseren, waardoor ingenieurs niet in staat zijn om de veiligheid van de systemen die ze hebben gebouwd te certificeren.

Een team van onderzoekers aan de University of Florida heeft een nieuwe methode ontwikkeld om dit evenwichtsprobleem op te lossen. Ze hebben een tool ontwikkeld genaamd S3, die fungeert als een vloeiende gids voor het verfijnen van deze vereenvoudigde modellen. In plaats van te gokken hoe de blokken van het model gerangschikt moeten worden, hebben de onderzoekers een wiskundig doel (objective) gebouwd dat kan worden bijgesteld en verbeterd met standaard optimalisatietechnieken. Deze tool stelt hen in staat om automatisch de grootte en vorm van de blokken van het model aan te passen om onnodige imaginaire gevaren te verwijderen, terwijl het model wel veilig blijft. Door deze aanpak te testen op drie verschillende scenario's — een spiraalsgewijs systeem, een unicycle-achtige robot en een gesimuleerde auto die een heuvel opklimt — ontdekten zij dat hun methode modellen produceert die veel nauwkeuriger zijn en veel sneller te berekenen zijn dan voorheen gebruikte technieken. Het resultaat is een manier om te verifiëren dat complexe, intelligente machines veilig zijn zonder te verdrinken in excessieve, onrealistische waarschuwingen.

De kernuitdaging bij het verifiëren van deze machines ligt in de spanning tussen veiligheid en praktische bruikbaarheid. Wanneer ingenieurs een vereenvoudigd model bouwen van een bewegend systeem, moeten ze ervoor zorgen dat elke mogelijke beweging in de echte wereld door het model wordt gedekt. Als het model een echt pad mist, is het onveilig. Om dit te garanderen, bevat het model vaak extra paden die de echte machine nooit zou kunnen nemen. Deze extra paden zijn de "spuria" (niet-echte) gedragingen die eerder werden genoemd. Ze zijn als het tekenen van een kaart die elke mogelijke weg bevat, inclusief wegen die geblokkeerd zijn door muren of naar een klif leiden, alleen maar om er zeker van te zijn dat je geen geldige route mist. Ho'ewel dit ervoor zorgt dat je geen echt gevaar mist, creëert het een kaart die zo vol staat met doodlopende wegen dat deze onbruikbaar wordt voor het plannen van een reis. De onderzoekers hadden een manier nodig om deze doodlopende wegen te snoeien zonder echte wegen af te snijden.

Om dit te bereiken, richtte het team zich op een specifiek type wiskundige relatie genaamd simulatie. In deze context is een simulatie een manier om te controleren of het vereenvoudigde model het gedrag van het echte systeem kan nabootsen. Als het model "sound" (degelijk) is, betekent dit dat het echte systeem nooit iets kan doen wat het model niet toestaat. De onderzoekers wilden de "reverse simulation" fout minimaliseren, die meet hoeveel het model de mogelijkheden van het systeem overschat. Een hoge fout betekent dat het model te conservatief is, gevuld met te veel nepaden. Het probleem was dat de standaardmanier om deze fout te meten te traag en te grillig was om automatisch te verbeteren. Het was alsoal proberen een gekreukeld stuk papier met de hand glad te strijken, plooi voor plooi, zonder een hulpmiddel om je vingers te geleiden.

De doorbraak van de onderzoekers was het creëren van een "surrogaat", een vloeiende, gemakkelijk te berekenen vervanger voor de moeilijke foutmeting. Ze hebben een nieuwe doelfunctie afgeleid die de fout in het slechtste geval benadert maar vloeiend verlojd, waardoor computers gebruik kunnen maken van gradiënt-gebaseerde optimalisatie. Denk hierbij aan het vervangen van een grillig, rotsachtig bergpad door een gladde, glooiende heuvel die naar dezelfde bestemming leidt. Door de helling van deze gladde heuvel te volgen, kan de computer snel de beste rangschikking van de blokken van het model vinden. Dit proces houdt in dat de tussenruimtes tussen de blokken worden aangepast, waarbij ze breder of smaller worden afhankelijk van waar het systeem het meest onvoorspelbaar beweegt. De methode garandeert dat het resulterende model veilig blijft door constructie, wat betekent dat het nooit een echt pad mist, maar de nepaden agressief wegknipt.

Het team testte deze aanpak op drie verschillende systemen om te zien of het in de praktijk werkte. De eerste was een eenvoudig tweedimensionaal systeem dat in een spiraal naar een doel beweegt. De tweede was een driedimensionale unicycle-robot die om een obstakel heen moest navigeren om een doel te bereiken. De derde was een simulatie van een auto die een steile heuvel probeert te beklimmen, een klassieke uitdaging in de robotica waarbij de auto momentum moet opbouwen om de top te bereiken. In elk geval vergeleken ze hun nieuwe methode met twee gevestigde strategieën: één die het model alleen verfijnt wanneer het een specifieke fout vindt, en een andere die de roostergrootte optimaliseert met een vaste vorm. De resultaten toonden aan dat de nieuwe methode aanzienlijk sneller was. Voor de unicycle-robot duurde de nieuwe aanpak ongeveer 140 seconden om het model te bouwen en te verifiëren, terwijl de oudere verfijningsmethode meer dan 1.900 seconden in beslag nam. Voor de auto die de heuvel opklom, duurde de nieuwe methode ongeveer 12 seconden vergeleken met bijna 100 seconden voor de oudere methode.

Naast snelheid verbeterde ook de kwaliteit van de modellen. De onderzoekers maten hoe goed de nieuwe modellen het gedrag van het systeem voorspelden en ontdekten dat ze veel minder conservatief waren. In de unicycle-test verminderde de nieuwe methode de gemiddelde fout met een aanzienlijke marge, wat betekende dat het model veel minder onmogelijke paden bevatte. Voor de auto op de heuvel stelde de nieuwe methode het verifiëren van een groter deel van de startposities mogelijk die daadwerkelijk tot succes zouden leiden. Dit is cruciaal omdat een model dat te conservatief is, een ingenieur kan vertellen dat een auto de heuvel niet vanuit een bepaalde positie kan beklimmen, zelfs als dat wel degelijk kan. Door dit valse conservatisme te verminderen, geeft de nieuwe methode ingenieurs meer vertrouwen dat hun systemen werken zoals bedoeld.

De studie onthulde ook hoe het nieuwe instrument zich gedraagt onder verschillende instellingen. De onderzoekers ontdekten dat ze de tool konden afstemmen om zich ofwel op het slechtste scenario, ofwel op het gemiddelde gedrag van het systeem te richten. Als het doel is om absolute veiligheid te garanderen tegen de meest extreme mogelijkheden, kan de tool worden ingesteld om prioriteit te geven aan de fout in het slechtste geval. Als het doel is om een beter algemeen beeld te krijgen van hoe het systeem gewoonlijk gedraagt, kan de tool worden aangepast om zich op het gemiddelde te richten. Deze flexibiliteit stelt ingenieurs in staat om de juiste balans te kiezen voor hun specifieke behoeften. Het team merkte ook op dat de tool er van nature in slaagde om de blokken van het model kleiner te maken in gebieden waar het systeem snel bewoog of van richting veranderde, en groter waar de beweging constant was. Deze adaptieve granulariteit is precies wat nodig is om efficiënte modellen te creëren zonder rekenkracht te verspillen aan gebieden die gemakkelijk te voorspellen zijn.

De implicaties van dit werk reiken verder dan alleen deze drie voorbeelden. De methode biedt een algemeen kader voor het praktisch maken van de verificatie van complexe, intelligente systemen. Naarmate machines autonomer worden en worden ingezet in veiligheidskritische omgevingen, is het vermogen om hun veiligheid snel en accuraat te verifiëren van groot belang. De nieuwe tool vereist niet dat ingenieurs de exacte controller weten die de machine gebruikt; het werkt met de bekende dynamica van het systeem en het gedrag van de controller. Dit maakt het toepasbaar op een breed scala aan scenario's, van industriële robots tot autonome voertuigen. De onderzoekers hebben hun code openbaar gemaakt en nodigen anderen uit om voort te bouwen op dit fundament.

Uiteindelijk toont het werk aan dat het mogelijk is om zowel veiligheid als efficiëntie te hebben in de verificatie van complexe systemen. Door een moeilijke, grillige meting te vervangen door een vloeiende, optimaliseerbare gids, hebben de onderzoekers een nieuw pad geopend voor ingenieurs om de volgende generatie intelligente machines te ontwerpen en te certificeren. De methode belooft niet elk probleem in kunstmatige intelligentie op te lossen, maar biedt een concrete, betrouwbare manier om te garanderen dat de systemen waarop we vertrouwen niet alleen slim, maar ook veilig zijn. Het vermogen om de ruis van valse alarmen weg te filteren en te focussen op de echte risico's is een belangrijke stap voorwaarts in het vakgebied van betrouwbare engineering.