Алгоритм сертификации
В теоретической информатике — сертифицирующий алгоритм это алгоритм, который выводит вместе с решением решаемой им проблемы доказательство того, что решение правильное. Сертифицирующий алгоритм считается эффективным, если общее время выполнения алгоритма и средства проверки доказательств медленнее не более чем в постоянный коэффициент, чем самый известный несертифицирующий алгоритм для той же задачи. [1]
Доказательство, полученное с помощью сертифицирующего алгоритма, должно быть в некотором смысле проще, чем сам алгоритм, поскольку в противном случае любой алгоритм можно было бы считать сертифицирующим (его результаты проверяются повторным запуском того же алгоритма). Иногда это формализуется требованием, чтобы проверка доказательства занимала меньше времени, чем исходный алгоритм, тогда как для других задач (в частности, тех, для которых решение может быть найдено за линейное время ) простота выходного доказательства рассматривается в менее формальном порядке. смысл. [1] Например, достоверность выходного доказательства может быть более очевидной для пользователей-людей, чем правильность алгоритма, или средство проверки доказательства может более поддаваться формальной проверке . [1] [2]
Реализации сертифицирующих алгоритмов, которые также включают в себя средство проверки доказательств, сгенерированных алгоритмом, могут считаться более надежными, чем несертифицирующие алгоритмы. Ибо при каждом запуске алгоритма происходит одно из трех: он выдает правильный результат (желаемый случай), обнаруживает ошибку в алгоритме или ее последствия (нежелательно, но обычно предпочтительнее, чем продолжать работу без обнаружения ошибки) или и алгоритм, и программа проверки ошибочны таким образом, что маскируют ошибку и предотвращают ее обнаружение (нежелательно, но маловероятно, поскольку это зависит от существования двух независимых ошибок). [1]
Примеры
[ редактировать ]Многие примеры проблем с проверяемыми алгоритмами взяты из теории графов .Например, классический алгоритм проверки того, является ли граф двудольным , просто выводит логическое значение: true, если граф двудольный, и false в противном случае. Напротив, сертифицирующий алгоритм может выводить 2-раскраску графа в случае, если он двудольный, или цикл нечетной длины, если это не так. Любой граф является двудольным тогда и только тогда, когда он может быть двухцветным, и недвудольным тогда и только тогда, когда он содержит нечетный цикл. Как проверку правильности 2-раскраски, так и проверку того, является ли данная последовательность вершин нечетной длины циклом, можно выполнить проще, чем проверку двудольности. [1]
Аналогично, можно проверить, является ли данный граф ориентированный ациклическим, с помощью проверяющего алгоритма, который выводит либо топологический порядок , либо ориентированный цикл. Можно проверить, является ли неориентированный граф хордальным графом, с помощью проверяющего алгоритма, который выводит либо порядок исключения (упорядочение всех вершин таким образом, что для каждой вершины соседи, находящиеся позже в упорядочении, образуют клику ) или безаккордовый цикл. можно А проверить, является ли граф планарным, с помощью проверяющего алгоритма, который выводит либо плоское вложение, либо подграф Куратовского . [1]
Расширенный алгоритм Евклида для определения наибольшего общего делителя двух целых чисел x и y является сертифицирующим: он выводит три целых числа g (делитель), a и b , такие, что ax + by = g . Это уравнение может быть верным только для кратных наибольшему общему делителю, поэтому проверка того, что g является наибольшим общим делителем, может быть выполнена путем проверки того, что g делит и x, и y , и что это уравнение правильно. [1]
См. также
[ редактировать ]- Проверка работоспособности — простая проверка правильности выходного или промежуточного результата, которая не обязательно должна быть полным доказательством правильности.
Ссылки
[ редактировать ]- ^ Jump up to: а б с д и ж г МакКоннелл, РМ; Мельхорн, К. ; Нэхер, С.; Швейцер, П. (май 2011 г.), «Сертификация алгоритмов», Computer Science Review , 5 (2): 119–161, doi : 10.1016/j.cosrev.2010.09.009 .
- ^ Алькассар, Эйад; Бёме, Саша; Мельхорн, Курт ; Ризкалла, Кристина (июнь 2013 г.), «Схема проверки сертифицирующих вычислений», Journal of Automated Reasoning , 52 (3): 241–273, arXiv : 1301.7462 , doi : 10.1007/s10817-013-9289-2 .