Vitalik Buterin proponuje język, który uczyni dowody AI czytelnymi

Współzałożyciel Ethereum, Vitalik Buterin, zaproponował nowy język programowania. Miałby kompilować się bezpośrednio do Lean lub HOL, innego asystenta do formalnych dowodów.

Ta idea rozwiązuje konkretną lukę w tym, jak ludzie czytają wyniki pracy sztucznej inteligencji. Sztuczna inteligencja generuje coraz większe bloki zautomatyzowanych dowodów, często szybciej niż jakikolwiek zespół ludzki napisałby je manualnie. Niewielu czytelników może gwałtownie potwierdzić, co te dowody rzeczywiście udowadniają.

Język przeznaczony tylko dla czytelników dowodów AI

Lean to asystent dowodów – oprogramowanie, którego matematycy i inżynierowie używają, by napisać dowody sprawdzane przez komputer linijka po linijce. Badacze Ethereum już go używają do weryfikacji kryptograficznego kodu i logiki konsensusu. Asystenci dowodów istnieją od prawie 60 lat, ale to przez cały czas niszowa dziedzina.

W swoim poście Buterin stwierdził, iż wewnętrzne kroki dowodu spełniają tylko jeden warunek. Tym warunkiem jest poprawność matematyczna, nic poza tym. Czytelnicy nigdy nie sprawdzają tej maszynerii bezpośrednio. Definicje i twierdzenia są inne, bo ludzie czytają je, by zrozumieć, co faktycznie gwarantuje dane oprogramowanie.

Buterin opisał podobny podział w majowym wpisie na blogu. Tam matematyczny dowód pokazuje, iż wydajny kod niskiego poziomu odpowiada osobnej, czytelnej specyfikacji, dzięki czemu jeden audyt pokrywa oba warianty jednocześnie.

Jego propozycja zbiega się w czasie z odbudową Ethereum, znaną też jako mapa drogowa Lean Ethereum. Badacze tworzą również formalnie zweryfikowany ZK-EVM, czyli wersję maszyny wirtualnej Ethereum z dowodami zerowej wiedzy, przez zastosowanie podobnych metod.

AI pisze dowody, ludzie sprawdzają twierdzenia

Duże modele językowe już potrafią pisać zrozumiałe dowody w Lean. Buterin wymienia Claude i Deepseek 4 Pro jako skuteczne narzędzia, obok Leanstral, mniejszego modelu dostrojonego pod Lean. Przykładem jest evm-asm, implementacja EVM zweryfikowana względem czytelnego wzorca. Taka umiejętność przypomina zdolności rozumowania, jakie deweloperzy pokazali w ostatnim wyzwaniu AI ogłoszonym przez Buterina. Testerzy rozwiązali je w kilka godzin.

Tu jednak stawka to nie tylko wygoda. Badacze bezpieczeństwa zauważyli w tym roku wzrost prób ataków z użyciem AI. Formalnie zweryfikowany kod może temu przeciwdziałać. Przyjaźniejszy język specyfikacji pozwoli deweloperom przeprowadzić audyt twierdzeń bez wczytywania się w otaczający je dowód.

Poza gronem badaczy Ethereum

Buterin publicznie testuje te pomysły i niedawno pokazał anonimowy billboard oparty na dowodach zerowej wiedzy. Demo pokazało, jak weryfikowalne twierdzenia mogą trafić z laboratoriów badawczych do praktycznych rozwiązań. Badacze zaczęli także formalnie weryfikować klientów konsensusu w Lean, aby wyłapać błędy na wczesnym etapie.

Jednak ten kierunek powiela znany schemat: oddziel szybki kod od czytelnych twierdzeń, a potem udowodnij ich zgodność.

Na razie nie istnieje żaden prototyp nowego języka, a Buterin nie określił dokładnej składni. Deweloperzy mogą uzgodnić jeden wspólny standard lub zaakceptować kilka niekompatybilnych dialektów. Ten wybór zdecyduje, jak gwałtownie kod weryfikowany przez AI trafi do zastosowań produkcyjnych.

BeInCrypto Polska - Vitalik Buterin proponuje język, który uczyni dowody AI czytelnymi