FormAI - Formally Verified AI-Generated Software

Syfte och mål

Det övergripande målet är att utvidga användningsfallet för generativ AI för att skapa mjukvara till områden där korrektheten av mjukvaran är kritisk, t.ex. i säkerhetskritiska system. Mer detaljerade mål är: generera C++-kod m.h.a. LLM, automatisera deduktiv verifiering av C++-kod, använda automatisk deduktiv verifiering för att iterativt generera kod m.h.a. AI; använda verifiering för att förbättra AI-kodgenereringsmodeller genom ”reinforcement learning”, skapa en demonstrator och proof-of-concept, och utforska metoder för att härleda de formella krav som behövs.

Förväntade effekter och resultat

Under förutsättning att projektet lyckas, så blir resultatet att formell deduktiv verifiering kan göras av C++ kod och inte bara C som idag. Automatiseringsgraden av formell kodverifiering kommer höjas vilket gör den användbar och tillgänglig för fler applikationer. Dessa effekter bidrar i sin tur till ökad mjukvarukvalitet i kritisk mjukvara vilket gör att system blir säkrare och mer hållbara.Vidare uppnås ökad kvalitete på kod genererad via AI genom förbättrade AI-kodgenereringsmodeller som uppnås från ”reinforcement learning” kombinerad med formell feedback.

Planerat upplägg och genomförande

Projektet leds av Scania. De första månaderna fokuserar på rekrytering och uppstart. Under 2024 är fokus dessutom val av LLM och initiala guidande experiment med C. Parallellt utvecklas stödet för verifiering av C++ kod. Projektet jobbar med fallstudier med riktiga industriella krav och industriell kod. Stegvis görs experiment med svårare och svårare exempel. Fokus i utvecklingen och forskningen läggs på saker som behöver förbättras för att få dessa industriella exempel att fungera.