Amazon använder AI för att bevisa säkerheten i sin databasprotokoller
Amazon har låtit stora språkmodeller skriva formella matematiska bevis för att verifiera att AWS Auroras databasprotokoll fungerar korrekt – och ett automatiserat bevisverktyg kallat Lean 4 kontrollerar varje steg. Det intressanta här är inte bara att AI sparar tid, utan att den faktiskt kan producera maskinverifierad, logiskt vattentät kod – något som traditionellt krävt specialiserade matematiker.
Djupdykning
AWS Aurora är Amazons molndatabas som används av tusentals företag världen över – och kärnan i systemet är ett komplext protokoll för hur data sprids och synkroniseras mellan servrar. Det som händer nu är att Amazon använder stora språkmodeller (LLM:er, alltså AI som GPT-varianter) för att faktiskt *skriva* de matematiska bevisen för att detta protokoll fungerar korrekt, och sedan låter ett verktyg kallat Lean 4 – ett formellt bevisassistentsystem – mekaniskt verifiera varje logiskt steg. Formell verifiering är inte nytt, men det har historiskt varit så tidskrävande att det reserverats för flygmjukvara och kärnkraftssystem, inte databaser som uppdateras kontinuerligt. Det som förändras här är att AI nu tar bort den mänskliga flaskhalsen i processen – att skriva dessa bevis är notoriskt trist och kräver sällsynt specialkompetens. Det de flesta missar är att detta inte primärt handlar om att AI är smart nog att bevisa matematik – det handlar om att mjukvaruindustrin äntligen börjar röra sig mot en värld där kod kan *bevisas* korrekt snarare än bara *testas*. Testning hittar buggar du tänkt på; formell verifiering visar att buggar av en viss typ är matematiskt omöjliga. När AI gör den processen skalbar kan vi se ett skifte där kritisk infrastruktur – banker, sjukvård, energinät – börjar kräva formella bevis som standard, ungefär som byggbranschen kräver statiska beräkningar innan en bro godkänns.