Sådan valideres kunstig intelligens
En af udfordringerne med robotter baseret på kunstig intelligens er at sørge for, at robotten ikke pludselig gør noget uventet, der kan få store konsekvenser. Dataloger fra SDU arbejder på at skabe en ny metode til validering af kunstig intelligens.
Robotter, som er baseret på kunstig intelligens, baserer sig i overordnede træk på ’trial and error’. Det betyder, at robotten prøver forskellige muligheder, indtil den finder den rette løsning. Det sker eksempelvis hos flere selvkørende støvsugere, som bevæger sig henover et gulv indtil den støder på en genstand, hvorefter den ændrer kurs og husker på, at her var en genstand, som den ikke skal køre ind i igen.
Den slags fungerer fint, når det gælder rengøring af gulv. Men når det drejer sig om mere kritiske systemer, som eksempelvis i forbindelse med lufttransport eller medicinsk diagnosticering, så er der ikke plads til fejl.
Luís Cruz-Filipe er adjunkt på Institut for Matematik og Datalogi, og han udvikler computerprogrammer, som bruges til at validere kunstig intelligens. Hans forskning hører til under feltet ’machine-assisted proofs’ (maskindrevet bevisførelse) og går ud på, at sætte kunstig intelligens på formel.
Ligninger for lange til at skrive ned
Metoden bag maskindrevede beviser er at konstruere et logisk udsagn, som udtrykker, at alle de mulige handlinger, som en robot kan vælge at udføre, ikke går galt. Det betyder, at udsagnet fungerer som en slags ”sikkerhedsnet” for, at robotten ikke kommer på afveje.
Disse udsagn kan blive lange og indviklede. Faktisk er de ofte så komplicerede, at end ikke forskeren selv kan skrive den ned på papir. Grunden til det er, at computeren får nogle input til at starte ud med og ud fra disse input, er det muligt at lave et matematisk setup, som altså kan undersøge alle de mulige scenarier, en robot kunne komme ud i.
Det betyder, at man via maskindrevet bevisførelse kan tjekke, om en robot potentielt kan komme i en situation, som vil være risikofyldt eller direkte skadelig. Det kan for eksempel være, hvis et flys autopilot skulle vælge en forkert rute, som kan få fatale konsekvenser. Dette scenarie vil dukke op, hvis man bruger disse metoder, og derved kan man programmere flyet om.
Tidligere overset forskning
Computer-drevet matematik som Luís Cruz-Filipe laver har ikke en lang historie bag sig. Feltet er relativt nyt, ifølge Luís Cruz-Filipe er dets praktiske anvendelser opstået for ca. 15 år siden. Han har selv arbejdet med det de seneste 5 år, og mener, at området bliver mere og mere udbredt blandt forskere indenfor computer science.
I sommeren 2018 var Luís Cruz-Filipe en del af ekspertpanelet på ICM2018, som er den vigtigste internationale konference for matematikere. Konferencen blev afholdt i Rio De Janeiro. ICM holdes hvert fjerde år, og det er endnu ikke offentliggjort hvor næste ICM afholdes.
Foto: Luís Cruz-Filipe , adjunkt, Institut for Matematik og Datalogi.