Pourquoi le vérificateur d'épreuves est-il requis dans le code de transport d'épreuves

9

Dans le document PLDI 98 classique de Necula, "La conception et la mise en œuvre d'un compilateur de certification", le vérificateur de haut niveau utilise:

  1. VCGen pour générer des conditions de vérification (prédicats de sécurité)
  2. Prouveur de théorème logique du premier ordre pour prouver les conditions
  3. Vérificateur d'épreuves LF pour vérifier l'épreuve de l'étape (2)

Je suis un peu confus à l'étape (3). Pourquoi est-ce obligatoire? Est-ce que (1) et (2) ne suffiront pas? Pourquoi ne faisons-nous pas simplement confiance à la preuve générée par un prouveur de théorème?

proof-theory automated-theorem-proving program-verification RAM
la source

Réponses:

19

Le vérificateur d'épreuves a pour objectif de minimiser la base informatique de confiance .

En ayant un vérificateur de preuve, ni le compilateur ni le prouveur de théorème n'ont besoin d'être corrects. Le papier fait ce point à la page 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.

Un vérificateur d'épreuves n'est que quelques lignes de code et peut être inspecté à la main pour en vérifier l'exactitude. En revanche, un prouveur automatisé qui fonctionne bien est extrêmement complexe et peu probable d'être correct, bien qu'avec des prouveurs bien testés et largement utilisés, les erreurs se produiront dans des cas marginaux qui pourraient ne pas être faciles à déclencher. Jetez un œil au code LOC C de 30k qui constitue Lingeling , un solveur SAT à la pointe de la technologie pour voir à quel point les prouveurs de théorèmes automatisés peuvent être compliqués. Sans vérificateur de preuve, vous devez prouver que ce prouveur de théorème est correct. C'est au-delà de ce que nous pouvons faire économiquement en 2015.

Martin Berger
la source
Je suis surpris que les preuves construites par les ATP puissent être boguées. (Je pensais que les ATP peuvent être incomplets mais pas défectueux / buggy) Je suis moins informé ici. Je serai heureux de savoir s'il existe des cas connus d'erreurs coûteuses dans les preuves générées par les ATP.
Ram
3
@Ram Il y a des milliers de minuscules bogues de solidité dans l'histoire de tout sérieux prouveur de théorème automatique. Voir par exemple stackoverflow.com/questions/12281085/… ou l'historique des révisions d'un tel outil sur github.
cody
@Ram En plus des excellents conseils de Cody, je recommande d'apprendre par expérience: écrire un petit ATP tel qu'un solveur SAT de base. Cela peut se faire en quelques lignes de code. Ensuite, essayez de le faire bien fonctionner en ajoutant, par exemple, l'apprentissage des clauses, les littéraux surveillés ou des heuristiques de sélection de variables intéressantes. Alors pensez à l'expérience ...
Martin Berger