Vinnere av Master-prisen 2022

Vinnere av NR-prisen for 2022 er Johannes Voll Kolstø fra NTNU, og Emil Haugen og Sarek Skotåm fra UiO. Alle har levert masteroppgaver som har begeistret juryene.

NR-prisen deles årlig ut til masterstudenter i matematikk og IKT ved Universitetet i Oslo (UiO) og Norges teknisk-naturvitenskapelige universitet (NTNU). Prisen består av et diplom og 40 000 kroner. Norsk Regnesentral rekrutterer mange forskere fra UiO og NTNU, og prisen skal styrke rekrutteringen til matematikk- og informatikkstudiene, og samtidig stimulere de beste studentene til ekstra arbeidsinnsats.

Les mer om de tre vinnerne Johannes Voll Kolstø, Emil Haugen og Sarek Skotåm:

Helt i starten av masteren derimot husker jeg at jeg følte på frykten for hvor åpen oppgaven var, uten et helt konkret mål for hva jeg og veilederen min skulle gjøre. Jeg tenker også tilbake på noen av de feilene og utfordringene jeg møtte underveis i løpet av masteren som åpenbare mtp. hvordan løse dem eller lande på et visst valg i etterkant, men jeg prøver å la være å dvele for mye ved det.

Kan du fortelle litt om deg og oppgaven du vant prisen for?

– Jeg tror mange vil beskrive meg som en småtypisk glad bergenser, som etter videregående på Katten (Bergen Katedralskole) visste at jeg ville studere på et sivilingeniørstudium i Trondheim. Jeg landet først på nanoteknologi-retningen, men etter å ha pratet med flere fra fysmat, og da spesifikt spesialiseringen industriell matematikk, ble det klart for meg at det var en haug av spennende fag som jeg ikke fikk plass til i fagplanen på nanostudiet. Derfor byttet jeg over til fysmat-retning Industriell matematikk og kom inn på tredjeåret der, og jeg har vært storfornøyd med det valget faglig sett siden.

Så trives jeg faglig med anvendt matematikk, men klarte aldri å velge ut en spesifikk retning blant mine tre favorittområder numerikk, optimering, og statistisk læring. Så da veilederen min Ronny Bergmann foreslo å studere hvordan man kunne generalisere klassifiseringsmodellen Support Vector Machines (SVM’s) til å operere på Riemanske mangfoldigheter, ble jeg fort interessert. Så i løpet av oppgaven gjorde jeg først et dypdykk i definisjonen og utledningen av SVM’s for klassiske vektorrom, før jeg leste meg opp på hva slags andre modeller inspirert av SVM’s det fantes for å gjøre klassifisering på Riemanske mangfoldigheter.

Mye av utfordringen i å generalisere SVM’s til Riemanske mangfoldigheter ligger i tapet av et globalt indreprodukt. Inspirert av andre SVM-modeller på mangfoldigheter og ved å studere hvordan man konstruerte det klassiske optimeringsproblemet for å løse for SVM-modellen, fant jeg en original måte å bruke den kvadrerte Riemanske avstandsfunksjonen. Dette er et utgangspunkt for en ny SVM-modell på Riemanske mangfoldigheter som jeg kalte Distance-SVM. Jeg testet flere utgaver av denne modellen numerisk på reelle og konstruerte datasett, og sammenlignet ytelsen med eksisterende modeller for klassifisering av mangfoldighetsdata.

Hva gjør du nå?

– Nå jobber jeg i Tunable i Oslo, et spin-off selskap fra Sintef som lager gass-analysatorer som kan detektere konsentrasjonen til et større antall gasser gjennom spektroskopi. Grunnteknologien er et veldig smart filter basert på nanoteknologi som lar oss selektere bølgelengden til lyset som går gjennom prøvene våre med høy presisjon. Så da ble det litt nano-relevant jobb på meg allikevel som er litt morsomt. Der jobber jeg hovedsakelig som som utvikler og skriver kode som kjører på selve analysatorene våre, men jeg er også tidvis med på modellerings og data-science siden av ting.

Hva skal du bruke pengene til?

– Det har jeg ikke tenkt så mye på enda, men det mest sannsynlige om enn litt kjedelige svaret blir nok at mesteparten går med til fondssparing med mål om et eventuelt boligkjøp en gang. Samtidig ble det lite til ferie i sommer mellom master-innleveringen, flytting til Oslo, og oppstart i ny jobb, så kanskje jeg velger å bruke noe av det på en ferie til varmere strøk neste sommer.

Den noe lengre beskrivelsen, som også gir litt kontekst: Når man lager et dataprogram, så er det som regel ønskelig at det gjør hva enn man ønsker at det skal gjøre, og at det ikke har “bugs”. For å sørge for at et program gjør det det skal, kan man anvende diverse teknikker, der en av de mest brukte er testing. Testing er betraktelig bedre enn ingenting, men gir deg fortsatt kun garantier av typen “for denne spesifikke inputen så oppfører programmet mitt seg slik jeg forventer at det skal oppføre seg”. Steget opp fra testing er det som kalles “formell verifisering”, som gir deg garantier av typen “for alle mulige inputs, så gjør programmet mitt det det skal”. Dette innebærer kort forklart et matematisk bevis for at programmet gjør det man ønsker. Før i tiden ble slike bevis gjort “for hånd”, men nå til dags bruker man datamaskiner for å sjekke at beviset er korrekt, også kjent som et “mekanisert” bevis. 

Det å bruke datamaskiner til å bevise full korrekthet for et dataprogram er nok noe mange ikke har vært borti, men de fleste som driver med programmering har vært borti en variant av et slikt verktøy, nemlig typesjekkeren i et typet programmeringsspråk. Typesjekkeren sjekker at programmet ditt er i henhold til reglene satt av typesystemet for alle mulige input, og gir sådan et bevis for veltypethet. Hva som bevises varier fra programmeringsspråk til programmeringsspråk, men kan inneholde for eksempel bevis for at alle funksjonsskall er gjort med verdier som har en type som svarer til en type som funksjonen er definert for, og at vi aldri forsøker å lagre en verdi av en gitt type i en variabel med en annen type. 

Et språk som beviser relativt mye i typesystemet sitt, og som også er det programmeringsspråket jeg har brukt, er programmeringsspråket Rust. Jeg skal ikke gå inn på alt hva Rust tilbyr, men kort fortalt kan man argumentere for at Rust sitt typesystem gir to fordeler. Den første er at siden vi alt må bevise så mye om programmet vårt for å få det til å kompilere, så er vi “nærmere” et bevis av full korrekthet. Den andre fordelen er spesifikt knyttet til Rust sin håndtering av referanser, også kjent som “lånte” verdier. I Rust kan vi enten gi ut et uendelig antall lån som kun kan lese en gitt verdi, eller opp til ett lån som både kan lese og endre en gitt verdi.

Garantiene gitt av dette lånesystemet blir så utnyttet av verktøyet jeg har brukt, Creusot, til å generere bevisuttrykk som er effektivt løselige av en datamaskin. Å bevise at to minneområder ikke overlapper tenderer til å være en av de vanskeligere delene ved å bevise et program korrekt, og blir her løst på typenivå. Videre gir Rust høy kjøretidsytelse både hva gjelder kjøretid og minnebruk, som er kritisk for en del bruksområder, deriblant bruksområdet jeg har valgt, SAT solving. SAT solving er et eget forskningsområde, og har flust av interessante detaljer, men for denne beskrivelsen kan vi vi kan abstrahere det vekk som et problemområde som folk som er interessert i informatikk finner interessant, og hvor både kjøretid og korrekthet er svært viktig.

Om man ikke ønsker å abstrahere vekk SAT solving fullstendig kan man lese følgende avsnitt. Kort fortalt er en SAT-solver et program som løser oppfyllbarhetsproblemet i utsagnslogikk (SAT for SATisfiability). SAT er det første problemet som ble bevist NP-komplett, hvilket vil si at alle andre problemer i kompleksitetsklassen NP (svarer ca. til det som effektivt kan beregnes av en datamaskin) kan skrives om til en utsagnslogisk formel i polynomiell tid (betyr ca. at omskrivingen ikke tar veldig lang tid). For mange problemer er det mer effektivt å skrive en spesialisert løser, men det er også en del problemer hvor SAT-solving er det beste alternativet, og SAT-solving er dermed av både teoretisk og praktisk interesse.

Så ja, kort fortalt har jeg lagd en serie dataprogrammer som folk som driver med informatikk syns er interessante og som trenger å være både raske og korrekte, og så har jeg bevist at disse programmene aldri tar feil. For å gjøre dette har jeg brukt programmeringsspråket Rust, som kombinerer et sterkt typesystem med solid kjøretidsytelse, og verktøyet Creusot, som gir brukeren anledning til å augmentere programkoden med logiske formler, og dermed muliggjør bevis av korrekthet. Dette er både den mest omfattende bruken av Creusot hittil, og, så vidt jeg vet, det hittil største beviset av kode skrevet i Rust. Dette er dermed med på å styrke tesen om at garantiene Rust gir kan brukes til å gi videre garantier, og at dette er en lovende fremgangsmåte for å oppnå verifiserte programmer med høy ytelse.

Den beste av løserne, CreuSAT, er den andre verifiserte løseren som er i stand til å løse en ikke-triviell mengde problemer fra nylige SAT-konkurranser, og er den første som har gjort det ved bruk av det som kalles deduktiv verifisering. Denne fremgangsmåten skiller seg fra tidligere fremgangsmåter for å oppnå verifiserte SAT-solvere, noe som har resultert i betraktelig mindre kode og et kortere bevis, uten at dette har gått på bekostning av kjøretidsytelse. Det å bruke en datamaskin for å sjekke bevisenes korrekthet tar i tillegg betydelig kortere tid enn tidligere fremgangsmåter.

Hva skal du bruke pengene til?

– Tja. Jeg tenkte først hva som ville vært et definitivt feil svar på dette spørsmålet, og konkluderte med fylla. Så jeg endte med å bruke noe av pengene på det, men nå er det for lenge siden jeg fikk pengene til at jeg føler jeg kan bruke de på det. Kanskje jeg kommer på noe tilsvarende dumt med tiden. Hvis ikke blir det vel å være mer spandabel enn vanlig, så å spandere middag og/eller pils på hvem enn som måtte finne på å komme på besøk i London.