Сложность доказательства - Proof complexity

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

Систематическое изучение сложности доказательства началось с работы Стивена Кука и Роберта Рекхоу (1979), которые дали базовое определение пропозициональной системы доказательства с точки зрения вычислительной сложности. В частности, Кук и Рекхоу заметили, что доказательство нижних границ размера доказательства для более сильных и сильных пропозициональных систем доказательства можно рассматривать как шаг к отделению NP от coNP (и, таким образом, P от NP), поскольку существование пропозициональной системы доказательств, допускающей доказательства полиномиального размера для всех тавтологий эквивалентно NP = coNP.

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

Математическая логика также может служить основой для изучения размеров пропозициональных доказательств. Теории первого порядка и, в частности, слабые фрагменты арифметики Пеано , которые называются теориями ограниченной арифметики , служат единообразными версиями систем пропозициональных доказательств и обеспечивают дополнительную основу для интерпретации коротких пропозициональных доказательств в терминах различных уровней допустимых рассуждений.

Системы доказательства

Система пропозициональных доказательств представлена как алгоритм проверки-доказательства P ( A , x ) с двумя входами. Если P принимает пару ( А , х ) мы говорим , что х является P -доказательство A . P требуется, чтобы работать за полиномиальное время, и, более того, должно выполняться то, что A имеет P- доказательство тогда и только тогда, когда это тавтология.

Примеры пропозициональных систем доказательства включают в себя последовательное исчисление , разрешение , плоскости отсечения и систему Фреге . Сильные математические теории, такие как ZFC, также порождают системы пропозициональных доказательств: доказательство тавтологии в пропозициональной интерпретации ZFC - это ZFC-доказательство формализованного утверждения « является тавтологией». ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$

Доказательства размера полинома и проблема NP и coNP

Сложность доказательства измеряет эффективность системы доказательств обычно с точки зрения минимального размера доказательств, возможных в системе для данной тавтологии. Размер доказательства (соотв. Формулы) - это количество символов, необходимых для представления доказательства (соотв. Формулы). Пропозициональная система доказательство P является полиномиально ограниченным , если существует постоянная такая , что каждая тавтология размера имеет P -доказательство размера . Центральный вопрос сложности доказательства - понять, допускают ли тавтологии доказательства полиномиального размера. Формально, ${\ displaystyle c}$ ${\ displaystyle n}$ ${\ Displaystyle (п + с) ^ {с}}$

Проблема (NP против coNP)

Существует ли полиномиально ограниченная система пропозициональных доказательств?

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

Оптимальность и моделирование между системами доказательства

Сложность доказательства сравнивает силу систем доказательства с использованием понятия моделирования. Система доказательств P p-моделирует систему доказательств Q, если существует функция с полиномиальным временем, которая при заданном Q- доказательстве дает P- доказательство той же тавтологии. Если Р р-имитирует Q и Q р-имитирует P , доказательство системы P и Q являются р-эквивалентными . Существует также более слабое понятие моделирования: доказательство системы P имитирует стойкие системы Q , если существует такой полином р , что для любого Q -доказательства х тавтологий А , существует Р -доказательства у из , что длина от у , | y | не превосходит p (| x |).

Например, исчисление секвенций p-эквивалентно (каждой) системе Фреге.

Система доказательства является p-оптимальной, если она p -моделирует все другие системы доказательств, и оптимальной, если она моделирует все другие системы доказательств. Существуют ли такие системы доказательств - открытый вопрос:

Проблема (оптимальность)

Существует ли p-оптимальная или оптимальная система пропозициональных доказательств?

Каждая пропозициональная система доказательств P может моделироваться Расширенная Фреге продлен с аксиомами постулировать разумность P . Известно, что существование оптимальной (соответственно p-оптимальной) системы доказательств следует из предположения, что NE = coNE (соответственно E = NE).

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

Автоматизация поиска доказательств

Важный вопрос в сложности доказательства - понять сложность поиска доказательств в системах доказательств.

Проблема (Автоматизируемость)

Существуют ли эффективные алгоритмы поиска доказательств в стандартных системах доказательств, таких как система Резолюции или Фреге?

Вопрос можно формализовать с помощью понятия автоматизируемости (также известной как автоматизируемость).

Система доказательства Р является автоматизируемым , если существует алгоритм , который дано тавтологию выводит P -доказательство в полиномиальное время в размерах и длине самого короткого P -доказательства . Обратите внимание, что если система доказательств не ограничена полиномиально, ее можно автоматизировать. Система доказательства Р является слабо автоматизирован , если существует доказательство системы R и алгоритм , который дано тавтологию выводит R -доказательство в полиномиальное время в размерах и длине самого короткого P -доказательства . ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$

Многие представляющие интерес системы доказательств считаются неавтоматическими. Однако в настоящее время известны лишь условно отрицательные результаты.

Krajíček и Pudlák (1998) доказали, что Extended Frege не является слабо автоматизируемым, если RSA не защищен от P / poly .
Бонет, Питасси и Раз (2000) доказали, что система -Frege не является слабо автоматизируемой, если только схема Диффи-Хелмана не защищена от P / poly. Это было расширено Бонет, Доминго, Гавалда, Масиел и Питасси (2004), которые доказали, что системы Фреге с постоянной глубиной глубины не менее 2 не являются слабо автоматизируемыми, если только схема Диффи-Хельмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени. ${\ displaystyle TC ^ {0}}$
Алехнович и Разборов (2008) доказали, что древовидная Резолюция и Резолюция не автоматизируются, если FPT = W [P]. Это было расширено Галези и Лаурией (2010), которые доказали, что Nullstellensatz и полиномиальное исчисление нельзя автоматизировать, если иерархия фиксированных параметров не рухнет. Mertz, Pitassi и Wei (2019) доказали, что древовидное разрешение и разрешение не могут быть автоматизированы даже в определенное квазиполиномиальное время, предполагая гипотезу экспоненциального времени.
Атсериас и Мюллер (2019) доказали, что разрешение невозможно автоматизировать, если P = NP. Это было расширено де Резенде, Гёсом, Нордстремом, Питасси, Робере и Соколовым (2020) до NP-сложности автоматизации Nullstellensatz, полиномиального исчисления, Шерали-Адамса; Гоэса, Корота, Мертца и Питасси (2020) на NP-твердость автоматизации плоскостей резки; и Гарлик (2020) к NP-сложности автоматизации разрешения k -DNF.

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

С положительной стороны,

Бим и Питасси (1996) показали, что древовидная Резолюция автоматизируется за квазиполиномиальное время, а Резолюция автоматизируется на формулах малой ширины за слабо субэкспоненциальное время.

Ограниченная арифметика

Системы пропозициональных доказательств можно интерпретировать как неоднородные эквиваленты теорий более высокого порядка. Эквивалентность чаще всего изучается в контексте теорий ограниченной арифметики . Например, Расширенная система Фреге соответствует теории Кука, формализующей рассуждения за полиномиальное время, а система Фреге соответствует теории, формализующей рассуждения. ${\ displaystyle PV_ {1}}$ ${\ displaystyle VNC ^ {1}}$ ${\ Displaystyle NC ^ {1}}$

Соответствие было введено Стивеном Куком (1975), который показал, что теоремы coNP, формально формулы теории, переводятся в последовательности тавтологий с доказательствами полиномиального размера в расширенном Фреге. Более того, Расширенная Фреге является самой слабой такой системой: если другая система доказательств P обладает этим свойством, то P имитирует Расширенная Фреге. ${\ displaystyle \ Pi _ {1} ^ {b}}$ ${\ displaystyle PV_ {1}}$

Альтернативный перевод между утверждениями второго порядка и пропозициональными формулами, данный Джеффом Пэрис и Алексом Уилки (1985), был более практичным для захвата подсистем Расширенного Фреге, таких как Фреге или Фреге постоянной глубины.

В то время как вышеупомянутое соответствие говорит, что доказательства в теории переводятся в последовательности коротких доказательств в соответствующей системе доказательств, также имеет место форма противоположной импликации. Можно получить нижние оценки размера доказательств в доказательство системы P путем построения подходящих моделей теории T , соответствующей системе P . Это позволяет доказывать нижние границы сложности с помощью теоретико-модельных построений, подхода, известного как метод Айтая.

SAT решатели

Системы пропозициональных доказательств можно интерпретировать как недетерминированные алгоритмы распознавания тавтологий. Доказав суперполиномиальным нижняя граница на доказательство системы P , таким образом , исключает существование полиномиального алгоритма для SAT на основе P . Например, прогоны алгоритма DPLL на неудовлетворительных экземплярах соответствуют древовидным опровержениям Резолюции. Следовательно, экспоненциальные нижние границы для древовидного разрешения (см. Ниже) исключают существование эффективных алгоритмов DPLL для SAT. Точно так же нижние границы экспоненциального разрешения подразумевают, что решатели SAT, основанные на разрешении, такие как алгоритмы CDCL , не могут эффективно решать SAT (в худшем случае).

Нижние оценки

Доказательство нижних оценок длины пропозициональных доказательств, как правило, очень сложно. Тем не менее было обнаружено несколько методов доказательства нижних оценок для слабых систем доказательства.

Хакен (1985) доказал экспоненциальную нижнюю границу разрешения и принципа ячейки.
Ajtai (1988) доказал суперполиномиальную нижнюю границу для системы Фреге постоянной глубины и принципа голубятни. Это было усилено до экспоненциальной нижней границы Крайичеком, Пудлаком и Вудсом, а также Питасси, Бимом и Импальяццо. Нижняя граница Аджтая использует метод случайных ограничений, который также использовался для получения нижних оценок AC ⁰ сложности схемы .
Крайичек (1994) сформулировал метод допустимой интерполяции и позже использовал его для получения новых нижних оценок для Резолюции и других систем доказательства.
Пудлак (1997) доказал экспоненциальные нижние оценки для секущих плоскостей с помощью допустимой интерполяции.
Бен-Сассон и Вигдерсон (1999) предоставили метод доказательства, снижающий нижние границы размера опровержений Резолюции до нижних границ ширины опровержений Резолюции, который захватил многие обобщения нижней границы Хакена.

Получение нетривиальной нижней оценки для системы Фреге - давняя открытая проблема.

Возможная интерполяция

Рассмотрим тавтологию формы . Тавтология верна для любого выбора и после фиксации оценки и являются независимыми, потому что они определены на непересекающихся наборах переменных. Это означает, что можно определить схему интерполяции , в которой выполняются оба и . Схема интерполянта решает, является ли оно ложным или истинным, только путем рассмотрения . Характер схемы интерполянта может быть произвольным. Тем не менее, можно использовать доказательство исходной тавтологии как подсказку о том, как строить . Системное доказательство P , как говорят, посильные интерполяции , если интерполянт эффективно вычислимый из любого доказательства тавтологии в P . Эффективность измеряется по длине доказательства: легче вычислить интерполянты для более длинных доказательств, поэтому это свойство кажется антимонотонным в силе системы доказательств. ${\ Displaystyle А (х, у) \ вправо В (у, г)}$ ${\ displaystyle y}$ ${\ displaystyle y}$ ${\ displaystyle A}$ ${\ displaystyle B}$ ${\ displaystyle C (y)}$ ${\ Displaystyle А (х, у) \ вправо С (у)}$ ${\ Displaystyle C (y) \ rightarrow B (y, z)}$ ${\ Displaystyle А (х, у)}$ ${\ Displaystyle В (у, г)}$ ${\ displaystyle y}$ ${\ Displaystyle А (х, у) \ вправо В (у, г)}$ ${\ displaystyle C}$ ${\ displaystyle C (y)}$ ${\ Displaystyle А (х, у) \ вправо В (у, г)}$

Следующие три утверждения не могут быть одновременно истинными: (а) имеет краткое доказательство в некоторой системе доказательств; (б) такая система доказательств имеет допустимую интерполяцию; (c) схема интерполянта решает вычислительно трудную задачу. Ясно, что из (a) и (b) следует, что существует небольшая схема интерполяции, что противоречит (c). Такое соотношение позволяет превратить верхние границы длины доказательства в нижние оценки вычислений и, вдвойне, превратить эффективные алгоритмы интерполяции в нижние границы длины доказательства. ${\ Displaystyle А (х, у) \ вправо В (у, г)}$

Некоторые системы проверки, такие как Разрешение и Плоскости сечения, допускают допустимую интерполяцию или ее варианты.

Возможная интерполяция может рассматриваться как слабая форма автоматизируемости. Фактически, для многих систем доказательства, таких как Расширенная Фреге, допустимая интерполяция эквивалентна слабой автоматизируемости. В частности, многие системы доказательства P способны доказать свою собственную состоятельность , которая является тавтологией о том , что `если это P -доказательство формулы , то имеет место. Здесь кодируются свободными переменными. Более того, можно генерировать P- доказательства за полиномиальное время, учитывая длину и . Следовательно, эффективный интерполянт, являющийся результатом коротких P- доказательств надежности P, будет определять, допускает ли данная формула короткое P- стойкость . Такой интерполянт можно использовать для определения системы доказательств R, свидетельствующей о том, что P слабо автоматизируется. С другой стороны, из слабой автоматизируемости системы доказательств P следует, что P допускает допустимую интерполяцию. Однако, если система доказательств P не доказывает эффективно свою собственную надежность, то она не может быть слабо автоматизируемой, даже если она допускает допустимую интерполяцию. ${\ displaystyle Ref_ {P} (\ pi, \ phi, x)}$ ${\ displaystyle \ pi}$ ${\ Displaystyle \ фи (х)}$ ${\ Displaystyle \ фи (х)}$ ${\ displaystyle \ pi, \ phi, x}$ ${\ displaystyle Ref_ {P} (\ pi, \ phi, x)}$ ${\ displaystyle \ pi}$ ${\ displaystyle \ phi}$ ${\ displaystyle \ phi}$ ${\ displaystyle \ pi}$

Многие результаты неавтоматизируемости фактически являются свидетельством против возможной интерполяции в соответствующих системах.

Krajíček и Pudlák (1998) доказали, что Extended Frege не допускает выполнимой интерполяции, если RSA не защищен от P / poly.
Бонет, Питасси и Раз (2000) доказали, что система -Frege не допускает допустимой интерполяции, если схема Диффи-Хелмана не защищена от P / poly. ${\ displaystyle TC ^ {0}}$
Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) доказали, что системы Фреге с постоянной глубиной не допускают допустимой интерполяции, если только схема Диффи-Хельмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени.

Неклассическая логика

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

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

Смотрите также

дальнейшее чтение

Бим, Пол; Pitassi, Toniann (1998), "Пропозициональное доказательство сложности: прошлое, настоящее и будущее", Бюллетень Европейской ассоциации по теоретической информатике , 65 : 66-89, MR 1650939 , ECCC TR98-067
Повар, Стивен ; Нгуен, Фуонг (2010), Логические основы сложности доказательства , перспективы в логике, Кембридж: Cambridge University Press, DOI : 10.1017 / CBO9780511676277 , ISBN 978-0-521-51729-4, Руководство по ремонту 2589550( проект от 2008 г. )
Крайичек, Ян (1995), Ограниченная арифметика, логика высказываний и теория сложности , Cambridge University Press
Крайичек, Ян (2005), «Сложность доказательства» (PDF) , в Лаптев, А. (ред.), Труды 4-го Европейского математического конгресса , Цюрих: Европейское математическое общество, стр. 221–231, MR 2185746
Крайичек, Ян, Сложность доказательства , Cambridge University Press, 2019.
Пудлак, Павел (1998), "Длина доказательств", в Buss, SR (ed.), Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, 137 , Amsterdam: North-Holland, pp. 547–637 , DOI : 10.1016 / S0049-237X (98) 80023-2 , MR 1640332

Languages

In other projects