Potężne algorytmy, które są zbyt trudne do wdrożenia - jak się upewnić, że mają rację?

9

Odnoszę się tutaj do pytania: potężne algorytmy zbyt złożone, aby je zaimplementować .

Jeśli algorytm jest potężny, ale zbyt skomplikowany, aby go wdrożyć, skąd możesz mieć pewność, że algorytm jest poprawny? Bez implementacji nie będzie można przetestować algorytmu w scenariuszu ze świata rzeczywistego, a tak złożony algorytm może zawierać błędy, które mogą unieważnić algorytm.

Tego nie rozumiem; jeśli masz techniki, aby udowodnić poprawność algorytmu, to algorytm już go implementuje, prawda? Albo w jaki sposób możemy być pewni, że technika sprawdzania jest poprawna?

Przepraszam, jeśli zabrzmi elementarnie!

Aktualizacja z Kaveha (odtworzona tutaj, ponieważ argument jest lepszy!):

Jeśli możesz formalnie udowodnić poprawność algorytmu w systemie formalnym, takim jak Coq, możesz również wyodrębnić algorytm (ponieważ zasadniczo zaimplementowałeś algorytm), ale kluczowym faktem jest to, że w przypadku większości algorytmów nie dajemy formalnych dowodów potwierdzających poprawność algorytmu, używamy nieformalnych dowodów poprawności. Dowody mogą być fałszywe, co zdarza się od czasu do czasu, a nawet formalny dowód poprawności nie zapewni nam absolutnej pewności, że algorytm jest poprawny.

ds.algorithms implementation Grawiton
źródło
6
Dlatego dysponujemy technikami potwierdzającymi poprawność algorytmów, nawet jeśli (poprawna) implementacja na prawdziwej maszynie jest trudna.
Raphael
9
Zgadzam się z Raphaelem. Wydaje się, że pytanie opiera się na założeniu, że poprawność algorytmu zwykle dowodzi się poprzez jego wdrożenie, ale tak nie jest. Udowodnienie poprawności algorytmu i implementacja algorytmu to zupełnie inne rzeczy, a jedna z nich nie implikuje drugiej w żadnym kierunku.
Tsuyoshi Ito
8
Proste algorytmy ze złożonymi dowodami poprawności - skąd wiesz, że mają rację? To, że algorytm działa na przykładach testów, nie oznacza, że ​​działa na wszystkich danych wejściowych.
Peter Shor
2
Zgadzam się z większością komentarzy, ale myślę, że brakuje im kluczowej kwestii. Jeśli możesz formalnie udowodnić poprawność algorytmu w systemie formalnym, takim jak Coq, możesz również wyodrębnić algorytm (ponieważ zasadniczo zaimplementowałeś algorytm), ale kluczowym faktem jest to, że w przypadku większości algorytmów nie dajemy formalnych dowodów potwierdzających poprawność algorytmu, używamy nieformalnych dowodów poprawności. Dowody mogą być fałszywe, co zdarza się od czasu do czasu, a nawet formalny dowód poprawności nie zapewni nam absolutnej pewności, że algorytm jest poprawny.
Kaveh
5
„Strzeż się błędów w powyższym kodzie; udowodniłem tylko, że jest poprawny, a nie wypróbowałem”. ~ Donald Knuth
Lew Reyzin

Odpowiedzi:

11

Kilka lat temu odbyła się (raczej ostra) debata na podobny temat. Wszystko zaczęło się, gdy kilka skomplikowanych dowodów okazało się niepoprawnych, a niektórzy badacze zaczęli wątpić w samą naturę dowodów (cóż, powinienem był powiedzieć „możliwa do udowodnienia kryptografia”, ale ze względu na ogólność nie zrobiłem tego) . Obie strony kontrowersji oskarżyły drugą stronę o niezrozumienie pojęć. Oto link, aby uzyskać więcej informacji .

Dowody są naszymi (matematycznymi) narzędziami do udowodnienia, że ​​twierdzenia / algorytmy są poprawne, ale gdy stają się zbyt złożone, możemy się poślizgnąć i udowodnić, że coś jest nie tak. Ostatnich 100 lub tak stronie dowód na P ≠ NP jest doskonałym przykład. Nie wyklucza to jednak samej natury dowodów: nic z nimi nie jest nie tak.

Ostatni punkt: myślę, że studiowanie filozofii nauki da nam więcej wglądu w to. (Pod podanym linkiem patrz punkt „ Skąd wiemy, czy matematyczny dowód jest poprawny? ”)

MS Dousti
źródło