Programowanie wnioskowania o własnym kodzie źródłowym

Inspiracją dla tego pytania jest następujące (niejasne) pytanie: Jakie są podstawy programowania / logiczne podstawy posiadania sztucznej inteligencji, która mogłaby rozumować własny kod źródłowy i go modyfikować?

To wcale nie jest rygorystyczne, więc oto moja próba wyciągnięcia z tego konkretnego pytania. Interesują mnie dwie rzeczy:

(A) Język programowania P, który może reprezentować własne programy i nimi manipulować jako program typu danych (np. Jako AST). (W razie potrzeby obiekt typu Program można przekonwertować na ciąg znaków, który jest tekstem poprawnego programu w tym języku. Byłoby to przeciwieństwo działania kompilatora.)

(B) Metoda uzasadnienia tego, co robi program w języku P. Oto dwa poziomy, o których myślę:

1. Inny język Q (z możliwościami dowodzenia twierdzeń), który modeluje to, co robi program P. Powinien być w stanie wyrazić i udowodnić takie stwierdzenia, jak „wynik działania Programu p jest foo”.
2. Sposób na uzasadnienie tego, co program p: Program robi w języku P. (Więc bierzemy P = Q powyżej.)

W jakim stopniu wdrożono coś takiego lub jaki jest postęp w tym kierunku? Jakie są praktyczne przeszkody? W świetle pierwotnej intencji pytania, jaki jest najlepszy sposób sformalizowania problemu?

*

Jak pokazują odpowiedzi (dzięki!), Zarówno (A), jak i (B1) można wykonać osobno, choć wydaje się, że robienie ich razem jest raczej pytaniem badawczym.

Oto kilka moich pierwszych przemyśleń na pytanie (ostrzeżenie: raczej niejasne). Zobacz także moje komentarze do odpowiedzi Martina Bergera.

Interesuje mnie język programowania modelujący ten sam język programowania, a nie prostszy (więc P = Q powyżej). Byłby to „dowód koncepcji” programu zdolnego do „rozumowania własnego kodu źródłowego”. Zależnie wpisane języki programowania mogą dawać gwarancje dotyczące wyników jego funkcji, ale nie liczy się to jako „rozumowanie własnego kodu źródłowego” bardziej niż „Witaj świecie!” liczy się jako quine w języku, który automatycznie wydrukuje nagi ciąg --- musi istnieć jakiś cytat / odnośnik. Tutaj analogiem jest typ danych reprezentujący Program.

Wydaje się, że jest to dość duży projekt - im prostszy język, tym trudniej jest wyrazić wszystko w nim; im bardziej skomplikowany język, tym więcej pracy trzeba wykonać, aby go wymodelować.

W duchu twierdzenia o rekurencji program może następnie „pobrać” własny kod źródłowy i zmodyfikować go (tj. Wygenerować zmodyfikowaną wersję samego siebie). (B2) następnie mówi nam, że program powinien móc wyrazić gwarancję na zmodyfikowany program (powinien on mieć możliwość ponownego wystąpienia, tj. Powinien być w stanie wyrazić coś o wszystkich przyszłych modyfikacjach -?).

Myślę, że pytasz o dwie różne rzeczy.

• Zdolność języka programowania do reprezentowania wszystkich swoich programów jako danych.
• Rozumowanie programów jako danych.

Do celów analitycznych warto je rozdzielić. Skoncentruję się na tym pierwszym.

Zdolność do reprezentowania języków programowania, manipulować (i bieg) swoje programy jako dane idzie pod określeniami takimi jak meta-programowania lub homoikoniczność .

W (niezręczny) sposób wszystkie dobrze znane języki programowania mogą wykonywać meta-programowanie, a mianowicie przy użyciu typu danych ciągu wraz z możliwością wywoływania programów zewnętrznych (kompilatora, konsolidatora itp.) Na ciągach znaków (np. Zapisując je do pliku najpierw system). Jednak prawdopodobnie nie to masz na myśli. Prawdopodobnie masz na myśli niezłą składnię. Ciągi nie są ładną składnią do reprezentacji programu, ponieważ prawie wszystkie ciągi nie reprezentują programów, tzn. Typ danych ciągów zawiera wiele „śmieci”, gdy są postrzegane jako mechanizm reprezentacji programu. Co gorsza, algebra operacji ciągów nie ma zasadniczo żadnego związku z algebrą budowy programu.

To, co prawdopodobnie masz na myśli, jest o wiele ładniejsze. Np. Jeśli jest programem, to to , ale jako dane, pod ręką do manipulacji i analizy. Jest to często nazywane cytatem . W praktyce oferta cenowa jest nieelastyczna, dlatego zamiast niej używamy quasi-oferty , która jest uogólnieniem oferty, w której oferta może zawierać „dziury”, w których można uruchamiać programy dostarczające dane do „wypełnienia” dziur. Na przykład to quasi-cytat reprezentujący warunek, w którym zamiast warunku mamy dziurę$P$P ⟨ i $\newcommand{\QUOTE}[1]{\langle #1\rangle}\QUOTE{P}$$P$[ ⋅ ] M ⟨ x > 0 ⟩ ⟨ i

(Zauważ, że jest normalnym programem (nie programem jako danymi), który zwraca cytowany program, tj. Program jako dane.) Aby to zadziałało, potrzebujesz typu danych do reprezentowania programów. Zazwyczaj ten typ danych nazywa się AST (abstrakcyjne drzewo składniowe) i można zobaczyć (quasi -) cytaty jako mechanizmy skrótów dla AST.$M$

Kilka języków programowania oferuje quasi-cytaty i inne funkcje meta-programowania. To Lisp z funkcją makrowania pionierem tej zdolności do traktowania programów jako danych. Być może niestety moc makr opartych na Lisp od dawna spoczywała w dużej mierze na minimalistycznej składni Lisp; dopiero w MetaML (1) okazało się, że nowoczesny język o bogatej składni jest zdolny do metaprogramowania. Od tego czasu MetaOCaml (2) (potomek MetaML, ważny dla jego przełomu w wciąż trwających poszukiwaniach rozwiązania problemu pisania programów jako dane), Template Haskell (3) i Converge (4) (pierwszy język do uzyskać wszystkie kluczowe funkcje metaprogramowania w mojej opinii) pokazały, że w wielu nowoczesnych językach programowania można umieścić metaprogramowanie. Ważne jest, aby zdać sobie sprawę, że możemy to zrobićdowolny język programowania i zamień go w język meta-programowania który jest wraz z możliwością reprezentowania (i oceny) własnych programów jako danych.L m p$L$$L_{mp}$$L$

Reprezentację wyniku działania programu, podanego jako dane, osiąga się przez dodanie funkcji która pobiera program (podany jako dane) jako dane wejściowe i uruchamia go , zwracając swój wynik. Np. Jeśli jest programem oceniającym na 17 i , wersja (quasi-) cytowana , tj. jako dane, to również również zwraca 17. Istnieją różne sposoby subtelności tutaj, które tutaj ignoruję, takie jak pytanie kiedy$\newcommand{\EVAL}{\mathsf{eval}}\EVAL(\cdot)$$P$$\QUOTE{P}$$P$$P$$\EVAL(\QUOTE{P})$programy meta-programowane są oceniane (co powoduje rozróżnienie między meta-programowaniem w czasie kompilacji a czasem wykonywania), co zrobić z typami lub błędnymi ocenami, co dzieje się ze zmiennymi powiązanymi i swobodnymi w procesie przechodzenia od do lub odwrotnie.$P$$\QUOTE{P}$

Jeśli chodzi o drugi wymiar, rozumowanie programów podanych jako dane. Gdy tylko przekształcisz programy w dane, są one „normalnymi” danymi i można je traktować jako dane. Możesz używać wszelkiego rodzaju technologii sprawdzających, np. Typy zależne lub umowy, interaktywne dowody twierdzeń lub zautomatyzowane narzędzia, jak zauważył Joshua. Będziesz jednak musiał przedstawić semantykę swojego języka w procesie rozumowania. Jeśli ten język, tak jak tego potrzebujesz, ma zdolności metaprogramowania, sprawy mogą stać się nieco trudne i nie wykonano wiele pracy w tym kierunku, przy czym (5) jest jedyną logiką programu w tym celu. Istnieją również prace Curry'ego-Howarda nad wnioskami dotyczącymi metaprogramowania (6, 7, 8). Zauważ, że te podejścia oparte na logice, a podejście oparte na typach (2) może rzeczywiście wyrażać właściwości, które zachowują się na wszystkich przyszłych etapach metaprogramowania. Poza (2) żaden z tych dokumentów nie został wdrożony.

Podsumowując: to, o co prosiłeś, zostało zaimplementowane, ale jest dość subtelne i wciąż istnieją otwarte pytania, w szczególności dotyczące typów i usprawnionego rozumowania.

1. W. Taha. Programowanie wieloetapowe: jego teoria i zastosowania .

2. W. Taha i MF Nielsen. Klasyfikatory środowiskowe .

3. T. Sheard i S. Peyton Jones. Szablon meta-programowania dla Haskell .

4. L. Tratt. Metaprogramowanie w czasie kompilacji w dynamicznie pisanym języku OO .

5. M. Berger, L. Tratt, Program Logics for Homogeneous Meta-Programming .

6. R. Davies, F. Pfenning, Analiza modalna obliczeń etapowych .

7. R. Davies, Podejście czasowo-logiczne do analizy czasu wiązania .

8. T. Tsukada, A. Igarashi. Logiczna podstawa dla klasyfikatorów środowiska .

Nie, nie ma obecnego systemu, który wykonuje wszystkie cztery kroki w twoim systemie. Jeśli chcesz zaprojektować system, jednym z pierwszych wymagań jest język homoiconic. Przynajmniej chciałbyś, aby Twój podstawowy język programowania był jak najmniejszy, aby po wejściu do systemu i rozpoczęciu samodzielnej interpretacji działał. Dlatego potrzebujesz interpretera międzykolistego, który był pionierem w seplenieniu. Inne języki również to zrobiły, ale istnieje wiele badań dotyczących seplenienia.

Pierwszym krokiem, jeśli chcesz to zrobić, jest posiadanie języka homoiconic, takiego jak Lisp, lub jakiegoś frameworka, w którym możesz przekonać się o działającym programie. Używa się do tego Lisp tylko dlatego, że możesz zdefiniować interpreter międzykręgowy w języku lub po prostu traktować swój kod jako dane. Najważniejsze jest traktowanie kodu jako danych. Dyskusje na temat tego, co homoiconic oznacza na wiki wiki c2.

Na przykład w Lisp typ danych „Program” jest prawidłowymi programami lisp. Przekazujesz programy lisp do tłumacza, a on coś oblicza. Zostanie odrzucony przez tłumacza, jeśli nie zaprogramujesz prawidłowego „Programu”.

Dlatego język homoiconic spełnia trzy z twoich wymagań. Możesz nawet w lisp zdefiniować ideę formalnego programu.

Czy możesz modelować seplenienie w seplenienie? Tak, często odbywa się to głównie jako ćwiczenie na końcu podręcznika programowania sepleniego, aby sprawdzić swoje umiejętności. SICP

W chwili obecnej czwarty numer jest pytaniem badawczym, a poniżej znalazłem próbę odpowiedzi na to pytanie.

Powiedziałbym, że istnieje wiele rodzajów programów, które próbują to zrobić. Poniżej znajdują się wszystkie programy, o których wiem.

• JSLint jest przykładem analizatora statycznego, który pobiera kod maszynowy lub inny język i wyraźnie szuka błędów. Następnie prosi programistę, aby to poprawił.

• Coq to środowisko, które pozwala określić dowody przy użyciu języka programowania. Ma taktykę, w której sugeruje sposoby rozwiązania problemu. Mimo to oczekuje się od człowieka wykonania pracy. Coq używa typów zależnych do pracy, a zatem jest bardzo teoretyczny. Jest bardzo popularny wśród informatyków i osób pracujących nad teorią typów homotopii.

• Z drugiej strony ACL2 to automatyczna przysłowiowa twierdzenie. Ten system sprawdzi wyciągi oparte na czymś, co programujesz.

• ACL2 i Coq mają wtyczkę oprogramowania, która łączy ich system z systemem uczenia maszynowego . Do szkolenia tych systemów wykorzystywane są wcześniej napisane programy. Z mojego zrozumienia systemy te dodają kolejną cechę, w której masz nie tylko swoją taktykę, ale sugerujesz twierdzenia, które pomagają w rozwoju dowodów.

Poniżej znajduje się podstawa tego, co oznacza twoje pytanie.

• gcc jest przykładem kompilatora optymalizacyjnego, który może brać siebie jako dane wejściowe, a następnie wypuszczać zoptymalizowaną wersję samego siebie. Idea kompilatora, który tłumaczy programy z jednej reprezentacji na drugą i poprawia prędkość z powodu niektórych flag optymalizacji jest bardzo dobrze zrozumiana. Po uruchomieniu kompilatora i wygenerowaniu prawidłowego kodu maszynowego można dodać optymalizację i ponownie skompilować kompilator, dzięki czemu jest on bardziej wydajną wersją samego siebie.

Jak wspomniano w odpowiedzi @ user217281728, istnieje pewien rodzaj maszyn związanych bardziej z wnioskami i sztuczną inteligencją, zwany maszynami Gödela

Maszyna Gödel to samodoskonalący się program komputerowy opracowany przez Jürgena Schmidhubera, który optymalnie rozwiązuje problemy. Wykorzystuje rekurencyjny protokół samodoskonalenia, w którym przepisuje własny kod, gdy może udowodnić, że nowy kod zapewnia bardziej optymalną strategię. Maszyna została wynaleziona przez Jürgena Schmidhubera, ale nosi imię Kurta Gödela, który zainspirował teorie matematyczne.

Przywołana publikacja Jürgena Schmidhubera na temat „Maszyny Goedela: uniwersalne rozwiązywanie problemów z samodzielnymi odniesieniami, które zapewniają optymalne samodoskonalenia”, (2006) arXiv: cs / 0309048v5

Sposób, w jaki maszyna działa w celu wdrożenia meta-uczenia się, składa się z dwóch etapów:

1. Uczenie się na podstawie danych (poziom 1, ucz się)
2. Wykorzystywanie wyuczonych danych do modyfikowania / optymalizacji kodu źródłowego / algorytmu (poziom 2, naucz się uczyć)

Ponieważ maszyna modyfikuje swoje własne źródło, jest autoreferencyjna, tzn. Ma właściwość samokodyfikacji (patrz także tutaj ).

W tym sensie może modyfikować sam algorytm uczenia się w ścisłym sensie (udowadniając optymalne samomodyfikacje). Występują problemy z odniesieniem do siebie i nierozstrzygalnością, które w tym przypadku przybierają postać:

.. maszyna Gödela z nieograniczonymi zasobami obliczeniowymi musi zignorować te samodoskonalenia, których skuteczności nie może udowodnić

Innymi językami (i powiązanymi z nimi maszynami tłumaczącymi), które mają właściwość auto-modyfikacji, są na przykład LISP .

W LISP kod i dane są wymienne lub kod źródłowy AST jest dostępny jako dane w programie LISP i może być modyfikowany jako dane. Z drugiej strony dane mogą być postrzegane jako AST dla niektórych kodów źródłowych.

aktualizacja

Istnieją również inne maszyny , takie jak maszyny samoregulujące (między innymi), które łączą samodzielne odniesienie , samoreprodukcję i autoprogramowanie .

Interesującym aspektem powyższego jest to, że samo-odniesienia nie jest problematyczne, w ogóle, a nie jest to konieczne, element samoreprodukcji / samoprogramujący automatów .

Więcej informacji (i więcej publikacji) można znaleźć w JP Moulin, CR Biologies 329 (2006)

abstrakcyjny

Żywe systemy potrafią odpowiednio reagować na nieprzewidywalne środowisko. Ten rodzaj samoorganizacji wydaje się działać jako maszyna samoregulująca, tj. Oprganizacja zdolna do samodzielnej modyfikacji. Do tej pory proponowane modele samoorganizacji istot żywych są funkcjami rozwiązań systemów różnicowych lub funkcjami przejściowymi automatów. Funkcje te są stałe i dlatego modele te nie mogą modyfikować swojej organizacji. Z drugiej strony informatyka proponuje wiele modeli posiadających właściwości systemów adaptacyjnych istot żywych, ale wszystkie te modele zależą od porównania celu i wyników oraz genialnego doboru parametrów przez programistów, podczas gdy programiści nie mają zamiaru ani wybór w żywych systemach.$\mathbb{m}_\mathbb{sp}$$\mathbb{M}_\mathbb{sp}$

Ten artykuł autorstwa Jurgena Schmidthubera może być interesujący:

http://arxiv.org/pdf/cs/0309048.pdf