Przykład algorytmu bez dowodu poprawności

18

Mamy logikę Hoare'a. Dlaczego wciąż jest możliwe, że algorytm ma rację, ale nie ma dowodów na jego poprawność? Załóżmy, że algorytm jest wyrażony w C. Następnie możemy argumentować krok po kroku, że robi to, co powinien.

Więc moje pytanie brzmi:

Podaj przykład algorytmu, który jest odpowiedni, ale nie ma dowodu poprawności.

EDYCJA: Myślę, że trochę tła może pomóc wyjaśnić, dokąd zmierzam. Pozwól, że zacytuję Scott Aaronson:

Od lat siedemdziesiątych pojawiły się spekulacje, że P NP może być niezależny (to znaczy nie do udowodnienia ani obalenia) od standardowych systemów aksjomatów dla matematyki, takich jak teoria mnogości Zermelo-Fraenkla. Dla jasności oznaczałoby to również jedno

  1. algorytm wielomianowy dla problemów z kompletnym NP nie istnieje, ale nigdy nie możemy tego udowodnić (przynajmniej nie w naszych zwykłych systemach formalnych), albo

  2. algorytm wielomianowy czasu dla problemów NP-zupełny nie istnieją, ale też nie możemy udowodnić, że to działa, czy nie możemy udowodnić, że zatrzymuje się w czasie wielomianowym.

Mam na myśli drugą możliwość. Ponieważ Aaronson może tak pewnie wymienić tę możliwość, myślę, że musi istnieć przykład typu 2. Dlatego zadaję to pytanie. Ale wydaje się, że szybka i jasna odpowiedź nie jest widoczna.

Zirui Wang
źródło
17
Co to znaczy powiedzieć, że algorytm jest poprawny, jeśli nie mamy dowodu poprawności?
David Richerby
14
Czy masz na myśli „dowód poprawności jest niemożliwy” czy „nikt nie udowodnił, że jest poprawny”?
gnasher729
12
Algorytmy nie muszą być poprawne ... załóżmy, że masz: (1) rano umieść puste wiadro na parapecie. (2) zdejmij go wieczorem. (3) zmierzyć objętość wody w wiadrze. (4) powtórz następnego dnia rano. Jest to opis algorytmu, ale nie opisuje niczego, co mogłoby bez odcinka być nazywane „poprawnym”. Co ciekawe, większość kodu programistycznego na świecie jest napisana w ten szczególny sposób: po prostu nie dotyczy poprawności tego, co robi.
wvxvw
@wvxvw Jestem więc zdezorientowany, co to znaczy, że algorytm jest „poprawny”? Jeśli robi to, co było zamierzone, czy to nie znaczy, że jest poprawne? Jeśli celem twojego scenariusza było znalezienie średniej ilości wody zebranej w wiadrze podczas opadów deszczu, czy algorytm nie byłby w tym przypadku poprawny na każdy dzień?
Abdul
8
@chi, którego nie rozumiesz ... nie chodzi o to, że programiści nie dbają o poprawność swojego kodu, ale o to, że w przypadku niektórych algorytmów pojęcie „poprawności” nie ma zastosowania. Weźmy aplikację .NET WindowsForms, która coś mówi: „umieść ten przycisk z tą etykietą w tej pozycji, a następnie umieść ten inny przycisk w tej innej pozycji i tak dalej ...” - może istnieć pewna interpretacja tego, co to program robi, zgodnie z którym to, co robi, może być uznane za (nie) poprawne (np. grafik mówi, że „wygląda brzydko”), ale to jest tak daleko, jak to możliwe.
wvxvw

Odpowiedzi:

50

Oto algorytm funkcji tożsamości:

  • Dane wejściowe: n
  • Sprawdź, czy ty ciąg binarny koduje dowód 0 > 1 w ZFC, a jeśli tak, wyślij n + 1n0>1n+1
  • W przeciwnym razie wyjdź n

Większość ludzi podejrzewa, że ​​ten algorytm oblicza funkcję tożsamości, ale nie wiemy i nie możemy tego udowodnić w powszechnie przyjętym środowisku matematycznym, ZFC .

Yuval Filmus
źródło
2
Czy na pewno Sprawdź, czy ty ciąg binarny koduje dowód 0 > 1 w ZFCn0>1 jest algorytmem?
Dmitrij Grigoriew
23
Nie, ale sprawdzenie można zdecydowanie zaimplementować algorytmicznie (tj. Za pomocą maszyny Turinga). W rzeczywistości jest to jedno z wymagań, jakie mamy dla systemów dowodu - że ważność dowodu może być sprawdzana algorytmicznie.
Yuval Filmus
6
@Puppy ZFC potwierdza . Ale może również udowodnić 0 > 1, jeśli (f) jest niespójny. Prawie wszyscy sądzi, że ZFC jest konsekwentny, oczywiście, ale z powodu twierdzeń o niekompletności nie możemy tego wiedzieć na pewno. ¬(0>1)0>1
chi
1
@Nanielski Wcale nie. Na przykład możesz łatwo udowodnić poprawność każdego algorytmu podręcznika. Algorytm ten różni się tym, że opiera się na spójności ZFC, czego nie może udowodnić sam ZFC.
Yuval Filmus
1
@ Nataniel: Jeśli chcesz, pozwól nam kontynuować tę dyskusję na czacie .
user21820
9

Większość algorytmów nie została udowodniona w logice Hoare'a. Głównym powodem jest to, że takie dowody poprawności są wyjątkowo drogie od stycznia 2017 r., Prawdopodobnie o kilka rzędów wielkości w porównaniu z „zwykłym” programowaniem. Trwa wiele prac nad obniżeniem tego kosztu dzięki automatyzacji, ale jest to trudna walka.

Innym powodem, dla którego algorytm może nie mieć dowodu poprawności, a który jest bardziej odpowiedni w praktyce niż zjawiska niekompletności, o których wspominali Yuval i chi, jest to, że możemy nie wiedzieć, czym jest ta specyfikacja. Ten problem ma dwa wymiary.

  • Klienci nie wiedzą, czego chcą. Jest to dobrze znany problem w inżynierii oprogramowania, a inżynierowie oprogramowania opracowali wiele sposobów rozwiązania tego problemu.

  • nprzekraczające liczby naturalne, a przeciwnicy to wielomianowe probabilistyczne maszyny Turinga. Według mojej najlepszej wiedzy (proszę mnie poprawić, jeśli się mylę) istnieje rozbieżność między teorią a praktyką, a konkretne algorytmy, takie jak AES i SHA256, nie mieszczą się w zakresie tych teoretycznych specyfikacji. Nie sądzę, aby istniała pełna specyfikacja takich algorytmów, dlatego w zasadzie nie możemy ich zweryfikować w sensie np. Logiki Hoare'a.

Martin Berger
źródło
AES wchodzi w zakres definicji bezpieczeństwa kryptograficznego. (Musisz używać konkretnych definicji zabezpieczeń zamiast definicji asymptotycznych, ale powinieneś to robić, jeśli chcesz bezpieczeństwa w praktyce.)
DW
@DW Ciekawe. Nie byłam tego świadoma. Jak obchodzi się asymptotyczną naturę kryptografii teoretycznej? Czy możesz wskazać mi artykuł na ten temat? Co z konkretnymi funkcjami kryptograficznymi funkcji skrótu?
Martin Berger
en.wikipedia.org/wiki/Concrete_security i odnośniki tam wymienione. Funkcje mieszania są bardziej złożonym przypadkiem, ponieważ zależy to od tego, do czego ich używasz - ale złożoności są w dużej mierze prostopadłe do asymptotycznego bezpieczeństwa w porównaniu do konkretnego bezpieczeństwa.
DW
2
Do szyfrowania potrzebne są dwa algorytmy: jeden szyfrujący, jeden odszyfrowujący. Jeden z nich nie może sam być poprawny. Mogą być poprawne tylko w parze (udowodnisz, że odszyfrowanie zaszyfrowanego wejścia powoduje powstanie oryginału). Ale jeśli chodzi o szyfrowanie, chcesz, aby było niewykrywalne, a tego nie można złapać za pomocą „poprawności”.
gnasher729
1
@DW Muszę się nieco nie zgadzać. Podczas gdy dokumenty Rogaway i Bellare są świetne, sugerują, że w jakikolwiek sposób uwzględniają dowody bezpieczeństwa prymitywów, które wprowadzają w błąd. Oba artykuły dotyczą przede wszystkim protokołów (tzn. Zakładają, że prymitywy, takie jak AES, SHA, RSA itp.) Są bezpieczne, a następnie dowodzą tego. Podstawowy problem polegający na udowodnieniu, że prymitywowie są bezpieczni, pozostaje. Jeśli masz jakieś referencje potwierdzające bezpieczeństwo prymitywów, byłbym zainteresowany. Drugi artykuł na przykład zakłada, że ​​RSA jest trudny, co stanowi bardzo otwarty problem.
DRF
5

Jest to związane z niekompletnością podstawowej logiki. Rzeczywiście, logika Hoare'a zawiera zwykle zasadę osłabienia lub „post-post”

PP{P}c{Q}QQ{P}c{Q}
PP,QQ należy udowodnić za pomocą logiki leżącej u podstaw, zwykle logiki pierwszego rzędu (FOL) z pewną teoretyczną aksjatyzacją, jak Zermelo-Fraenkel (ZF).

P(n)P(0)P(1)P(2)nN. P(n)

MnP(n)Mn. P(n)Mn. P(n)

chi
źródło
5

Problem: Wydrukuj „Tak”, jeśli każda liczba parzysta ≥ 4 jest sumą dwóch liczb pierwszych, i „Nie”, jeśli liczba parzysta ≥ 4 nie jest sumą dwóch liczb pierwszych.

Algorytm: Drukuj „Tak”

Większość ludzi uważa, że ​​algorytm jest poprawny. Nie jest znane dowód, i to jest całkiem możliwe, że nie ma żadnego dowodu.

gnasher729
źródło
3

Każdy algorytm, który jest poprawny, ale nie wiemy, ile czasu zajmuje jego uruchomienie, można przekształcić w algorytm, który zatrzymuje się w gwarantowanym czasie, ale nie jesteśmy pewni, czy jest poprawny.

nn+10log(n)20n

P=NP

Dan Brumleve
źródło