Nowa metoda weryfikacji AI ma oswoić czarne skrzynki w systemach krytycznych
Praca opublikowana w JAIR pokazuje, jak uczyć bariery bezpieczeństwa dla systemów AI bez znajomości ich wewnętrznej dynamiki.
Szybkie wchodzenie algorytmów sztucznej inteligencji do zastosowań krytycznych dla bezpieczeństwa, takich jak autonomiczna jazda czy opieka zdrowotna, coraz mocniej zderza się z pytaniem o wiarygodną weryfikację. Problem nie dotyczy już wyłącznie jakości predykcji ani skuteczności modeli w typowych scenariuszach, lecz tego, czy system da się formalnie uzasadnić jako bezpieczny w warunkach niepewności. Artykuł opublikowany w Journal of Artificial Intelligence Research przez Olivera Schöna z ETH Zürich, Zhenganga Zhonga i Sadegha Soudjaniego proponuje podejście, które ma odpowiedzieć właśnie na tę lukę: dane z działania systemu służą do uczenia certyfikatów barierowych, a następnie do weryfikacji bezpieczeństwa nawet wtedy, gdy sam system pozostaje czarną skrzynką.
Punkt wyjścia jest dobrze znany w inżynierii AI: klasyczne narzędzia formalnej weryfikacji wymagają zwykle jasnego modelu dynamiki systemu, tymczasem współczesne układy sterowane przez algorytmy uczące się często nie dają się łatwo opisać prostymi równaniami. Ich działanie zależy od danych, architektury modelu, kontrolera, niepewności środowiska i zmiennych, których projektanci nie zawsze potrafią wprost ująć w formalnym modelu. Autorzy pracy koncentrują się na systemach czarnoskrzynkowych o dyskretno-czasowej dynamice stochastycznej, czyli takich, których kolejne stany obserwuje się w krokach czasowych, a przejścia między nimi obarczone są losowością. To istotne, bo właśnie w takich warunkach proste zapewnienie, że system zachowa się bezpiecznie, przestaje być oczywiste.
Centralnym pojęciem proponowanej metody są certyfikaty barier sterowania. W uproszczeniu bariera ma oddzielać stany dopuszczalne od niebezpiecznych i dostarczać formalnego argumentu, że system nie przekroczy granicy bezpieczeństwa. Nowość polega na tym, że autorzy nie zakładają pełnej znajomości mechanizmu działania układu. Certyfikat jest uczony bezpośrednio ze zbioru trajektorii systemu, czyli z obserwacji tego, jak system przechodził przez kolejne stany. W praktyce przesuwa to ciężar z modelowania od podstaw na wykorzystanie danych operacyjnych. Dla obszarów takich jak autonomiczne pojazdy czy medycyna oznacza to kierunek, w którym weryfikacja może być bliższa realnemu zachowaniu systemu niż wyidealizowanemu opisowi matematycznemu.
Techniczny rdzeń rozwiązania opiera się na zanurzeniach średniej warunkowej oraz przestrzeniach Hilberta z reprodukującym jądrem, znanych jako RKHS. Autorzy wykorzystują te narzędzia do osadzenia danych z systemu w strukturze matematycznej, która pozwala operować na rozkładach i niepewności bez konieczności pełnego opisu dynamiki. Szczególnie ważny jest tu zbiór niejednoznaczności w RKHS. Może on zostać powiększony tak, aby wynik był bardziej odporny na zachowania spoza rozkładu danych treningowych. To element krytyczny, bo w systemach bezpieczeństwa samo dobre dopasowanie do obserwowanych trajektorii nie wystarcza. Istotne jest także to, co stanie się, gdy system napotka sytuacje odbiegające od wcześniejszych przykładów.
Autorzy deklarują, że ich ramy nie ograniczają się wyłącznie do prostego pytania, czy system pozostaje bezpieczny. W pracy przedstawiono wyniki teoretyczne dotyczące zastosowania metody do ogólniejszych klas specyfikacji logiki temporalnej wykraczających poza bezpieczeństwo. To ważne rozróżnienie: bezpieczeństwo często sprowadza się do unikania stanów zakazanych, ale systemy działające w świecie rzeczywistym mogą mieć bardziej złożone wymagania rozłożone w czasie. Mogą dotyczyć kolejności zdarzeń, trwałości pewnych warunków lub spełniania określonych własności w kolejnych etapach działania. Rozszerzenie w stronę logiki temporalnej sugeruje, że proponowana technika może być elementem szerszego aparatu weryfikacji zachowania systemów AI, a nie jedynie narzędziem do sprawdzania pojedynczej bariery.
Istotnym ograniczeniem wielu metod formalnych jest skala obliczeń. Autorzy wskazują, że typowy problem półnieskończenie wymiarowej optymalizacji, który pojawia się przy obliczaniu barier bezpieczeństwa opartych na danych, bywa w praktyce trudny do rozwiązania. W proponowanym podejściu zastosowano skończone rozwinięcie Fouriera, które pozwala przekształcić ten problem w program liniowy. Powstała w ten sposób bariera spektralna umożliwia wykorzystanie szybkiej transformaty Fouriera do efektywnego generowania problemu zrelaksowanego. Z perspektywy wdrażania metod weryfikacji to nie jest detal matematyczny, lecz warunek użyteczności: jeśli formalna gwarancja wymagałaby obliczeń nieprzystających do złożoności realnych systemów, pozostałaby głównie koncepcją akademicką.
Praca podkreśla również odporność dystrybucyjną proponowanych ram. W systemach uczonych z danych granica między tym, co model widział, a tym, czego nie widział, jest jednym z najbardziej wrażliwych punktów. Autorzy nie obiecują eliminacji niepewności, lecz budują mechanizm, który ma ją uwzględniać w formalnym procesie weryfikacji. Inflacja zbioru niejednoznaczności w RKHS ma chronić przed zbyt optymistycznym wnioskowaniem opartym wyłącznie na dostępnych trajektoriach. To podejście wpisuje się w praktyczny problem czarnych skrzynek: skoro nie znamy w pełni wnętrza systemu ani wszystkich przyszłych sytuacji, trzeba konstruować gwarancje z marginesem na odchylenia od danych.
Znaczenie pracy autorzy pokazują na dwóch studiach przypadku, w tym na systemie czarnoskrzynkowym z kontrolerem opartym na sieci neuronowej. To szczególnie istotny test deklarowanego celu, bo sieci neuronowe są jednym z powodów, dla których tradycyjna formalna weryfikacja traci elastyczność. Jeżeli metoda potrafi działać w scenariuszu, w którym kontroler jest neuronowy i traktowany jako czarna skrzynka, wzmacnia to argument, że może być przydatna dla nowej generacji systemów AI. Nie oznacza to jeszcze gotowego standardu dla rynku autonomicznych pojazdów czy technologii medycznych, ale wskazuje kierunek: bezpieczeństwo AI może być weryfikowane nie tylko przez analizę kodu i modelu, lecz także przez matematycznie ugruntowane uczenie certyfikatów z obserwowanego zachowania systemu.