Mākslīgais intelekts var padarīt praktisku programmatūras matemātisko pārbaudi
Jaunuzņēmumi uzskata, ka ģeneratīvais mākslīgais intelekts padarīs formālo verifikāciju – matemātisku pierādījumu, ka programmatūrā nav kļūdu – lētāku un plašāk izmantojamu. Taču nozares eksperti šaubās, vai metode no kritiskajām sistēmām nonāks masveida lietošanā.
Stenfordas universitātes pētniece Čujue Sun un viņas kolēģi datorzinātnieki izstrādājuši mākslīgā intelekta rīku, kas inženiertehnisku projektu paveica mazāk nekā pusdienā un par mazāk nekā 500 dolāriem. Trīs augsti kvalificēti eksperti to pašu darbu ar rokām veica piecus mēnešus. Šie agrīnie rezultāti pievērsuši uzmanību formālajai verifikācijai – samērā šaurai programmēšanas un matemātikas jomai, kurā ar matemātiskiem paņēmieniem pierāda, ka programmatūra darbojas pareizi.
Tradicionāli šis process ir ilgs un darbietilpīgs: inženieriem jāuzraksta precīzi apgalvojumi par programmas mērķiem un kods jāpārvērš formulās, ko var pārbaudīt. Uzņēmumi parasti veic sarežģītus testus, bet formālo verifikāciju izmanto reti, kaut gan tā spēj atklāt vēl neparastāku rīcību.
Jaunuzņēmumu sacensība
Tagad vairāki jaunuzņēmumi cer, ka ģeneratīvais mākslīgais intelekts to padarīs praktisku. Sun augustā pievienojās uzņēmumam &Truth, kas ceturtdien publiski sāka darbību un piesaistījis 70 miljonus dolāru. Viņas pētījumā ar mākslīgā intelekta palīdzību pārbaudīta daļa koda, kas šifrē sarunas ziņojumapmaiņas lietotnē Signal. Konkurents Harmonic, ko līdzdibinājis Robinhood vadītājs Vlads Teņevs un kas saņēmis 295 miljonus dolāru, paziņoja, ka tā rīks Aristotle atbalsta C valodā rakstītas programmatūras un Verilog valodā rakstītu aparatūras projektu pārbaudi. To vērtē potenciālie lietotāji, tostarp Nvidia un Tensordyne. Anthropic un uzņēmums Theorem pērn nedēļu paziņoja, ka ar mākslīgo intelektu atraduši kļūdas atvērtā koda programmatūrā, ko triljoniem testu nebija uztvēruši.
Šaubas un ierobežojumi
Tehnoloģija joprojām ir prototipu stadijā, un nav skaidrs, cik klienti ir gatavi maksāt. Daži eksperti apšauba, ka tā atklāj kļūdas, ko rada lietotāju rīcība vai aparatūras bojājumi. Antithesis vadītājs Vils Vilsons verifikāciju nosauc par “lamatām” un uzsver, ka drošību apliecina tikai rūpīga testēšana. Arī Vitaliks Buterins norādījis, ka verifikācija nav universāls līdzeklis.
Formāli pārbaudīta programmatūra jau ir Boeing lidmašīnās, Amazon serveros un Apple ierīcēs. Vidēja izmēra uzņēmumi parasti pārbauda vien vienu galveno funkciju, jo trūkst speciālistu, izmaksas ir augstas un pārbaude var bremzēt jauninājumus. Proofcraft vadītāji brīdina, ka mākslīgā intelekta veidotas specifikācijas var radīt nepamatotu uzticēšanos rezultātiem.
