Каковы источники ненадежности доказательств Дафни?

Question

Я иногда (не часто, но достаточно часто) вижу, что доказательство будет работать в Dafny, а затем что-то, что кажется неуместным, изменится (например, имена переменных, определение функции, не имеющее отношения к доказательству и т. Д.) и доказательство сломается.

Мне интересно узнать технические причины, почему это происходит. В настоящее время у меня есть приблизительное представление об электронном сопоставлении и создании экземпляров квантора. Для меня не очевидно, что эти алгоритмы должны быть устойчивыми к этим, казалось бы, несущественным функциям ввода; также не очевидно, почему они не будут надежными. Я также не знаю, есть ли какие-либо соображения по поводу реализаций электронного сопоставления на практике, которые могут привести к ненадежности.

Под "надежным" я подразумеваю "либо всегда будет успешным, либо всегда не удастся, независимо от таких факторов, как имена переменных".

Итак, мне интересно понять технические причины (практические или теоретические) этой ненадежности.

Одна из причин, по которой я хотел бы получить больше интуиции, заключается в том, что, когда я сталкиваюсь с такой ситуацией, я могу исправить доказательство таким образом, чтобы сделать его более надежным. (Вместо этого сейчас обычно происходит то, что я исправляю доказательство произвольным образом, оно исправляется, а потом снова ломается.)

Я надеюсь найти ответ вроде "Z3 использует алгоритм X, который использует сложную эвристику Y, чтобы определить, когда отказаться от поиска в части области поиска, и ясно, что Y зависит от порядка поиска".. Такой ответ, вероятно, не помог бы мне написать лучшие доказательства Дафни, но удовлетворил бы мое любопытство.

Answer 1

Ни на один из этих вопросов нет простого ответа. Ниже я обобщу свой опыт работы с z3. Хотя люди из Дафни могут дать другие советы, я рискну предположить, что они применимы ко всем существующим (полу) автоматизированным инструментам проверки.

Хорошо известно, что даже изменение имен переменных может заставить z3 ответить sat или unknown, см. эту ветку для обсуждения.

Когда вы используете Dafny/Boogie и т. Д., Они выполняют массу преобразований в вашей программе, и даже простые изменения могут привести к тому, что серверный решатель будет демонстрировать совершенно разное поведение. (Обратите внимание, чтоsat никогда не должен становиться unsatили наоборот: это была бы законная ошибка. Но все может статьunknown, или возьмите сильно разное время.) Вот еще одна ветка, обсуждающая подобное явление.

Основная причина всегда сводится к случайному начальному значению, которое z3 использует для решения проблемы, выбранной эвристике и множеству настроек, которые могут повлиять на процесс поиска. Пробегz3 -pdна вашем терминале. На сегодняшний день существует более 500 "параметров", которые вы можете настроить! Практически невозможно попробовать все подходящие варианты, не говоря уже о выборе "правильных" настроек. Есть исследования по "модификации" параметров в fly, чтобы выбрать наиболее эффективный набор для целей регрессии, но это обычно не помогает, поскольку проблемы и способы их решения постоянно меняются.

Вы даже можете получить различную производительность для одной и той же задачи, изменяя параметр z3. smt.random_seed=N. Для разных значенийN, производительность может отличаться.

Итак, как практик вы действительно мало что можете сделать; К сожалению. Особенно, если вы используете такой инструмент, как Dafny/Boogie поверх z3, который добавляет свою магию. Простая идея состоит в том, чтобы задействовать множество ядер: запустите множество экземпляров решателя на многих ядрах с различными начальными числами, эвристиками, тактиками и т. Д. И выберите самый быстрый результат. Конечно, легче сказать, чем сделать.

Подводя итог, можно сказать, что большинство этих решателей / систем работают как черные ящики. Даже если бы вы много знали об их внутреннем устройстве, было бы сложно всегда "надежно" использовать их. Фактически, возможность сделать это, вероятно, достойна степени доктора философии. диссертационная работа на уровне, если бы вы могли придумать решатель / систему доказательства, которая была бы невосприимчивой к таким отклонениям.

Как конечный пользователь и при условии, что вы используете SMTLib, вы должны знать набор "общих" уловок и ловушек, которые могут помочь в создании более эффективных моделей. См. Этот ответ для обзора.

Но и отчаиваться тоже не стоит. Ситуация улучшается, и современные решатели во много раз производительнее, чем прошлогодние. Результаты SMT-конкурса - хороший способ отслеживать прогресс.

Удачи!