¿Por qué se requiere el comprobador de pruebas en el código de prueba?

9

En el clásico artículo PLDI'98 de Necula, "El diseño e implementación de un compilador certificador", el verificador de alto nivel utiliza:

  1. VCGen para generar condiciones de verificación (predicados de seguridad)
  2. Probador del teorema lógico de primer orden para probar las condiciones
  3. Comprobador de pruebas LF para verificar la prueba del paso (2)

Estoy un poco confundido por el paso (3). ¿Por qué se requiere en absoluto? ¿Solo (1) y (2) no serán suficientes? ¿Por qué no confiamos simplemente en la prueba generada por un probador de teoremas?

proof-theory automated-theorem-proving program-verification RAM
fuente

Respuestas:

19

El propósito del comprobador de pruebas es minimizar la base informática confiable .

Al tener un comprobador de pruebas, ni el compilador ni el probador de teoremas deben ser correctos. El documento hace este punto en la página 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 comprobador de pruebas es solo un par de líneas de código y puede inspeccionarse a mano para verificar que sea correcto. Por el contrario, un comprobador automatizado que funciona bien es extremadamente complejo y es poco probable que sea correcto, aunque con comprobadores bien probados y ampliamente utilizados, los errores se producirán en casos extremos que podrían no ser fáciles de activar. Eche un vistazo al código LOC C de 30k que conforma Lingeling , un solucionador SAT de última generación para ver cuán complicados pueden ser los comprobadores de teoremas automatizados. Sin un comprobador de pruebas, tendrías que demostrar que ese teorema es correcto. Esto está más allá de lo que podemos hacer económicamente en 2015.

Martin Berger
fuente
Me sorprende que las pruebas construidas por los ATP puedan tener errores. (Pensé que los ATP pueden estar incompletos pero no son defectuosos / con errores) Aquí estoy menos informado. Me alegrará saber si hay casos conocidos de errores costosos en las pruebas generadas por los ATP.
Ram
3
@Ram Hay miles de pequeños errores de solidez en la historia de cualquier comprobador de teoremas automático serio. Consulte, por ejemplo, stackoverflow.com/questions/12281085/… o el historial de revisiones de cualquier herramienta de este tipo en github.
cody
@Ram Además del gran consejo de Cody, recomiendo aprender de la experiencia: escriba un pequeño ATP, como un solucionador de SAT básico. Eso se puede hacer en unas pocas líneas de código. Luego intente y haga que funcione bien agregando, por ejemplo, aprendizaje de cláusulas, literales observados o heurísticas de selección de variables interesantes. Entonces piense en la experiencia ...
Martin Berger