Nyt globalt initiativ skal gøre software og AI matematisk sikre
Syddansk Universitet har ledende rolle i et nyt internationalt initiativ, CSLib, der skal udvikle en fælles, formel infrastruktur til softwareudvikling med matematiske garantier.
Moderne samfund er dybt afhængige af software. Fra energisystemer og offentlig infrastruktur til sundhedsvæsen, forskning og kommunikation spiller software en afgørende rolle. Samtidig bliver kunstig intelligens i stigende grad brugt til at skabe og forbedre kode. Det øger behovet for, at software er pålidelig, sikker og gennemsigtig.
Inden for datalogi findes der allerede matematiske metoder til præcist at beskrive og verificere software – såkaldte Formal Methods. Men i dag er denne viden spredt på tværs af forskningsartikler og specialiserede værktøjer, hvilket gør den svær at anvende i almindelig softwareudvikling som helhed.
Det vil det nye internationale initiativ CSLib ændre på. Målet er at gøre Formal Methods til en fælles, genanvendelig infrastruktur for softwareudvikling. Initiativet samler forskere og eksperter fra blandt andre Syddansk Universitet, Stanford University, University of Texas at Austin, Amazon, Google DeepMind og Lean FRO.
For Syddansk Universitet betyder deltagelsen, at vi placerer os centralt i udviklingen af fremtidens fundament for software og kunstig intelligens. Initiativet bygger videre på den forskning i Formal Methods, distribuerede systemer og sikker software, der allerede foregår på SDU, og giver forskere og studerende mulighed for at samarbejde tæt med nogle af verdens førende miljøer inden for området. Projektet er derved også i tråd med Syddansk Universitets strategi om at styrke det internationale forskningssamarbejde og udvikle stærke forsknings- og innovationsmiljøer.
Professor Fabrizio Montesi, centerleder for Centre for Formal Methods and Future Computing (FORM) og professor ved Danish Institute for Advanced Study (DIAS) ved Syddansk Universitet, er hovedansvarlig for projektets fremdrift og medlem af initiativets styregruppe.
”Software opererer i dag i global målestok. Hvis vi vil skabe digitale systemer, man kan have tillid til – også de, der formes af AI – har vi brug for matematisk klarhed i samme skala,” siger Montesi. ”CSLib er et langsigtet arkitekturarbejde: vi bygger på den fælles intellektuelle infrastruktur, som fremtidens software og computersystemer kommer til at stå på.
Ifølge Montesi er ambitionen ikke blot at udvikle nye forskningsresultater, men at skabe en fælles infrastruktur, som forskere og udviklere verden over kan bygge videre på.
Matematiske byggesten til fremtidens software
CSLib arbejder med at formalisere centrale områder inden for datalogi – blandt andet algoritmer, programmeringssprog og distribuerede systemer – i programmeringssproget og den digitale bevisassistent Lean. Lean gør det muligt at efterprøve software matematisk, ved hjælp af beviser, der verificeres af en computer.
”Lean giver os et sprog, hvor software og dets matematiske specifikation kan eksistere side om side. Det, der har manglet, er et fælles og modulært bibliotek af verificerede byggeklodser, som udviklere faktisk kan tage i brug. CSLib er netop dette manglende lag.
Målet er her at opbygge et stort bibliotek af verificerede komponenter og matematiske specifikationer, som både forskere og udviklere kan bruge til at bygge pålidelige systemer.
For forskningen betyder det, at nye resultater lettere kan genbruges og bygges videre på, i stedet for at hver forskergruppe skal udvikle deres egne formelle modeller fra bunden. Det kan accelerere udviklingen inden for både softwareteori, sikkerhed og kunstig intelligens.
Kunstig intelligens øger behovet for verificeret software
Projektet ser dagens lys på et tidspunkt, hvor AI-systemer i stigende grad kan generere og optimere komplekse kodebaser på egen hånd. Det kan accelerere innovation - men også gøre det muligt for fejl og sårbarheder at sprede sig hurtigt. Derfor bliver computerverificeret matematik ræsonnement en vigtig del af fundamentet for fremtidens software.
”CSLib vil levere matematisk solide rammer for AI-drevet softwareudvikling og give en model for, hvordan mennesker og AI kan samarbejde sammen på en langt mere sikker måde, til gavn for samfundet.
Samtidig peger forskere på, at netop AI-genereret kode gør behovet for formel verifikation endnu tydeligere. Når software kan produceres i langt større hastighed end tidligere, bliver det afgørende også at have metoder til automatisk at kontrollere, at koden faktisk opfører sig korrekt og sikkert.
”Det som jeg er mest begejstret for, er CSLibs potentiale til at accelerere formel verifikation af kode, der er skabt af kunstig intelligens. AI-baserede kodningsværktøjer er berygtede for at producere usikker kode. Formel verifikation er en guldstandard for at gøre kode sikker fra starten, men det kræver en infrastruktur, der kan modellere kodens matematiske betydning. CSLib bliver den første universelle infrastruktur til netop denne form for modellering.
Ved at integrere formel verifikation direkte i måden software designes og udvikles på, er ambitionen, at CSLib kan bidrage til at styrke tilliden til digitale systemer i de kommende årtier.
For SDU åbner projektet nye muligheder for internationale forskningssamarbejder, fælles innovationsprojekter og talentudvikling inden for et felt, der får stor betydning for både teknologiudvikling og samfundets digitale infrastruktur.
CSLib er et åbent kollaborativt initiativ, og forskere, udviklere og institutioner fra hele verden inviteres til at bidrage til udviklingen.
Om Formal Methods
Formal Methods er matematiske metoder til at beskrive, udvikle og verificere software og computersystemer. Ved at bruge disse metoder kan man lave præcise specifikationer af, hvordan et system skal fungere, og derefter matematisk bevise, at specifikationerne er implementeret korrekt i systemets kode.
Dermed kan man opdage fejl eller sikkerhedsproblemer tidligt i udviklingen og skabe sikrere, mere gennemsigtige og mere pålidelige systemer. Metoderne bruges især i systemer, hvor høj sikkerhed og pålidelighed er afgørende, for eksempel i luftfart, medicinsk udstyr, kritisk infrastruktur og finansielle systemer.
Om Centre for Formal Methods and Future Computing (FORM)
FORM er et forskningscenter, der arbejder med Formal Methods, programmeringssprog og matematiske teknikker til at udvikle pålidelige og fremtidssikrede digitale systemer.
Centret er forankret ved Institut for Matematik og Datalogi (IMADA) på Syddansk Universitet og fungerer som et samlingspunkt for forskning i matematisk baseret softwareudvikling.
FORM har en etableret tilknytning til Danish Institute for Advanced Study (DIAS) gennem forskningssamarbejder og bidrag til tværfaglige forskningsaktiviteter. Denne forbindelse understøtter centrets fokus på interdisciplinær forskning og et bredt, internationalt udsyn.