Kunstig intelligens kan nu løse komplekse programmeringsopgaver, som for blot få år siden ville kræve avanceret universitetsviden. Men vi står over for et paradoks: jo hurtigere AI genererer kode, desto sværere bliver det at stole på den.
Problemet er ikke nyhederne. Det er tilliden. Når en menneskelig programmør løser en opgave for os, bygger vi tillid gennem dialog: Hvad var intentionen? Hvorfor blev netop disse valg truffet? Hvor var der usikkerhed? Gennem samtalen danner vi os et reelt billede af arbejdet.
Med AI bryder denne dynamik sammen. En AI-agent kan skifte tilgang midt i arbejdet, omfortolke instruktioner og omskrive sin egen arbejdskontekst – gentagne gange i en enkelt session. Når AI’en færdiggør koden og vi spørger, hvorfor den skrev det sådan, udledes svaret på baggrund af koden og konteksten på det tidspunkt – ikke som en stabil forståelse, der styrede arbejdet hele vejen. Svaret kan lyde overbevisende uden at være pålidelig.
Hastighed uden kontrol
Man kunne indvende, at løsningen er simpel: læs koden selv. Men så møder vi det andet problem. AI genererer og ændrer kode langt hurtigere, end mennesker kan forstå den. Det er netop her produktivitetsgevinsten ligger. Hvis vi skal håndtere enhver linje kode gennem menneskelig kontrol, mister vi hele fordelen ved automatiseringen.
Løsningen ligger i at kvalitetssikre software med maskinernes hastighed. Det gøres gennem formelle metoder og bevisassistenter – værktøjer, der præcist kan beskrive, hvad software skal gøre, og maskinelt bevise, at kravene er opfyldt.
Tag eksemplet med robotkoordinering på et lager. Vi kan specificere, at to robotter aldrig må køre ind i samme passage samtidigt. AI skriver koordinationsalgoritmen, mens en bevisassistent kontrollerer – uafhængigt af AI – at hver version opfylder kravet. Det skabes matematisk sikkerhed, ikke blot menneskeligt håb.
Fra kontrol til viden
Men formelle metoder gør mere end at verificere. De giver også AI bedre begreber og viden at arbejde ud fra. Inden for matematik har vi allerede set dette gennembrud. For blot få år siden havde AI-systemer svært med avanceret matematisk ræsonnement. I dag når de internationale matematikolympiader og arbejder på uløste forskningsproblemer.
Nøglen har været at integrere AI med bevisassistenten Lean og dens matematikbibliotek Mathlib – et globalt samarbejde på millioner af linjer med præcise definitioner og sætninger. Det giver AI ikke bare fakta at slå op, men et rigt matematisk sprog, hvor nye ræsonnementer kan formuleres og kontrolleres maskinelt.
Samme princip er nu ved at blive anvendt på datalogi. Lean-fællesskabet arbejder på Lean Computer Science Library (CSLib) – et internationalt open source-projekt om at opbygge et fælles, maskinverificeret bibliotek af verificeret kode og datalogisk viden. Det var CSLib, der gjorde det muligt for en AI-agent at løse den svære programmeringsopgave, der blev nævnt i indledningen – og som forskeren kunne bevise matematisk korrekt.
To bølger af udvikling
Der tegner sig et billede af to bølger, der kan transformere programmering.
Den første bølge handler om at bevise, at AI-genereret software opfylder vores specifikationer. AI får frihed til at afprøve løsninger uden konstant menneskelig kontrol, men inden for sikre matematiske rammer. Det erstatter ikke test eller ingeniørfaglig dømmekraft – det tilføjer en ny form for kvalitetssikring, der kan skaleres op med AI’s egen hastighed.
Den anden bølge er mere ambitiøs: at gøre AI bedre til programmering ved at give den bedre datalogisk viden. Jo rigere det formelle begrebsapparat bliver – med præcise definitioner af ‘sikkerhed’, ‘effektivitet’ og ‘korrekthed’ – desto mere komplekse problemer kan AI løse. Det er ikke længere blot om at verificere, hvad AI allerede kan. Det er om at udvide, hvad AI og mennesker kan bygge sammen i stor skala og med tillid til resultatet.
Danmark har muligheden
For Danmark er denne udvikling langt fra teoretisk. Syddansk Universitet (SDU) spiller allerede en førende rolle i CSLib-projektet, og flere danske universiteter har gennem mange år opbygget stærk ekspertise inden for formelle metoder. Der er en reel mulighed for at være med til at forme den næste æra af softwareudvikling – en æra, hvor mennesker og AI udvikler pålidelig teknologi med hidtil uset fart.