Agenci Gemini 4 Carbon znaleźli programy kwantowe z dowodami poprawności w Lean, jeden według autorów tańszy o ponad 290 razy

Zespół z Google DeepMind i Google Quantum AI zaprezentował w preprincie na arXiv system, w którym agenci AI sami projektują programy kwantowe i dowodzą ich poprawności w asystencie dowodzenia Lean. Autorzy podają, że dla jednego z podprogramów, arcusa sinusa, koszt zasobów spadł ponad 290 razy względem punktu odniesienia. Większość tej oszczędności dały jednak obwody sprawdzalne klasycznie, a krok weryfikowany wyłącznie w Lean przyniósł ostatnie 11 procent. Autorzy zaznaczają też, że przy nowszym punkcie odniesienia zysk mógłby być bliższy 100 razy.

Jak działa system

Problem polega na tym, że algorytmy kwantowe da się sprawdzić na klasycznych komputerach tylko dla małych lub ograniczonych instancji. Autorzy preprintu piszą, że zbudowali bibliotekę programów kwantowych w Lean, w której agenci Gemini 4 piszą nowe programy względem formalnych specyfikacji i weryfikują zarówno poprawność, jak i koszt.

Według The Quantum Insider ludzie wybierali problemy, pisali specyfikacje i interpretowali wyniki. Gdy dowód się nie udawał, komunikaty o błędach wracały do agentów, które poprawiały pracę. Osobny mechanizm sprawdzał, czy agenci nie osłabili twierdzenia, nie zmienili zadania ani nie dodali nieuzasadnionych założeń.

Zespoły agentów dzieliły się wynikami przez wiki i spotykały na zaplanowanych wirtualnych konferencjach. Serwis Quantum Zeitgeist wskazuje, że w zespołach pracowały modele Gemini 4 Carbon, część jako pojedyncze agenty, część jako hierarchie z osobnymi rolami do projektu podprogramów, analizy błędów i dowodów.

Liczby z preprintu

W symulacji związanej z fuzją (zatrzymywanie cząstki alfa, 218 elektronów, 216 ustalonych protonów) liczba logicznych kubitów spadła z 5650 do 4374, a łączny koszt zmalał 10,9 razy. W fotochemii (187 elektronów, 47 jąder, jedna femtosekunda ewolucji) redukcja wyniosła 8,08 razy względem punktu odniesienia, który już zawierał wcześniejsze usprawnienia.

Dla związku I cytochromu P450, istotnego dla metabolizmu leków (63 elektrony, 58 orbitali), redukcja to 2,49 razy względem zaktualizowanego punktu odniesienia. W wyszukiwaniu równoległym autorzy w drugiej wersji preprintu podają poprawę do 2,55 razy przy znajdowaniu wszystkich oznaczonych elementów i do 1,22 razy przy znajdowaniu dowolnego z nich. Pierwsza wersja mówiła o 1,41 razy i tę liczbę cytuje The Quantum Insider.

Strona arXiv zaznacza, że wszystkie poprawy są liczone względem wcześniejszych punktów odniesienia, a nie jako wartości bezwzględne.

Zastrzeżenia autorów

The Quantum Insider podkreśla, że opisane programy nadal przekraczają to, co mają obsłużyć wczesne maszyny z korekcją błędów. Wiele zastosowań wymaga miliardów do biliardów operacji logicznych, a prognozy dla takich maszyn mówią o około milionie, więc potrzeba jeszcze kilku rzędów wielkości poprawy.

Są też ograniczenia samej metody. Przypisanie zasług między zespołami agentów bywało trudne, a w fotochemii wymóg poprawności dla każdego stanu wejściowego, także fizycznie niepoprawnego, zawężał pole optymalizacji. W przypadku P450 reprezentacja była ustalona, co wykluczało zyski ze zmiany jej postaci.

Co dalej

Autorzy wskazują kolejne kierunki: kody korekcji błędów, przemieszczanie informacji między kubitami, układ chipów i miary kosztu dopasowane do sprzętu. Dla czytelnika to sygnał, że agentów AI próbuje się łączyć z formalnym dowodem, choć dowód gwarantuje tylko zgodność ze specyfikacją. Biblioteka Lean nie jest jeszcze publiczna, więc do czasu jej otwarcia wartości kosztu pozostają twierdzeniem autorów.