Почему проверка кода требуется в коде переноса доказательства

9

В классической статье PLDI'98 Necula «Разработка и реализация сертифицирующего компилятора» верификатор высокого уровня использует:

  1. VCGen для генерации условий проверки (предикаты безопасности)
  2. Доказательство логической теоремы первого порядка для доказательства условий
  3. LF proof checker для проверки доказательства с шага (2)

Я немного смущен шагом (3). Зачем это вообще нужно? Только (1) и (2) не будет достаточно? Почему бы нам просто не доверять доказательству, созданному доказателем теорем?

proof-theory automated-theorem-proving program-verification Баран
источник

Ответы:

19

Целью проверки корректности является минимизация базы доверенных компьютеров .

Имея средство проверки, ни компилятор, ни доказатель теоремы не должны быть правильными. В документе говорится об этом на странице 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.

Проверка корректности - это всего лишь пара строк кода, и ее можно проверить вручную на правильность. В отличие от этого, автоматический проверяющий, который хорошо работает, чрезвычайно сложен и вряд ли будет корректным, хотя в случае хорошо проверенных и широко используемых проверок ошибки будут в крайних случаях, которые может быть нелегко вызвать. Взгляните на 30- килограммовый код LOC C, который составляет Lingeling , современный SAT-решатель, чтобы увидеть, насколько сложными могут быть автоматизированные средства доказательства теорем. Без проверки вы должны были бы доказать правильность этой теоремы. Это выше того, что мы можем сделать экономически в 2015 году.

Мартин Бергер
источник
Я удивлен, что доказательства, построенные с помощью ATP, могут содержать ошибки. (Я думал, что АТФ могут быть неполными, но не несостоятельными / глючными). Здесь я менее информирован. Я буду рад узнать, есть ли какие-либо известные случаи дорогостоящих ошибок в доказательствах, генерируемых ATP.
Рам
3
@Ram В истории любого серьезного автоматического тестера теорем есть тысячи крошечных ошибок. См., Например, stackoverflow.com/questions/12281085/… или историю изменений любого такого инструмента на github.
Коди
@Ram В дополнение к отличному совету Коди, я рекомендую учиться на собственном опыте: написать немного ATP, например, базовый SAT-решатель. Это можно сделать в несколько строк кода. Затем попытайтесь заставить его работать хорошо, добавив, например, изучение предложений, наблюдаемые литералы или интересные эвристики выбора переменных. Тогда подумайте об опыте ...
Мартин Бергер,