Maszyna Gödla - Gödel machine

Maszyna Gödel jest hipotetyczny self-poprawa program komputerowy , który rozwiązuje problemy w sposób optymalny. Używa rekurencyjnego protokołu samodoskonalenia, w którym przepisuje swój własny kod, gdy może udowodnić, że nowy kod zapewnia lepszą strategię. Maszyna została wynaleziona przez Jürgena Schmidhubera (po raz pierwszy zaproponowana w 2003 roku), ale jej nazwa pochodzi od Kurta Gödla, który zainspirował teorie matematyczne.

Maszyna Gödla jest często omawiana podczas rozwiązywania problemów związanych z meta-learningiem , znanym również jako „nauka uczenia się”. Aplikacje obejmują automatyzację ludzkich decyzji projektowych i transfer wiedzy między wieloma powiązanymi zadaniami i mogą prowadzić do projektowania bardziej solidnych i ogólnych architektur uczenia się. Choć teoretycznie możliwe, nie stworzono pełnej implementacji.

Maszyna Gödel jest często porównywana z Marcus Hutter „s AIXItl , innej formalnej specyfikacji na sztucznej inteligencji ogólnej . Schmidhuber wskazuje, że maszyna Gödel mogłaby zacząć od implementacji AIXItl jako swojego początkowego podprogramu i dokonać samodzielnej modyfikacji po znalezieniu dowodu, że inny algorytm dla jej kodu wyszukiwania będzie lepszy.

Ograniczenia

Tradycyjne problemy rozwiązywane przez komputer wymagają tylko jednego wejścia i zapewniają pewne wyjście. Komputery tego rodzaju miały wbudowany swój pierwotny algorytm. Nie uwzględnia to dynamicznego środowiska naturalnego, a zatem było celem maszyny Gödla do pokonania.

Jednak maszyna Gödla ma swoje własne ograniczenia. Zgodnie z pierwszym twierdzeniem o niezupełności Gödla każdy formalny system, który obejmuje arytmetykę, jest albo wadliwy, albo dopuszcza twierdzenia, których nie można udowodnić w systemie. Dlatego nawet maszyna Gödla z nieograniczonymi zasobami obliczeniowymi musi ignorować te samodoskonalenia, których skuteczności nie może udowodnić.

Interesujące zmienne

Istnieją trzy zmienne, które są szczególnie przydatne w czasie wykonywania maszyny Gödla.

W pewnym momencie zmienna będzie miała binarny odpowiednik . Jest to stale zwiększane przez cały czas pracy maszyny. ${\ displaystyle t}$ ${\ displaystyle {\ text {czas}}}$ ${\ displaystyle t}$

Wszelkie dane wejściowe przeznaczone dla maszyny Gödela ze środowiska naturalnego są przechowywane w zmiennej . Jest prawdopodobne, że będzie miał różne wartości dla różnych wartości zmiennej . ${\ displaystyle x}$ ${\ displaystyle x}$ ${\ displaystyle {\ text {czas}}}$

Dane wyjściowe maszyny Gödela są przechowywane w zmiennej , gdzie w pewnym momencie byłby wyjściowy ciąg bitów . ${\ displaystyle y}$ ${\ Displaystyle y (t)}$ ${\ displaystyle t}$

W dowolnym momencie , gdy celem jest maksymalizacja przyszłego sukcesu lub użyteczności. Typowa funkcja użyteczności jest zgodna ze wzorem : ${\ displaystyle t}$ ${\ Displaystyle (1 \ równoważnik t \ równoważnik T)}$ ${\ Displaystyle u (s, \ mathrm {kop.}): S \ razy E \ rightarrow \ mathbb {R}}$

{\ Displaystyle u (s, \ mathrm {koperta}) = E _ {\ mu} {\ Bigg [} \ sum _ {\ tau = {\ tekst {czas}}} ^ {T} r (\ tau) \ mid s, \ mathrm {Env} {\ Bigg]}}

gdzie jest wartością wejściową nagrody o wartości rzeczywistej (zakodowaną w ) w czasie , oznacza warunkowy operator oczekiwania w odniesieniu do jakiejś prawdopodobnie nieznanej dystrybucji ze zbioru możliwych dystrybucji ( odzwierciedla wszystko, co wiadomo o możliwych probabilistycznych reakcjach środowiska), a wyżej wymienione zależy od stanu , który jednoznacznie identyfikuje bieżący cykl. Pamiętaj, że bierzemy pod uwagę możliwość wydłużenia oczekiwanej żywotności poprzez odpowiednie działania. ${\ displaystyle r (t)}$ ${\ Displaystyle s (t)}$ ${\ displaystyle t}$ ${\ Displaystyle E _ {\ mu} [\ cdot \ mid \ cdot]}$ ${\ displaystyle \ mu}$ ${\ displaystyle M}$ ${\ displaystyle M}$ ${\ displaystyle {\ text {czas}} = \ operatorname {czas} (s)}$ ${\ displaystyle s}$

Instrukcje używane przez techniki dowodowe

Charakter sześciu poniższych instrukcji modyfikujących dowód uniemożliwia wstawienie niepoprawnego twierdzenia do dowodu, tym samym trywializując weryfikację dowodu.

get-axiom ( n )

Dołącza n- ty aksjomat jako twierdzenie do bieżącej sekwencji twierdzeń. Poniżej znajduje się wstępny schemat aksjomatów:

Aksjomaty sprzętowe formalnie określają, w jaki sposób komponenty maszyny mogą się zmieniać z jednego cyklu do drugiego.
Aksjomaty nagród określają obliczeniowy koszt instrukcji sprzętowych i fizyczny koszt działań wyjściowych. Powiązane aksjomaty również definiują żywotność maszyny Gödla jako wielkości skalarne reprezentujące wszystkie korzyści / koszty.
Aksjomaty środowiskowe ograniczają sposób, w jaki nowe dane wejściowe x są wytwarzane ze środowiska, w oparciu o poprzednie sekwencje danych wejściowych y .
Aksjomaty niepewności / manipulacji na łańcuchach Aksjomaty to standardowe aksjomaty arytmetyki, rachunku różniczkowego, teorii prawdopodobieństwa i manipulacji na łańcuchach, które pozwalają na tworzenie dowodów związanych z przyszłymi wartościami zmiennych w maszynie Gödla.
Aksjomaty stanu początkowego zawierają informacje o tym, jak zrekonstruować części lub całość stanu początkowego.
Aksjomaty użyteczności opisują ogólny cel w postaci funkcji użyteczności u .

reguła zastosuj ( k , m , n )

Przyjmuje indeks k reguły wnioskowania (takiej jak Modus tollens , Modus ponens ) i próbuje zastosować go do dwóch wcześniej udowodnionych twierdzeń m i n . Wynikowe twierdzenie jest następnie dodawane do dowodu.

twierdzenie o usunięciu ( m )

Usuwa twierdzenie zapisane pod indeksem m w bieżącym dowodzie. Pomaga to złagodzić ograniczenia pamięci spowodowane przez zbędne i niepotrzebne twierdzenia. Powyższa funkcja reguły stosowania nie może już odwoływać się do usuniętych twierdzeń .

set-switchprog ( m , n )

Zastępuje switchprog S ^s_{m n} , pod warunkiem, że jest niepusty podciąg o S ^s .

czek()

Weryfikuje, czy cel wyszukiwania dowodowego został osiągnięty. Twierdzenie o celu stwierdza, że biorąc pod uwagę obecną aksjomatyzowaną funkcję użyteczności u (pozycja 1f), użyteczność przejścia z p na bieżący switchprog byłaby wyższa niż użyteczność kontynuowania wykonywania p (co powodowałoby ciągłe poszukiwanie alternatywnych przełączników). Jest to zademonstrowane w poniższym opisie zdekodowanej funkcji check () dla maszyny Gödla:

{\ displaystyle D_ {KA} = {\ Frac {d _ {\ text {pory}}} {3}} u = {\ frac {d _ {\ text {por}}} {3}} {\ sqrt {\ frac {8 \ kappa NT} {\ pi M_ {A}}}}}

state2theorem ( m , n )

Przyjmuje dwa argumenty, m i n , i próbuje przekształcić zawartość S _{m: n} w twierdzenie.

Przykładowe aplikacje

Ograniczona czasowo optymalizacja NP-trudna

Początkowe dane wejściowe do maszyny Gödla to reprezentacja połączonego grafu z dużą liczbą węzłów połączonych krawędziami o różnych długościach. W określonym czasie T powinien znaleźć ścieżkę cykliczną łączącą wszystkie węzły. Jedyna rzeczywista zapłata nastąpi w czasie T . Jest równa 1 podzielonej przez długość najlepszej znalezionej dotychczas ścieżki (0, jeśli żadna nie została znaleziona). Nie ma innych danych wejściowych. Produktem ubocznym maksymalizacji oczekiwanej nagrody jest znalezienie najkrótszej możliwej do znalezienia ścieżki w ograniczonym czasie, biorąc pod uwagę początkowe odchylenie.

Szybkie dowodzenie twierdzeń

Jak najszybciej udowodnić lub obalić, że wszystkie liczby całkowite parzyste> 2 są sumą dwóch liczb pierwszych ( przypuszczenie Goldbacha ). Nagroda wynosi 1 / t , gdzie t to czas potrzebny na wyprodukowanie i zweryfikowanie pierwszego takiego dowodu.

Maksymalizacja oczekiwanej nagrody dzięki ograniczonym zasobom

Poznawczy robot, który potrzebuje co najmniej 1 litr benzyny na godzinę współdziała z częściowo nieznanym środowisku, starając się znaleźć ukryte, ograniczone magazyny benzyna od czasu do czasu zatankować swój zbiornik. Jest nagradzany proporcjonalnie do swojego życia i umiera po co najwyżej 100 latach lub gdy tylko jego zbiornik jest pusty lub spadnie z urwiska i tak dalej. W probabilistyczne reakcje otoczenia są początkowo nieznany, ale zakłada się, że próbki z axiomatized Szybkości Prior, zgodnie z którym trudno obliczyć reakcje otoczenia są mało prawdopodobne. Pozwala to na obliczalną strategię tworzenia niemal optymalnych prognoz. Jednym z produktów ubocznych maksymalizacji oczekiwanej nagrody jest maksymalizacja oczekiwanego czasu życia.

Zobacz też

Twierdzenia o niezupełności Gödla

Languages

In other projects