Когда дело доходит до сложных задач, специалисты по информатике часто заходят в тупик. Рассмотрим, например, известную задачу о поиске кратчайшего маршрута туда и обратно, проходящего через каждый город на карте ровно один раз. Все известные методы решения этой «задачи коммивояжёра» работают очень медленно на картах с большим количеством городов, и исследователи подозревают, что не существует способа их оптимизировать. Но никто не знает, как это доказать.
Более 50 лет исследователи в области теории вычислительной сложности пытаются превратить интуитивные утверждения, такие как «задача коммивояжёра сложна», в железобетонные математические теоремы, но без особого успеха. Всё чаще они также ищут строгие ответы на связанный с этим и более туманный вопрос: почему их доказательства не увенчались успехом?
Эта работа, в которой процесс математического доказательства рассматривается как объект математического анализа, является частью известной своей сложностью области, называемой метаматематикой. Метаматематики часто тщательно изучают основные предположения, или аксиомы, которые служат отправной точкой для всех доказательств. Они изменяют исходные аксиомы, а затем исследуют, как эти изменения влияют на теоремы, которые они могут доказать. Когда исследователи используют метаматематику для изучения теории сложности, они пытаются составить карту того, что различные наборы аксиом могут и не могут доказать о вычислительной сложности. Они надеются, что это поможет им понять, почему их попытки доказать сложность задач не увенчались успехом.
В статье, опубликованной в прошлом году, три исследователя применили к этой задаче новый подход. Они инвертировали формулу, которую математики использовали на протяжении тысячелетий: вместо того, чтобы начинать со стандартного набора аксиом и доказывать теорему, они заменили одну из аксиом теоремой, а затем доказали её. Они использовали этот подход, называемый реверсивной математикой, чтобы доказать, что многие различные теоремы в теории сложности на самом деле являются эквивалентными.
«Я был удивлён, что им удалось сделать так много», — сказал Марко Кармозино, теоретик сложности из IBM. «Позже люди посмотрят на это и скажут: „Вот что привело меня в метаматематику“».
Голубиные доказательства
История статьи по обратной математике началась летом 2022 года, когда Лицзе Чен, теоретик сложности, ныне работающий в Калифорнийском университете в Беркли, заканчивал свою докторскую диссертацию. У него появилось много свободного времени, и он решил посвятить несколько месяцев чтению литературы по метаматематике.
«Поскольку я заканчивал учёбу, у меня было немного исследовательской работы, — сказал Чен. — Я решил, что мне нужно изучить что-то новое».
Читая, Чен начал размышлять об одной из ветвей теории сложности, называемой коммуникационной сложностью. В ней изучается информация, которой два или более человек должны обменяться для выполнения определённых задач. Одна из простейших задач в коммуникационной сложности, называемая «проблемой равенства», похожа на игру. Два игрока начинают с отдельных строк из нулей и единиц (или битов). Их цель — с помощью минимального количества переданных данных определить, одинаковы ли их строки. Самая простая стратегия заключается в том, что один игрок просто отправляет свою полную строку другому для проверки. Есть ли способ сделать это лучше?
Теоретики сложности ещё несколько десятилетий назад доказали, что ответ — нет. Чтобы решить проблему равенства, игроки должны отправить как минимум количество битов, равное количеству в полной строке. Теоретики говорят, что эта длина строки является «нижней границей» необходимого объёма коммуникации.
Чен не сосредоточился на нижней границе проблемы равенства как таковой — его интересовало, как исследователи доказали её. Все известные доказательства основаны на простой теореме, называемой принципом голубей и ящиков (или ��ринципом Дирихле), которая гласит, что если попытаться поместить некоторое количество голубей в меньшее количество ящиков, то по крайней мере в одном ящике окажется более одной птицы. Это может показаться само собой разумеющимся, но это утверждение оказывается удивительно мощным инструментом в теории сложности и за её пределами.
Чен наткнулся на интригующую подсказку, что связь между проблемой равенства и принципом Дирихле может быть и обратной. Принцип Дирихле легко использовать для доказательства нижней границы проблемы равенства. А можно ли использовать нижнюю границу для доказательства принципа Дирихле?
Странное равенство
Чен обсудил свою идею с Цзяту Ли, в то время студентом Цинхуаского университета, с которым Чен незадолго до этого сотрудничал над другой статьёй. Чтобы сделать связь строгой, им нужно было выбрать набор аксиом, с которыми они будут работать. Исследователи в области метаматематики предпочитают использовать аксиомы, которые являются более ограниченными, чем типичные. Эти более слабые аксиомы упрощают определение точных отношений между различными теоремами. Чен и Ли решили работать с популярным набором аксиом, называемым PV1. PV1 достаточно силён, чтобы самостоятельно доказать некоторые важные теоремы о вычислительной сложности. Добавьте конкретную версию принципа голубей и ящиков в качестве дополнительной аксиомы, и вы также сможете доказать нижнюю границу проблемы равенства. В декабре 2022 года Ли и Чен официально показа��и, что, как и предполагал Чен, доказательство также работает, если две теоремы переставить местами.
Тот факт, что можно доказать нижнюю границу проблемы равенства на основе принципа голубей и ящиков или наоборот, означает, что в логической структуре PV1 эти две теоремы являются точно эквивалентными. Когда Ли и Чен обсуждали результат с Игорем Оливейра, теоретиком сложности из Уорикского университета, трое учёных поняли, что их метод обратной математики может также работать для теорем в других отдалённых областях теории сложности. В течение следующих нескольких месяцев они систематически доказали эквивалентность многих других теорем.
«Вначале у нас было только два эквивалентных понятия, — сказал Чен. — Но теперь у нас есть целая сеть взаимосвязей».
Наиболее поразительная связь, обнаруженная командой, касалась одной из первых теорем, с которой студенты сталкиваются на вводных курсах по теории сложности, и которая связана с той же версией принципа ящиков. Эта «классическая теорема», как её описал Кармосино, устанавливает нижнюю границу времени, необходимого для теоретического компьютера, называемого одномерной машиной Тьюринга, чтобы определить, является ли строка из нулей и единиц палиндромом (то есть читается ли она одинаково в прямом и обратном направлении). Ли, Чен и Оливейра использовали обратную математику, чтобы доказать, что в рамках PV1 эта теорема о нижней границе палиндрома эквивалентна принципу голубей и ящиков.
«Если бы вы мне это сказали раньше, я бы не поверил, — сказал Чен. — Это звучит совершенно нелепо».
Эквивалентность нижней границы палиндрома и принципа Дирихле удивительна, потому что эти две теоремы на первый взгляд очень отличаются друг от друга. Принцип голубей и ящиков по сути не имеет ничего общего с вычислениями: это простое утверждение о подсчёте. Нижняя граница палиндрома, с другой стороны, является утверждением о конкретной модели вычислений. Новый результат подразумевает, что такие, казалось бы, узкие теоремы являются более общими, чем кажется.
«Это говорит о том, что нижние границы сложности, которые мы хотим понять, гораздо более фундаментальны», — сказал Оливейра.
Скрытно одинаковые
Три следующих внешне разных теоремы логически эквивалентны.
Принцип Дирихле (принцип голубей и ящиков)
Если поместить большее число голубей в меньшее число ящиков, то хотя бы в одном ящике окажется больше одного голубя.
Нижняя граница для проверки равенства
Двум людям с разными сообщениями нужно поделиться определённым минимальным количеством информации, чтобы определить, одинаковы ли их сообщения.
Нижняя граница для проверки палиндрома
Одномерная машина Тьюринга требует определённого минимального времени, чтобы определить, является ли строка битов палиндромом.
Неизведанная территория
Эта новая сеть эквивалентностей также помогла пролить свет на ограничения PV1. Исследователи уже имели основания полагать, что принцип голубей и ящиков нельзя доказать, опираясь только на аксиомы PV1, поэтому результаты Ли, Чена и Оливейры предполагают, что их другие эквивалентные теоремы также, вероятно, недоказуемы в PV1.
«Я думаю, что это прекрасно», — сказал Ян Пич, теоретик сложности из Оксфордского университета, который в 2014 году доказал важный результат о силе PV1. Но он предупредил, что подход обратной математики может быть наиболее полезен для выявления новых связей между теоремами, которые исследователи уже доказали. «Насколько мы можем судить, это не даёт нам много информации о сложности утверждений, которые мы не знаем, как доказать».
Понимание этой неизведанной территории остаётся далёкой целью для исследователей метаматематики. Но это не охладило энтузиазм Ли по отношению к этой теме. В 2023 году он поступил в аспирантуру Массачусетского технологического института, а недавно написал 140-страничное руководство по метаматематике для теоретиков сложности. Это один из примеров более широкой тенденции: после десятилетий относительной неизвестности метаматематика всё больше привлекает внимание более широкого круга исследователей, которые привносят в эту область новые перспективы.
«Люди устали от застоя, — сказал Кармосино. — Пришло время сделать шаг назад и проработать базу».
