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

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

Dlatego dysponujemy technikami potwierdzającymi poprawność algorytmów, nawet jeśli (poprawna) implementacja na prawdziwej maszynie jest trudna.

— Raphael

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

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

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

„Strzeż się błędów w powyższym kodzie; udowodniłem tylko, że jest poprawny, a nie wypróbowałem”. ~ Donald Knuth

— Lew Reyzin

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