Google paplašinājis savu Antigravity daudzu aģentu sistēmu, kurā specializēti aģenti, ko darbina uzņēmuma Gemini modeļi, paralēli risina ilgstoši neatrisinātas matemātikas problēmas, pārbauda sarežģītus pierādījumus un optimizē programmatūras sistēmas. Uzņēmums norāda, ka Teamwork ietvars apvieno cilvēku ekspertīzi ar vairākiem aģentiem, kuri neatkarīgi meklē risinājumus, pārbauda pieejas un ar skaitļošanas rīkiem verificē rezultātus.

Matemātisku pierādījumu pārnešana pārbaudāmā formā

Viens no nozīmīgākajiem rezultātiem ir Veila konjektūru formalizēšana. Tas ir nozīmīgs matemātisku rezultātu kopums par polinomu vienādojumu risinājumu skaitu galīgos laukos. Google Teamwork-LEAP sistēma šim uzdevumam radīja aptuveni 1,8 miljonus Lean koda rindu, izmantojot 28 800 apakšaģentu izsaukumu. Rezultāti sākotnēji tika pierādīti matemātiķa Pjēra Delinja darbā 1974. gadā.

Google arī paziņoja, ka sistēma atkārtoti formalizējusi nesenu pierādījumu par galīgu laiku ilgu singularitātes jeb risinājuma “uzsprāgšanu” trīsdimensiju Navjē–Stoksa vienādojumos. Šī problēma ir saistīta ar vienu no septiņām Tūkstošgades balvas problēmām. Jautājums par to, vai šo vienādojumu gludi risinājumi ierobežotā laikā var kļūt singulāri, ir palicis neatrisināts aptuveni 90 gadus.

Sistēma palīdzējusi arī risināt Kortādes–Kumāra konjektūru informācijas teorijā, kas pirmoreiz izvirzīta 2013. gadā. Google un akadēmisko institūciju pētnieki ar šī ietvara palīdzību izstrādāja pierādījumu vispārīgā formā. Gemini modeļi palīdzēja iegūt analītiskas robežas un izveidot datoram pārbaudāmus sertifikātus.

Pierādījums tika formalizēts Lean 4 — programmēšanas valodā un pierādījumu asistentā, kas ļauj datoram pārbaudīt matemātiskus argumentus.

Neatkarīgi aģenti pārbauda cits cita darbu

Google pieeja balstās uz vairāku aģentu paralēlu darbu. Atsevišķas sistēmas tiek norīkotas piedāvātos risinājumus apstrīdēt un verificēt, tādējādi mazinot kļūdu risku, kas var rasties, vienam modelim ģenerējot garu spriešanas ķēdi.

Katrs specializētais aģents saņem tikai tā uzdevumam nepieciešamos failus un rīkus. Pēc tam neatkarīgi kritiķi un auditori pārbauda rezultātus, nepaļaujoties uz sākotnējā aģenta spriešanas procesu.

Šo pieeju Google izmantoja arī molekulārajā ķīmijā. Komanda, kurā darbojās 30 specializēti aģenti un fizikā balstīts simulators, no kodolmagnētiskās rezonanses jeb NMR datiem noteica molekulu struktūras. Sarežģītu etalona molekulu kopā sistēma sasniedza 95% precizitāti, pareizi nosakot labāko rezultātu, un 100% precizitāti, ja tika ņemti vērā trīs labākie varianti.

Rust pārveide paātrināja AV1 dekoderu

Teamwork ietvars sniedza rezultātus arī sistēmu inženierijā. Google aģenti uzņēmuma libgav1 AV1 video dekoderu pārveidoja no C++ uz aptuveni 170 000 Rust koda rindu. Plašā testu komplektā jaunā versija nodrošināja pilnīgu izvades atbilstību sākotnējai implementācijai.

Sākotnēji Rust versija darbojās aptuveni četras reizes lēnāk nekā C++ variants. Pēc tam, kad aģentiem tika piešķirta piekļuve profilēšanas rīkiem un uzdots uzlabot veiktspēju, Rust versija kļuva par 20–30% ātrāka nekā sākotnējā C++ implementācija gan x86_64, gan ARM procesoros.

Kādā citā projektā divu nedēļu kampaņas laikā aģenti pārveidoja atlikušo C++ kodu Zircon mikrokodolā par aptuveni 800 000 Rust koda rindu. Sistēma izturēja kodola vienību testus, un mikrokodols tika ielādēts ARM64 aparatūrā.

Uzlabota arī Google infrastruktūra

Google ziņoja par uzlabojumiem arī iekšējā infrastruktūrā. Aģentu vadīta plānošanas darbplūsma dažos aparatūras veidos par 24% samazināja TPU darba slodzes pārtraukšanu, vienlaikus saglabājot pakalpojumu līmeņa mērķus un klastera izmantošanas līmeni.

Uzņēmums Teamwork un iteratīvo programmēšanas darbplūsmu /boost padara pieejamu platformā Antigravity. Google arī izsludinājis pieteikšanos 10 000 akadēmisko pētnieku programmai, kurā sešus mēnešus būs pieejams augstākais lietošanas līmenis bez maksas.

Google norāda, ka nākotnē būs pieejamas arī citas specializētas darbplūsmas, tostarp rīki formālu pierādījumu veidošanai.