Пример алгоритма, в котором отсутствует доказательство правильности

18

У нас есть логика Хоара. Почему все еще возможно, что алгоритм верен, но нет никаких доказательств того, что он верен? Предположим, что алгоритм выражен в C. Тогда мы можем шаг за шагом утверждать, что он делает то, что должен делать.

Итак, мой вопрос:

Приведите мне пример алгоритма, который является правильным, но не имеет доказательства правильности.

РЕДАКТИРОВАТЬ: Я думаю, немного фона может помочь уточнить, куда я иду. Позвольте мне процитировать Скотта Ааронсона:

С 1970-х годов появились предположения, что P NP может быть независимым (то есть ни доказуемым, ни опровергаемым) от стандартных систем аксиом математики, таких как теория множеств Цермело-Френкеля. Чтобы было ясно, это будет означать, что либо

  1. Алгоритм полиномиального времени для NP-полных задач не существует, но мы никогда не сможем доказать это (по крайней мере, в наших обычных формальных системах), иначе

  2. полиномиальный алгоритм для NP-полных задач делает существует, но либо мы никогда не можем доказать , что он работает, или мы никогда не можем доказать , что он останавливается в полиномиальное время.

Я имею в виду вторую возможность. Поскольку Ааронсон может так уверенно перечислить это как возможность, я думаю, что должен существовать пример типа 2. Вот почему я задаю этот вопрос. Но, кажется, быстрого и ясного ответа не видно.

Зируй Ван
источник
17
Что значит сказать, что алгоритм верен, если у нас нет доказательства правильности?
Дэвид Ричерби
14
Вы имеете в виду «доказательство правильности невозможно» или «никто не доказал, что это правильно»?
gnasher729
12
Алгоритмы не должны быть правильными ... предположим, у вас есть: (1) положите пустое ведро на подоконник утром. (2) снять его вечером. (3) измерить объем воды в ведре. (4) повторить на следующее утро. Это описание алгоритма, но оно не описывает ничего, что можно без всяких усилий назвать «правильным». Интересно, что большая часть программного кода в мире написана именно таким образом: его просто не касается правильности того, что он вообще делает.
wvxvw
@wvxvw Я запутался тогда, что значит для алгоритма быть «правильным» тогда? Если он делает то, что должен был сделать, не значит ли это, что это правильно? Если цель вашего сценария состояла в том, чтобы найти среднее количество воды, собираемой в ведре во время дождя, на каждый день, разве алгоритм не будет правильным в этом случае?
Абдул
8
@ Чи, ты не понимаешь ... дело не в том, что программисты не заботятся о правильности своего кода, а в том, что для некоторых алгоритмов понятие «корректность» неприменимо. Возьмите какое-нибудь приложение .NET WindowsForms, которое говорит что-то вроде: «поместите эту кнопку с этим ярлыком в это положение, затем поместите эту другую кнопку в это другое положение и т. Д.» - может быть некоторая интерпретация программа делает, в соответствии с чем то, что она делает, может быть оценено как (не) правильное (например, графический дизайнер говорит, что это «выглядит некрасиво»), но это далеко не так.
wvxvw

Ответы:

50

Вот алгоритм для функции тождества:

  • Вход:n
  • Проверьте, кодирует ли ая двоичная строка доказательство в ZFC, и если да, выведите0 > 1 n + 1n0>1n+1
  • В противном случае выведитеn

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

Юваль Фильмус
источник
2
Вы уверены, что Проверка, кодирует ли ая двоичная строка доказательство в ZFC,0 > 1n0>1 является алгоритмом?
Дмитрий Григорьев
23
Нет, но проверка определенно может быть реализована алгоритмически (т. Е. На машине Тьюринга). Фактически это одно из требований, которые мы предъявляем к системам доказательств - чтобы валидность доказательств проверялась алгоритмически.
Юваль
6
@Puppy ZFC доказывает . Но это также может доказать если (f) это противоречиво. Конечно, почти все считают, что ZFC непротиворечив, но из-за теорем о неполноте мы не можем знать это наверняка. 0 > 1¬(0>1)0>1
Чи
1
@ Натаниэль Вовсе нет. Например, вы можете легко доказать правильность каждого алгоритма учебника. Этот алгоритм отличается тем, что он основан на согласованности ZFC, что само по себе ZFC не может доказать.
Юваль
1
@ Натаниэль: Если хотите, давайте продолжим эту дискуссию в чате .
user21820
9

Большинство алгоритмов не доказали свою корректность в логике Хоара. Основная причина в том, что такие корректные доказательства чрезвычайно дороги по состоянию на январь 2017 года, вероятно, на несколько порядков по сравнению с «простым» программированием. В настоящее время ведется большая работа по снижению этих затрат за счет автоматизации, но это нелегкая борьба.

Другая причина, по которой у алгоритма может не быть доказательства корректности, и который на практике более актуален, чем явления неполноты, о которых упоминали Ювал и Чи, заключается в том, что мы можем не знать, что это за спецификация. Эта проблема имеет два измерения.

  • Клиенты не знают, чего хотят. Это хорошо известная проблема в разработке программного обеспечения, и разработчики программного обеспечения разработали множество подходов для решения этой проблемы.

  • Спецификация сложна. Хорошим примером является правильность криптографических алгоритмов. Только недавно Micali & Goldwasser получили награды Turing за то, что они указали, что означает криптографическая безопасность. Однако обратите внимание, что это определение (насколько мне известно) для «теоретической криптографии», где у вас есть параметр безопасностиnначиная с натуральных чисел, и противники являются вероятностными машинами Тьюринга за полиномиальное время. Насколько мне известно (пожалуйста, исправьте меня, если я ошибаюсь), существует несоответствие между теорией и практикой, и конкретные алгоритмы, такие как AES и SHA256, не вполне соответствуют этим теоретическим спецификациям. Я не думаю, что есть полная спецификация для таких алгоритмов, поэтому мы не можем, в принципе, проверить их в смысле, например, логики Хоара.

Мартин Бергер
источник
AES входит в компетенцию определений криптографической безопасности. (Вам нужно использовать конкретные определения безопасности, а не асимптотические определения, но вы должны делать это в любом случае, если вы хотите обеспечить безопасность на практике.)
DW
@DW Интересно. Я не знал об этом. Как обходится асимптотическая природа теоретической криптографии? Не могли бы вы указать мне на бумагу по этому вопросу? Как насчет конкретных криптографических хеш-функций?
Мартин Бергер
en.wikipedia.org/wiki/Concrete_security и ссылки, перечисленные там. Хеш-функции - более сложный случай, потому что это зависит от того, для чего вы их используете, но сложности в значительной степени ортогональны асимптотической безопасности по сравнению с конкретной безопасностью.
DW
2
Для шифрования вам нужны два алгоритма: один, который шифрует, другой, который расшифровывает. Один из них не может быть правильным сам по себе. Они могут быть правильными только в паре (вы докажете, что расшифровка зашифрованного ввода приводит к оригиналу). Но для шифрования вы хотите, чтобы он не поддавался взлому, и это то, что вы не можете уловить с «правильностью».
gnasher729
1
@WW Я должен несколько не согласиться. Хотя работы Рогэвея и Белларе велики, они подразумевают, что они каким-либо образом допускают доказательства безопасности примитивов, что вводит в заблуждение. Обе статьи в основном касаются протоколов (то есть предполагают, что примитивы, такие как AES, SHA, RSA и т. Д.) Безопасны, а затем доказывают это. Основная проблема обеспечения безопасности самих примитивов остается. Если у вас есть ссылки на доказательства безопасности примитивов, мне было бы интересно. Например, во второй статье предполагается, что RSA сложен, что является большой проблемой.
DRF
5

Это связано с незавершенностью базовой логики. Действительно, логика Хоара обычно содержит правило ослабления или «до публикации» где значение необходимо доказать в базовой логике, обычно это логика первого порядка (FOL) с некоторой теоретико-множественной аксиоматизацией, такой как Zermelo- Френкель (ZF). P

PP{P}c{Q}QQ{P}c{Q}
PP,QQ

Сложность в том, что мы знаем, что такая логика неполна, как доказал Гедель почти сто лет назад. Более конкретно, существует предикат о натуральных числах для которого мы можем доказать внутри логики , , и так далее для любой данной натуральной постоянной, но нет никакого способа доказать .Р ( 0 ) Р ( 1 ) Р ( 2 ) п N . P ( n )P(n)P(0)P(1)P(2)nN. P(n)

Со стороны информатики это странное поведение может быть продемонстрировано с помощью теории вычислимости. Предположим, что машина Тьюринга при запуске на пустой ленте не останавливается за шагов ( ). Тогда в ZF мы можем доказать этот факт, по существу разворачивая выполнение шаг за шагом в доказательстве. Однако, когда расходится, мы не можем надеяться, что сможем доказать дивергенцию в ZF ( ). В самом деле, если бы это было возможно для всех данных , то мы могли бы полуопределить дивергенцию, перечислив все возможные доказательства для и остановившись, когда он найден. Поскольку мы знаем, что дивергенция не является RE, это невозможно.n P ( n ) M n . P ( n ) M n . P ( n )MnP(n)Mn. P(n)Mn. P(n)

чи
источник
5

Проблема: выведите «Да», если каждое четное число ≥ 4 ​​является суммой двух простых чисел, и «Нет», если существует четное число ≥ 4, которое не является суммой двух простых чисел.

Алгоритм: вывести «Да»

Большинство людей считают, что алгоритм правильный. Там нет известных доказательств, и это вполне возможно , что нет никаких доказательств.

gnasher729
источник
3

Любой алгоритм, который является правильным, но мы не знаем, сколько времени потребуется для его запуска, может быть преобразован в алгоритм, который останавливается за гарантированное количество времени, но мы не уверены, что он правильный.

Например, чтобы найти простое число больше , начните отсчет с тестирования, если каждое число простое, пока не найдете его. Теперь измените его, чтобы сдаться и вернуть если мы не можем найти простое число после попытки . Если модифицированный алгоритм когда-либо возвращает , это неверно, но никто не знает, случится ли это когда-либо или нет. Даже с помощью шагов, которые мы не можем доказать, простое число всегда будет найдено.n + 1 0 log ( n ) 2 0 nn+10log(n)20n

Итак, у нас есть алгоритм, который является правильным, но у нас нет доказательств того, что он работает за полиномиальное время, и алгоритм (тот же, но ограниченный по времени), который работает за полиномиальное время, но у нас нет никаких доказательств того, что он верен. Как и в случае с проблемой , для этого примера также вероятно, что таких доказательств не существует.P=NP

Дан Брумлев
источник