Świadkowie oprogramowania matematycznego

Podobnie jak wiele osób, jestem zapalonym użytkownikiem oprogramowania matematycznego, takiego jak Mathematica i Maple. Jednak coraz bardziej frustruje mnie wiele przypadków, w których takie oprogramowanie po prostu daje złą odpowiedź bez ostrzeżenia. Może się to zdarzyć podczas wykonywania wszelkiego rodzaju operacji, od prostych sum do optymalizacji wśród wielu innych przykładów.

Zastanawiałem się, co można zrobić z tym poważnym problemem. Potrzebny jest sposób, aby umożliwić użytkownikowi zweryfikowanie poprawności udzielonej odpowiedzi, aby mieć pewność co do tego, co zostało powiedziane. Jeśli chcesz znaleźć rozwiązanie od kolegi z matematyki, on / on może po prostu usiąść i pokazać ci ich pracę. Jednak w większości przypadków nie jest to możliwe do wykonania przez komputer. Czy komputer może zamiast tego dać ci proste i łatwe do sprawdzenia świadectwo poprawności odpowiedzi? Sprawdzanie może być konieczne przez komputer, ale mam nadzieję, że sprawdzenie algorytmu sprawdzania będzie znacznie łatwiejsze niż sprawdzenie algorytmu w celu przedstawienia świadka. Kiedy byłoby to wykonalne i jak dokładnie można to sformalizować

Podsumowując, moje pytanie jest następujące.

Czy możliwe jest przynajmniej teoretycznie, że oprogramowanie matematyczne może dostarczyć krótki sprawdzalny dowód wraz z odpowiedzią, o którą prosiłeś?

Trywialnym przypadkiem, w którym możemy to zrobić natychmiast, jest faktoryzacja liczb całkowitych lub wielu klasycznych problemów NP-zupełnych (np. Obwód hamiltonowski itp.).

cc.complexity-theory

— Społeczność
źródło

Czy możesz podać przykład, w którym uzyskana odpowiedź jest nieprawidłowa? Oczywiście możliwe jest wygenerowanie weryfikowalnego dowodu poprawności obliczeń, ale taki dowód nie musi być łatwy do sprawdzenia ręcznie, po prostu dlatego, że oprogramowanie zwykle wykorzystuje wysoce nietrywialne algorytmy, które są bardziej wydajne niż te najbardziej intuicyjne.

— Mahdi Cheraghchi,

Podałem dwa przykłady w pytaniu, ale kolory linków mogą nie być łatwo widoczne. Kliknij „sumy” lub „optymalizacja”.

W pewnym sensie, co zrobili Manuel Blum i Sampath Kannan w dl.acm.org/citation.cfm?id=200880 ?

— Andrej Bauer,

Możesz rzucić okiem na Algorytmy certyfikujące .

— Pratik Deoghare

tak, zbyt wiele symbolicznych systemów oprogramowania jest traktowanych jako „czarne skrzynki” i jest to również korporacyjna strategia ochrony tajemnic handlowych. (1) wypróbuj alternatywy typu open source (2) rozważ „najlepszą praktykę” inżynierii oprogramowania w „testowaniu jednostkowym”. krótko mówiąc, pomysł polegałby na stworzeniu „kontroli rozsądku” wyników, np. przez zastąpienie znanych wartości, inne manipulacje, inwersje itp. dobrze skonstruowanymi testami, jest mało prawdopodobne, aby zarówno formuła, jak i test zakończyły się niepowodzeniem w sposób, który dałby „fałszywie pozytywny”.

— dniu

Pojęcie „świadków” lub „sprawdzalnych dowodów” nie jest zupełnie nowe: jak wspomniano w komentarzach, szukaj pojęcia „świadectwa”. Przyszło mi do głowy trzy przykłady, jest ich więcej (w komentarzach i gdzie indziej):
- Kurt Mehlhorn opisał w 1999 r. Podobny problem w algorytmach geometrii obliczeniowej (np. Drobne błędy we współrzędnych mogą powodować duże błędy w wynikach niektórych algorytmów), rozwiązany w podobny sposób w bibliotece Leda , nalegając, aby każdy algorytm tworzył „certyfikat” swojej odpowiedzi oprócz samej odpowiedzi.
- Demaine, Lopez-Ortiz i Munro w 2000 r. Wykorzystali koncepcje certyfikatów (nazywają je „dowodami”), aby pokazać adaptacyjne dolne granice obliczeń związku i przecięcia (i różnicy, ale ta jest trywialna) posortowanych zbiorów. Nie wykluczaj ich pracy, ponieważ nie używali certyfikatów do ochrony przed błędami obliczeniowymi: wykazali, że nawet jeśli certyfikat może mieć rozmiar instancji liniowy w najgorszym przypadku, jest on często krótszy i dlatego można go „sprawdzić „w czasie podliniowym (dany losowy dostęp do danych wejściowych w postaci posortowanej tablicy lub drzewa B), a w szczególności w czasie krótszym niż wymagany do obliczenia takiego certyfikatu.
- Używam koncepcji certyfikatów w różnych innych problemach od czasu, gdy Ian Munro prezentował ich implementację na Alenex 2001 , aw szczególności w przypadku permutacji (przepraszam za bezwstydną wtyczkę, nadchodzi kolejna), gdzie certyfikat jest w najlepszym przypadku krótszy niż w najgorszym lub średnim przypadku, który daje skompresowaną strukturę danych dla permutacji. Również w tym przypadku sprawdzenie certyfikatu (tj. Kolejności) zajmuje co najwyżej liniowy czas, mniej niż jego obliczenie (tj. Sortowanie).
Ta koncepcja nie zawsze jest przydatna do sprawdzania błędów: istnieją problemy, w których sprawdzenie certyfikatu zajmuje tyle samo czasu, co jego wyprodukowanie (lub po prostu wygenerowanie wyniku). Przychodzą mi na myśl dwa przykłady, jeden trywialny i jeden skomplikowany, Blum i Kannan (wspomniani w komentarzach) podają inne.
- Certyfikat potwierdzający, że element nie znajduje się w nieposortowanej tablicy elementów, jest uzyskiwany w porównaniach i sprawdzany w tym samym czasie. $n$ $n$
- Certyfikat wypukłego kadłuba w dwóch i trzech wymiarach, jeśli punkty są podane w losowej kolejności, wymaga tyle bitów do zakodowania, ile porównań do obliczenia [FOCS 2009] (inna bezwstydna wtyczka).

Biblioteka Leda to najbardziej ogólny wysiłek (jaki znam), aby deterministyczne algorytmy generujące certyfikaty stały się normą w praktyce. Artykuł Bluma i Kannana to najlepszy wysiłek, jaki widziałem, aby uczynić go normą w teorii, ale pokazują granice tego podejścia.

Mam nadzieję, że to pomoże...

— Jeremy
źródło

Dziękuję, to jest bardzo interesujące. W odniesieniu do twojego punktu 2. Myślę, że mówię o czymś nieco innym. Problemem nie są błędy w kodzie, ale znane algorytmy mogą dać złą odpowiedź. Ponadto na poziomie przyziemnym nie wiem nawet, jak wyglądałby przydatny certyfikat dla wielu funkcji matematycznych. Na przykład dla nieskończonej sumy lub, powiedzmy, minimalizacji funkcji.

Aby być nieco jaśniejszym. Wydaje się, że bardzo trudno jest opracować poprawne algorytmy dla wielu problemów matematycznych. Jednak żyjemy z algorytmami, które mogą popełnić błąd bez ostrzeżenia (i faktycznie są możliwe do udowodnienia) z przyczyn praktycznych. Mam nadzieję, że nie jest (jak) trudne do ustalenia możliwe do sprawdzenia poprawności sprawdzania poprawności dla tego samego zestawu problemów.

Daleki jestem od mojej wiedzy, ale myślałem, że błędy obliczeniowe były generalnie spowodowane błędami zaokrąglania z wynikami pośrednimi (wyraźnie tak było w przykładach motywujących Leda) w przypadku podstawowych operacji (mnożenia, dzielenia itp.) Zamiast błędów w algorytmach. Myślałbym, że systemy algebraiczne, takie jak klon i matlab, unikają takich :(

— Jeremy,

To interesujące pytanie i być może ktoś tu wie na pewno ... jednak wiele niepoprawnych odpowiedzi, o których mówię, nie dotyczą obliczeń numerycznych, więc implikuje to przynajmniej prima facie, że problemy są więcej niż opisujesz. Nie znam złożoności obliczania limitów / nieskończonych kwot itp., Ale zakładam, że ogólnie są one najtrudniejsze w najgorszym przypadku, dlatego heurystyka, która czasami daje złą odpowiedź, jest potrzebna / przydatna. mathematica.stackexchange.com/questions/tagged/bugs nie jest pozbawiony informacji, aby dowiedzieć się, co dzieje się źle.

Teoretyczny CS ma koncepcję samokontroli, która dotyczy wielu problemów w algebrze liniowej. Jednym z podstawowych pomysłów jest to, że w przypadku wielu problemów rozwiązanie można sprawdzić (być może z odrobiną dodatkowych informacji) łatwiej niż można je obliczyć. Patrz np . Https://doi.org/10.1016/0022-0000(93)90044-W .

— Neal Young,