FormAI

Utmaningar

Generativ AI används redan inom industrin för att skapa programvara. En stor utmaning är dock att säkerställa tillförlitligheten hos sådan programvara och att uppfylla säkerhetskritiska systemkrav. FormAI-projektet kombinerar generativ AI för att skapa programvara med deduktiv verifiering, vilket ger formella bevis för att programvaran uppfyller kraven.

Om projektet

Det övergripande målet är att utvidga användningsområdet för generativ AI för att skapa programvara till områden där programvarans korrekthet är kritisk, t.ex. i säkerhetskritiska system. Mer detaljerade mål är: generera C++-kod med generativ AI, automatisera deduktiv verifiering av C++-kod, använda automatisk deduktiv verifiering för att iterativt generera kod med AI; använda verifiering för att förbättra AI-kodgenereringsmodeller genom "förstärkt inlärning", skapa en demonstrator och proof-of-concept, och utforska metoder för att härleda de formella behörighetskrav som behövs.

Förväntade resultat

Om projektet lyckas kommer resultatet att bli att formell deduktiv verifiering kan göras för C++-kod och inte bara C som idag. Graden av automatisering av formell kodverifiering kommer att öka, vilket gör den användbar och tillgänglig för fler tillämpningar. Dessa effekter bidrar i sin tur till ökad programvarukvalitet i kritisk programvara, vilket gör systemen säkrare och mer tillförlitliga. Dessutom uppnås ökad kvalitet på kod som genereras via AI genom förbättrade AI-kodgenereringsmodeller som uppnås genom förstärkningsinlärning i kombination med formell feedback.

För mer information, kontakta