Dlaczego Proof Checker jest wymagany w Proof Carry Code?

W klasycznym dokumencie PLDI'98 autorstwa Neculi „Projekt i implementacja kompilatora certyfikującego” weryfikator wysokiego poziomu wykorzystuje:

VCGen generuje warunki weryfikacji (prognozy bezpieczeństwa)
Dowódca logiki twierdzenia pierwszego rzędu, aby udowodnić warunki
Kontroler sprawdzania LF, aby sprawdzić dowód od kroku (2)

Jestem trochę zdezorientowany krokiem (3). Dlaczego w ogóle jest to wymagane? Czy po prostu (1) i (2) nie wystarczy? Dlaczego po prostu nie ufamy dowodom wygenerowanym przez twierdzącego twierdzącego?

proof-theory automated-theorem-proving program-verification

— Baran
źródło

Celem sprawdzania poprawności jest zminimalizowanie zaufanej bazy obliczeniowej .

Dzięki sprawdzaniu poprawności ani kompilator, ani twierdzenie twierdzeń nie muszą być poprawne. Artykuł wskazuje na to na stronie 3:

Neither the compiler nor the prover need to be correct in order to be guaranteed to   
detect incorrect compiler output. This is a significant advantage since the VCGen and  
the  proof checker are significantly simpler than the compiler and the prover.

Sprawdzanie poprawności to tylko kilka wierszy kodu i można je sprawdzić ręcznie pod kątem poprawności. W przeciwieństwie do tego automatyczny przyrząd, który działa dobrze, jest niezwykle złożony i mało prawdopodobne, aby był poprawny, chociaż przy dobrze przetestowanych i szeroko stosowanych dowodach błędy będą w skrajnych przypadkach, które mogą nie być łatwe do uruchomienia. Spójrz na 30k kod LOC C, który składa się na Lingeling , najnowocześniejszy solver SAT, aby zobaczyć, jak skomplikowane mogą być automatyczne dowody twierdzeń. Bez sprawdzania poprawności musiałbyś udowodnić, że ten dowód twierdzenia jest poprawny. To więcej niż możemy zrobić ekonomicznie w 2015 roku.

— Martin Berger
źródło

Dziwi mnie, że dowody zbudowane przez ATP mogą być błędne. (Myślałem, że ATP mogą być niekompletne, ale nie niesłuszne / błędne) Jestem tutaj mniej informowany. Z przyjemnością dowiem się, czy istnieją znane przypadki kosztownych błędów w dowodach generowanych przez ATP.

— Ram

@Ram W historii każdego poważnego automatycznego dowodu twierdzeń istnieją tysiące drobnych błędów w poprawności dźwięku. Zobacz np. Stackoverflow.com/questions/12281085/... lub historię zmian każdego takiego narzędzia na github.

— cody

@Ram Oprócz świetnych rad Cody'ego, polecam uczyć się z doświadczenia: napisz trochę ATP, takiego jak podstawowy solver SAT. Można to zrobić za pomocą kilku wierszy kodu. Następnie spróbuj sprawić, by działał dobrze, dodając np. Uczenie się klauzul, oglądane literały lub interesującą heurystykę wyboru zmiennych. Pomyśl o tym doświadczeniu ...

— Martin Berger,