Dowód użycia asystenta w badaniach teorii złożoności?

Biorąc pod uwagę tematy poruszane na konferencji, takie jak STOC, czy naukowcy zajmujący się algorytmem lub złożonością aktywnie korzystają z COQ lub Isabelle? Jeśli tak, to jak wykorzystują go w swoich badaniach? Zakładam, że większość ludzi nie użyłaby takich narzędzi, ponieważ dowody byłyby zbyt niskie. Czy ktoś używa tych asystentów dowodu w sposób, który ma kluczowe znaczenie dla ich badań, w przeciwieństwie do miłego suplementu?

Jestem zainteresowany, ponieważ mógłbym zacząć uczyć się jednego z tych narzędzi i byłoby fajnie poznać je w kontekście dowodów na zmniejszenie, poprawność lub czas pracy.

— nish2575
źródło

Czy chcesz wykluczyć „Teorię B”, a zwłaszcza teorię języków programowania? Rozumiem, że asystenci

— ds

— Poszukałem

O ile mi wiadomo, większość teorii A należy do tej samej kategorii, co większość matematyki: do tej pory dodano kilka fundamentów do tych systemów, więc najciekawsze twierdzenia wymagałyby znacznego wysiłku, aby najpierw opracować infrastruktura do wdrożenia niezbędnych definicji. Istnieje kilka interesujących fragmentów teorii automatów, które zostały sformalizowane, więc może to być miejsce do patrzenia.

— András Salamon

Wyniki w teorii złożoności są zwykle możliwe do udowodnienia w znacznie słabszych systemach, zwykle nie potrzebujesz nawet PA. Powiedziałbym, że Coq i Isabeller nie nadają się zbyt dobrze do teorii złożoności. Istnieją prawie formalne szkice dowodowe, takie jak te w książce Cooka i Nguyena, ale głównym celem jest udowodnienie ich w systemie dowodu związanym z klasami złożoności. Dlaczego ktoś chciałby to udowodnić, mówiąc: Przełączanie lematu w Coq, kiedy można to udowodnić w znacznie słabszych systemach?

— Kaveh

@Kaveh Słabość / siła różnych systemów dowodowych nie jest tu problemem: chcielibyśmy formalnie zweryfikować dowody w teorii złożoności z tego samego powodu, dla którego chcielibyśmy zweryfikować programy: mieć wyższy stopień niezawodności. Ponadto interesującym wyzwaniem jest rozszerzenie teorii przysłowiowej, aby wygodniej obsługiwać dowody teorii złożoności.

— Martin Berger

Odpowiedzi:

Ogólna zasada jest taka, że im bardziej abstrakcyjna / egzotyczna matematyka ma być mechanizowana, tym łatwiej. I odwrotnie, im bardziej konkretna / znajoma jest matematyka, tym trudniej będzie. Tak więc (na przykład) rzadkie zwierzęta, takie jak predykcyjna topologia bez punktów, są znacznie łatwiejsze do zmechanizowania niż zwykła topologia metryczna.

Początkowo może się to wydawać nieco zaskakujące, ale dzieje się tak głównie dlatego, że konkretne obiekty, takie jak liczby rzeczywiste, uczestniczą w wielu różnorodnych strukturach algebraicznych, a dowody z nimi związane mogą korzystać z dowolnej właściwości z dowolnego ich widoku. Aby więc być w stanie zrozumieć zwykłe rozumowanie, do którego matematycy są przyzwyczajeni, musisz zmechanizować wszystkie te rzeczy. W przeciwieństwie do tego, wysoce abstrakcyjne konstrukcje mają (celowo) mały i ograniczony zestaw właściwości, więc musisz zmechanizować znacznie mniej, zanim dojdziesz do dobrych bitów.

Dowody w teorii złożoności oraz algorytmach / strukturach danych (z reguły) wykorzystują wyrafinowane właściwości prostych gadżetów, takich jak liczby, drzewa lub listy. Np. Argumenty kombinatoryczne, probabilistyczne i teoretyczne rutynowo pojawiają się jednocześnie w twierdzeniach teorii złożoności. Uzyskanie wsparcia biblioteki asystenta dowodu do tego stopnia, że jest to przyjemne do zrobienia, to sporo pracy!

Jednym z kontekstów, w których ludzie chętnie angażują się w pracę, są algorytmy kryptograficzne. Istnieją bardzo subtelne ograniczenia algorytmiczne ze złożonych przyczyn matematycznych, a ponieważ kod kryptograficzny działa w środowisku przeciwnym, nawet najmniejszy błąd może być katastrofalny. Na przykład w ramach projektu Certicrypt zbudowano wiele infrastruktury weryfikacyjnej w celu budowania sprawdzanych maszynowo dowodów poprawności algorytmów kryptograficznych.

— Neel Krishnaswami
źródło

Jednym z bardzo znaczących przykładów jest oczywiście formalizacja Gonthiersa Coqa twierdzenia o 4 kolorach w Coq, który wykorzystuje wiele kombinacji.

Mój kolega Uli Schöpp wykorzystał do tego celu bibliotekę ssreflect opracowaną przez Gonthiera w celu zweryfikowania (i nieznacznego rozszerzenia) również w Coq wyniku Cooka i Rackoffa na automatach grafowych. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Sformalizowana dolna granica nieukierunkowanej dostępności grafów. W logice programowania, sztucznej inteligencji i uzasadnienia ( str. 621-635). Springer Berlin / Heidelberg.)

— Martin Hofmann
źródło