Строгость, ведущая к пониманию

На MathOverflow Тимоти Гауэрс задал вопрос под названием « Демонстрируя, что строгость важна ». Большая часть обсуждения была посвящена случаям, показывающим важность доказательств, в которых, вероятно, нет необходимости убеждать людей на CSTheory. По моему опыту доказательства должны быть более строгими в теоретической информатике, чем во многих частях непрерывной математики, потому что наша интуиция так часто оказывается неправильной для дискретных структур, и потому что стремление создавать реализации поощряет более подробные аргументы. Математик может быть доволен доказательством существования, но теоретик-компьютерщик обычно пытается найти конструктивное доказательство. Локальная лемма Ловаша является хорошим примером [1].

Поэтому я хотел бы знать

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

Недавним примером, который не является прямым следствием алгоритмов и теории сложности, является теоретико-теоретический синтез , автоматический вывод правильных и эффективных алгоритмов из предварительных и постусловий [2].

• [1] Робин А. Мозер и Габор Тардос . Конструктивное доказательство локальной леммы генерала Ловаша , JACM 57 , статья 11, 2010 г. http://doi.acm.org/10.1145/1667053.1667060
• [2] Саурабх Шривастава, Сумит Гулвани и Джеффри С. Фостер. От проверки программы к обобщению программы , ACM SIGPLAN Notices 45 , 313–326, 2010. http://doi.acm.org/10.1145/1707801.1706337

Редактировать:Ответ, который я имел в виду, похож на ответ Скотта и Матуса. Как предположил Каве, это тройка того, что люди хотели доказать (но это не обязательно было неожиданно для «физики», «рукопожатия» или «интуитивных» аргументов), доказательство и последствия для «основной проблемы», которую следовало из того доказательства, которое не было ожидаемым (возможно, создание доказательства потребовало неожиданных новых идей, или, естественно, привело к алгоритму, или изменило наш взгляд на область). Методы, разработанные при разработке доказательств, являются строительными блоками теоретической информатики, поэтому, чтобы сохранить ценность этого несколько субъективного вопроса, стоило бы сосредоточиться на личном опыте, таком как предоставленный Скоттом, или на аргументе, подкрепленном ссылками, как и Матус Кроме того, я я пытаюсь избежать споров о том, имеет ли что-то право или нет; к сожалению, природа вопроса может быть по сути проблематичной.

У нас уже есть вопрос об «удивительных» результатах в сложности: « Удивительные результаты в сложности» (нет в списке блогов о сложности), поэтому в идеале я ищу ответы, которые фокусируются на ценности строгих доказательств , а не на размере прорыва.

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

Когда я был старшекурсником, первая настоящая проблема TCS, с которой я столкнулся, заключалась в следующем: какой самый быстрый квантовый алгоритм оценивает OR из √n AND из √n булевых переменных каждая? Мне и всем остальным, с кем я говорил, было до боли очевидно, что лучшее, что вы можете сделать, - это рекурсивно применять алгоритм Гровера, как к операционному оператору, так и к логическому оператору. Это дало верхнюю оценку O (√n log (n)). (На самом деле вы можете сбрить логарифмический фактор, но давайте пока проигнорируем это.)

К моему огромному разочарованию, однако, я не смог доказать какую-либо нижнюю границу лучше, чем тривиальное Ω (n ^1/4 ). «Идущий физик» и «ответ рукой» никогда не выглядели более привлекательными! :-D

Но затем, спустя несколько месяцев, Андрис Амбайнис (Andris Ambainis) выступил со своим квантовым методом противника , основным применением которого вначале была оценка Ω (√n) для OR-of-AND. Чтобы доказать этот результат, Андрис представил подачу квантового алгоритма суперпозиции различных входных данных; Затем он изучил, как запутанность между входами и алгоритмом увеличивалась с каждым запросом алгоритма. Он показал, как этот подход позволяет ограничивать сложность квантовых запросов даже для «грязных» несимметричных задач, используя только очень общие комбинаторные свойства функции f, которые пытается вычислить квантовый алгоритм.

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

Конечно, это «просто еще один день в чудесном мире математики и TCS». Даже если все «уже знают», что X верен, доказательство X очень часто требует изобретения новых методов, которые затем применяются далеко за пределами X, и, в частности, для задач, для которых правильный ответ априори был гораздо менее очевиден .

Параллельное повторение - хороший пример из моей области:

Краткое объяснение параллельного повторения. Предположим , что у вас есть система доказательства два-Доказывающий для языка : С учетом входного х , известный всем, верификатор посылает вопрос д 1 к Доказывающий 1, и вопрос д 2 к Доказывающий 2. испытатели ответ с ответами 1 и 2 соответственно без общения. Верификатор выполняет некоторые проверки на в 1 и в 2 ( в зависимости от д 1 , д 2 ) , и решает , следует ли принять или отклонить. Если x ∈ $L$$x$$q_1$$q_2$$a_1$$a_2$$a_1$$a_2$$q_1,q_2$$x\in L$, существует стратегия проверки, которую всегда принимает верификатор. Если , для любой стратегии проверки, верификатор принимает с вероятностью не более s («вероятность ошибки»).$x\not\in L$$s$

Теперь предположим, что мы хотим меньшую вероятность ошибки. Может быть, близко к 1 , и мы хотим, чтобы s = 10 - 15 . Естественным подходом будет параллельное повторение : пусть проверяющий отправит k независимых вопросов каждому проверяющему, q ( 1 ) 1 , … , q ( k ) 1 и q ( 1 ) 2 , … , q ( k ) 2 , получит k ответов от испытателей $s$$1$$s = 10^{-15}$$k$$q_1^{(1)},\ldots,q_1^{(k)}$$q_2^{(1)},\ldots,q_2^{(k)}$ иa ( 1 ) 1 ,…,a ( k ) 1 и выполняетkпроверок ответов.$a_1^{(1)},\ldots,a_1^{(k)}$$a_1^{(1)},\ldots,a_1^{(k)}$$k$

История. Сначала было «ясно», что вероятность ошибки должна уменьшиться как , как если бы верификатор сделал k последовательных проверок. Легенда гласит, что это было дано студенту, чтобы доказать, прежде чем стало понятно, что «очевидное» утверждение просто ложно. Вот пример контрпримеров: http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf . Потребовалось некоторое время (и несколько более слабых результатов), прежде чем Ран Раз окончательно подтвердил, что вероятность ошибки действительно экспоненциально уменьшается, но имеет немного сложное поведение: это s Ω ( k / log | Σ |$s^{k}$$k$$s^{\Omega(k/\log|\Sigma|)}$где алфавит - это множество возможных ответов пруверов в исходной системе. В доказательстве использовались теоретико-информационные идеи, и, как говорили, он был вдохновлен идеей Разборова в сложности коммуникации. Грязная часть оригинального доказательства Рана была впоследствии красиво упрощена Томасом Холенштейном, что привело к одному из моих любимых доказательств.$\Sigma$

Взгляд на проблему и другие последствия. Сначала есть непосредственные вещи: лучшее понимание количественного поведения параллельного повторения и роли, которую играет алфавит , лучшее понимание того, когда проверяющие могут использовать параллельные вопросы для обмана, лучшее понимание важности независимости параллельное повторение между k парами вопросов (позднее оформленных Фейге и Килианом).$\Sigma$$k$

Затем появились расширения, которые стали возможными: Ануп Рао смог адаптировать анализ, чтобы показать, что когда исходная система доказательств представляет собой {\ em проекционную игру}, т. Е. Ответ первого испытателя определяет не более одного приемлемого ответа: второе доказательство - нет никакой зависимости от алфавита, и постоянная в показателе степени может быть улучшена. Это важно, поскольку большая часть результатов аппроксимации основана на проекционных играх, а уникальные игры являются частным случаем проекционных игр. Также есть количественные улучшения в играх на экспандерах (Рики Розен и Ран Раз) и многое другое.

Тогда есть далеко идущие последствия. Всего несколько примеров. Информационно-теоретическая лемма из статьи Раза использовалась во многих других контекстах (в криптографии, в эквивалентности выборки и поиска и т. Д.). Метод «коррелированной выборки», который использовал Холенштейн, применялся во многих других работах (в области сложности коммуникации, в PCP и т. Д.).

Еще один хороший пример строгости (и новых методов), необходимых для доказательства утверждений, которые считались верными: сглаженный анализ. Два рассматриваемых случая:

• Симплексный алгоритм
• Алгоритм k-средних

$k$$O(n^{c \cdot kd})$$n$

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

Роберт Э. Шапире. Сила слабой обучаемости. Машинное обучение, 5 (2): 197-227, 1990.

$\epsilon>0, \delta>0$$1-\delta$$\epsilon$$\epsilon$$\delta$$\delta$$\delta$$\gamma$

Во всяком случае, все стало очень интересно после работы Шапире. Его решение породило большинство над гипотезами в исходном классе. Затем пришли:

Йоав Фрейнд. Усиление слабого алгоритма обучения большинством. Информация и вычисления, 121 (2): 256-285, 1995.

В этой статье было «обличение» результата Шапира, но теперь построенная гипотеза использовала только одно большинство. Вдоль этих строк оба затем произвели еще одно упрек, названный AdaBoost:

Йоав Фрейнд и Роберт Э. Шапире. Теоретическое обобщение он-лайн обучения и приложение для повышения. Журнал компьютерных и системных наук, 55 (1): 119-139, 1997.

Вопрос о слабом / сильном обучении начинался как теоретическая проблема, но эта последовательность «упреков» привела к красивому алгоритму, одному из наиболее влиятельных результатов в машинном обучении. Я мог бы пойти на все виды касательных здесь, но сдержусь. В контексте TCS эти результаты дышат большой жизнью в контексте (1) алгоритмов мультипликативного веса и (2) результатов сложного набора. Что касается (1), я просто хотел бы уточнить, что AdaBoost можно рассматривать как пример мультипликативной работы Warmuth / Littlestone, основанной на весовых коэффициентах / веялке (Фрейнд был студентом Warmuth), но есть много нового в повышении полученные результаты. О (2), я

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

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

Этот пример соответствует ответам Даны и Скотта.

$n$$d$$d$$2^{n-1}$$d$$2$$n^{1/(d-1)}$$2^{n^{1/(d-1)}}$$1$$n^{1/(d-1)}$$d-1$$2^{n^{1/(d-1)}}$$2^{n^{1/(d-1)}}$$d$$2^{O(n^{1/(d-1)})}$

$d$$AC^0$

Статья Расборова и Рудича «Естественные доказательства» предлагает строгое доказательство (формализацию) болезненно очевидного утверждения « Действительно трудно доказать, что P ≠ NP».

Идея о том, что некоторые алгоритмические проблемы требуют экспоненциального числа шагов или исчерпывающего поиска по всем возможностям, возникла с 50-х годов и, возможно, раньше. (Конечно, конкурирующая наивная идея о том, что компьютеры могут делать все, была также распространена.) Главный прорыв Кука и Левина состоял в том, чтобы поставить эту идею на строгие основания. Это, конечно, все изменило.

Обновление: я только что понял, что мой ответ, как хороший ответ Тюркистани, касается названия вопроса «строгость, ведущая к пониманию», но, возможно, не конкретной формулировки, которая была о «строгом доказательстве теоремы».

Алан Тьюринг формализовал понятие алгоритма (эффективной вычислимости) с использованием машин Тьюринга. Он использовал этот новый формализм, чтобы доказать, что проблема Остановки неразрешима (т.е. проблема Остановки не может быть решена никаким алгоритмом). Это привело к длительной исследовательской программе, которая доказала невозможность 10-й проблемы Гильберта. Матиясевич в 1970 году доказал, что не существует алгоритма, который мог бы решить, имеет ли целочисленное диофантово уравнение целочисленное решение.