Agentinės programinės įrangos inžinerijos pažadai ir iššūkiai: nuo didelio masto kodo migracijos iki programavimo kalbų modernizavimo.
Kas nutinka, kai dirbtinio intelekto agentai gali perrašyti milijonus kodo eilučių keliomis eilėmis greičiau, nei žmonės spėja jas peržiūrėti?
Microsoft teigia, kad būtent šią problemą ir sprendžia.
Bendrovė kuria ir paleidžia dirbtinio intelekto agentus, kurie keičia vienas didžiausių pasaulyje kodų bazių, tarp jų „Windows“ ir „Azure“. Darbai apima ir 400 milijonų eilučių kodų bazės perkėlimą į naują kompiliatoriaus įrankių rinkinį, ir senojo C bei C++ kodo modernizavimą į Rust, vis dažniau pasitelkiant formalią verifikaciją.
Paaiškinimas: Rust yra programavimo kalba, sukurta taip, kad dar kompiliuojant būtų užkirstas kelias daugeliui atminties valdymo klaidų, būdingų C ir C++. Formali verifikacija – tai matematiniais metodais atliekamas įrodymas, kad programa atitinka nustatytus reikalavimus.
Kodo generavimas tampa lengvąja dalimi. Tikrasis iššūkis – žinoti, ar juo galima pasitikėti. Kai agentai keičia šimtus milijonų kodo eilučių, kaip suprasti, ar jie nesugadino ko nors subtilaus? Kaip išsaugoti elgseną, saugumą ir architektūrinį sumanymą? Ir kaip nedidelė inžinierių komanda gali užtikrintai prisiimti atsakomybę už tokio masto pakeitimus, kuriuos atlieka dirbtinio intelekto agentai?
Šie klausimai yra komandos darbo esmė. Nuo 2024 metų Microsoft derina dirbtinio intelekto agentus su statine analize, testavimu ir formalia verifikacija, siekdama, kad didelio masto programinės įrangos transformacija taptų praktiška ir patikima.
Laikui bėgant valdymo srautas apsivertė. Iš pradžių komanda programavo iš anksto nustatytas darbo eigas, kuriose didieji kalbos modeliai (LLM) buvo kviečiami kaip paprogramės. Iki 2025 metų gegužės agentai tapo geresniais planuotojais nei komandos sukurti konvejeriai, todėl komandos užduotimi tapo kurti įrankius, kuriuos agentai kviečia. Vertingiausi iš tų įrankių yra tie, kurie pasako agentui ir už jo stovintiems inžinieriams, ar pakeitimas teisingas.
Dabar Microsoft nuolat tobulina savo požiūrį naudodama lanksčią agentų valdymo sistemą (angl. harness): ji padeda taikyti formaliuosius metodus, skaidyti didelio masto tikslus sudėtingose sistemose ir spręsti problemas, su kuriomis susiduria brandžios įmonės, turinčios didelių ir sudėtingų kodų bazių. Bendrovė taip pat iš naujo apmąsto, kaip turėtų bendradarbiauti žmonės ir agentai. Net tobulėjant modeliams ir agentų valdymo sistemoms, ekspertų kognityvinė apkrova auga. Žmogaus dėmesys tapo brangiausiu ištekliumi agentinėje programinės įrangos inžinerijoje, o įrankiai kuriami taip, kad jį panaudotų ten, kur svarbiausia.
Tai pirmasis įrašas serijoje apie tai, ką Microsoft kuria, ko išmoko ir į kokius klausimus dar bando atsakyti. Jame pristatomos kai kurios sprendžiamos problemos ir jas jungiančios idėjos.
Migracija
Įsivaizduokite, kad panašius pakeitimus reikia atlikti šimtuose milijonų kodo eilučių, kurias prižiūri tūkstančiai inžinierių. Toks yra didelio masto kodo migracijos iššūkis. Sugeneruoti vieną pakeitimą nesunku. Sunku tūkstančius pakeitimų atlikti vienodai teisingai: užfiksuoti, ką žino ekspertai, patikrinti tas žinias ir nuosekliai jas pritaikyti, neįtraukiant į darbą kiekvieno organizacijos inžinieriaus.
Microsoft migraciją apibrėžia kaip visoje kodų bazėje taikomą transformaciją tam tikram inžineriniam tikslui pasiekti, pavyzdžiui, atnaujinti priklausomybes, pereiti prie naujo kompiliatoriaus, pašalinti statinės analizės nustatytus trūkumus arba persikelti į naują platformą. Bendrovės atvejų tyrimai apima visos „Windows“ kodų bazės, kurią sudaro kelios šimtai milijonų kodo eilučių, migraciją siekiant pridėti Clang/LLVM įrankių rinkinio palaikymą; CodeQL, PREfast ir Roslyn analizatorių nustatytų trūkumų šalinimą įvairiose kodų bazėse; ir paslaugų perkėlimą iš x86 į ARM architektūrą.
Bendrovė sąmoningai pasirinko tokį veikimo modelį: labai nedidelė migracijos ekspertų komanda gali ir turėtų vadovauti didelei migracijai. Užuot migracijos atsakomybę paskirsčiusi visai inžinerijos organizacijai, Microsoft sutelkia kompetenciją ir sustiprina ją agentais.
Pirmiausia agentai iš atrinktų radinių išmoksta kandidatinę žinių bazę. Peržiūros agentas įvertina kiekvieną siūlomą pataisą pagal teisingumą, minimalumą, atitiktį failų konvencijoms ir palaikomumą, o jo išvados padeda tobulinti žinių bazę. Tada ekspertai tvirtina žinių bazę, o ne atskiras pataisas, ir agentai ją pritaiko visoje kodų bazėje. Žmonių grįžtamasis ryšys išlieka esminis, tačiau jis nukreipiamas ten, kur duoda didžiausią naudą: žinioms tvirtinti ir naujiems ar dviprasmiškiems atvejams spręsti. Panašių pataisų grupavimas peržiūrai dar labiau sumažina recenzentų kognityvinę apkrovą.
Kalbų modernizavimas
Didelė dalis svarbiausios pasaulio programinės įrangos parašyta tokiomis kalbomis kaip C/C++, kuriose atminties saugumo klaidas lengva padaryti ir sunku pašalinti. Perrašymas Rust kalba žada saugumą pačioje konstrukcijoje, bet tik jei perrašytas kodas tiksliai išsaugo tai, ką darė originalas. Realių sistemų mastu rankinis perrašymas retai praktiškas, o automatizuotas naudingas tik tada, kai juo galima pasitikėti.
Microsoft darbas sutelktas į senųjų kodų bazių perkėlimą į Rust, o sparčiai tobulėję modeliai ir agentai pakeitė tai, kas įmanoma:
Kiekvienas žingsnis perkėlė kliūtį: nuo sukompiliavimo prie testų išlaikymo ir toliau prie patikrintos elgsenos dideliu mastu. Gerėjant generavimui, iššūkiu tapo nuspręsti, ką modernizuoti, ir parodyti, kad rezultatas teisingas.
Bendrovė sukūrė interaktyvias priemones, padedančias inžinieriams vizualizuoti kodų bazės modulių struktūrą ir sluoksniavimą bei nuspręsti, kuriuos komponentus modernizuoti ir kokia tvarka. Tada įrankiai sukuria ir modernizuotą kodą, ir jo patikros strategiją.
Microsoft nustatė, kad migruoti funkcija po funkcijos veiksmingiau nei versti komponentą eilutė po eilutės. Funkcija yra vartotojui matomos elgsenos vienetas, kurį galima patikrinti visa apimtimi scenarijais grįstais testais, o kiekviena funkcija turi savo patikros barjerą. Diferencinis testavimas lygina pirminio ir tikslinio kodo elgseną, o agentui neatskleisti testai (kad jis nepersimokytų pagal juos) parodo vertimo atsparumą. Visai neseniai bendrovė pradėjo iš pirminio kodo išgauti formaliąsias specifikacijas, perkelti jas į tikslinę kalbą ir naudoti Verus įrodymui, kad modernizuotas kodas jas tenkina.
Specifikacijomis grįstas kūrimas
Agentai gali sukurti pakeitimus greičiau, nei žmonės spėja juos įvertinti, o vietoje tikėtinai atrodantis kodas vis tiek gali pažeisti architektūrines prielaidas, paskirstytuosius protokolus, saugumo ribas ar veikimo invariantus. Testai sugauna dalį tokių problemų, recenzentai – kitą dalį, bet nė vieni nespėja paskui agentų kuriamų pakeitimų tempą. Microsoft mano, kad atsakymas – aiškiai išreikšti ketinimą. Agentams rašant vis daugiau kodo, kūrėjų dėmesys slenka nuo kodo rašymo prie specifikacijų, kurios nukreipia agentus ir patikrina jų rezultatus, valdymo. Bendrovė kuria įrankius, kurie formalias, interpretuojamas specifikacijas padeda programinės įrangos kūrimo gyvavimo ciklo centre.
Pirmasis žingsnis – naudojant agentus iš esamų kodų bazių išvesti formaliąsias specifikacijas (pvz., TLA+). Šios specifikacijos fiksuoja lygiagretumą, atsparumą gedimams ir kitus svarbių programinės įrangos komponentų aspektus. Bendrovė naudoja tokius įrankius kaip TLC, kad patikrintų, ar realizacijos vykdymo pėdsakus specifikacijos leidžia. Tai suteikia įrodymų, kad specifikacijos priima realizacijos stebėtą elgseną; ar jos taip pat atspindi tai, ką sistema turėtų daryti, yra sunkesnis klausimas, prie kurio grįžtama toliau. Kai pėdsakas nepriimamas, neatitikimas gali rodyti realizacijos defektą, netikslią specifikaciją arba netinkamą testą, o agentai pataiso tai, kas klaidinga.
Paaiškinimas: TLA+ yra formali kalba, skirta tiksliai aprašyti, kaip turi elgtis sudėtingos, ypač paskirstytosios, sistemos. TLC – įrankis, kuris automatiškai tikrina tokius aprašus.
Turėdama specifikacijas, Microsoft jas panaudoja praktiškai. Jos yra geras „lietingos dienos“ testų atvejų šaltinis – tokių, kurie tikrina sudėtingus lygiagrečių operacijų persipynimus ir gedimų scenarijus. Bendrovė modelių tikrinimu ieško kontrapavyzdžių mažose, baigtinėse konfigūracijose, kad galimus ypatumus ir induktyviuosius invariantus patikrintų greitai, o savybes visoms konfigūracijoms įrodo F* ir Lean, naudodama kuriamą TLA+ į F* ir TLA+ į Lean kompiliatorių. Esamoms (angl. brownfield) kodų bazėms šis specifikacijų, testų atvejų ir savybių sluoksnis tampa apsauginiu turėklu būsimiems dirbtinio intelekto atliekamiems pakeitimams.
Microsoft tikslas – suteikti formaliųjų metodų galią kiekvienam inžinieriui, nereikalaujant jo tapti TLA+ ar formaliosios verifikacijos ekspertu. Inžinierius peržiūri ir patvirtina savybes, kurias sistema turi tenkinti, o agentai suranda joms įrodyti reikalingus induktyviuosius invariantus. Specifikacijoms tapus išsamioms, jos gali tapti ir modernizavimo atspirties tašku, būtent taip bendrovė žiūri į C/C++ vertimą į Verus patikrintą Rust kodą.
Atviri klausimai
Štai keli atviri klausimai, su kuriais Microsoft komanda tebesiknaiso:
- Ar galima pasitikėti dirbtinio intelekto parašytomis specifikacijomis? Kai agentas specifikaciją išveda iš paties kodo, kurį ji turėtų tikrinti, kaip žinoti, kad specifikacija atspindi tai, ką sistema turėtų daryti, o ne vien tai, ką ji daro dabar?
- Ar galime patikrinti daugiau nei funkcinį teisingumą? Ar agentai gali padėti analizuoti saugumą, našumą ir patikimumą, o ne vien tikrinti, ar kodas pateikia laukiamą rezultatą?
- Ar inžinieriai galiausiai nustos skaityti kodą? Jei agentai generuoja kodą, o verifikavimo įrankiai įrodo, kad jis atitinka patvirtintas specifikacijas, ar inžinieriai gali nustoti skaityti kodą ir dirbti tik specifikacijų lygmeniu?
- Kam priklauso kodas, kai kiekvienas agentas gali pakeisti viską? Tradicinė kodo nuosavybė remiasi prielaida, kad inžinieriai dirba gana aiškiai apibrėžtose ribose. Agentinis kūrimas meta iššūkį šiai prielaidai. Kas ją pakeis?
Komandai tai nėra hipotetiniai klausimai. Jie lemia, ką ji kurs toliau.
Microsoft komanda kviečia skaitytojus pasidalyti tuo, ką jie mato savo darbe, nurodyti, kur su ja nesutinka, ir kokias problemas laiko svarbiausiomis. Savo mintimis galima laisvai pasidalyti susisiekus su komanda.
