Профессор Калаи: «Протокол Sumcheck — это хлеб с маслом систем доказательств»

MIT OpenCourseWare 6,7 тыс. 1 ч 53 мин 9 мин 29.01.2025
Главное

В рамках открытого курса MIT OpenCourseWare профессор Яэль Калаи представляет детальный анализ интерактивных доказательств с двойной эффективностью (doubly efficient interactive proofs). Прослеживая эволюцию от классического протокола Sumcheck до архитектуры GKR, лекция раскрывает, как сложные структурированные вычисления могут быть верифицированы практически мгновенно. Главным связующим звеном теории становится теорема о расширении низкой степени, превращающая хаотичные наборы данных в строгие математические объекты.

📅 Организационные моменты и квантовый алгоритм Регева 0:13

Лекция начинается с разбора организационных планов на ближайшие недели. Ввиду праздников и запланированной поездки профессора Калаи в Германию расписание занятий претерпит изменения: одну из лекций проведет исследовательница Рейчел. Однако ключевым событием осеннего семестра, по словам Калаи, станет лекция 6 октября. Вместо стандартного занятия студенты посетят выступление Одеда Регева (Oded Regev) из Парижа, который представит свой новый квантовый алгоритм факторизации.

По мнению Калаи, эта работа является крайне захватывающей, поскольку она существенно улучшает знаменитый алгоритм Шора. Формат мероприятия объединит в себе коллоквиум и группу по чтению теории: первый час будет посвящен общему обзору для широкой аудитории, а последующие два часа — детальному разбору алгоритма и дискуссии.

🍞 Протокол Sumcheck: «хлеб с маслом» систем доказательств 2:15

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

Назначение протокола Sumcheck состоит в эффективной проверке того, что сумма многочлена от нескольких переменных по некоторому небольшому множеству $H$ (например, булеву кубу ${0,1}^m$) равна определенному значению в конечном поле. Напрямую вычислить такую сумму крайне долго — это требует выполнения порядка $|H|^m$ операций.

Однако интерактивный протокол позволяет верификатору убедиться в правильности результата за полилогарифмическое время при условии, что у него есть оракульный доступ к функции. Одним из первых знаковых применений этой техники стала интерактивная верификация для задачи Sharp-SAT (#SAT). Это было достигнуто благодаря методу арифметизации — перевода булевой схемы в арифметическую.

📐 Теорема о расширении низкой степени (Low-Degree Extension) 4:33

В традиционных интерактивных доказательствах все внимание исследователей было сосредоточено исключительно на эффективности верификатора, тогда как время работы доказывающего (prover) игнорировалось — его условно считали всемогущим. В концепции интерактивных доказательств с двойной эффективностью ситуация меняется: время работы доказывающего теперь также имеет критическое значение. Как иронично замечает Яэль Калаи, в нашем мире нет всемогущих сущностей. Доказывающий по-прежнему мощнее верификатора (иначе верификатор делал бы всю работу сам), но его вычисления не должны быть безумно дорогими.

Инструментом, который дает протоколу Sumcheck его колоссальную силу, является теорема о расширении низкой степени (Low-Degree Extension, LDE). Калаи подчеркивает, что из комбинации LDE и Sumcheck практически в виде следствий вытекает большинство результатов в этой области.

Формулировка теоремы LDE гласит, что для любой функции $f: H^m \to {0,1}$, где $H$ — любое дискретное множество, и для любого конечного поля $F$, содержащего $H$, существует единственное полиномиальное расширение $\tilde{f}: F^m \to F$, удовлетворяющее двум условиям.

Если $H = {0,1}$, то степень по каждой переменной равна 1. Такое расширение называют тривиальным мультилинейным расширением (multilinear extension). По мнению профессора Калаи, главная ценность теоремы заключается в возможности навязать жесткую структуру низкой степени любому хаотичному и произвольному набору бит. Как только структура получена, к ней сразу становится применимым протокол Sumcheck.

🔍 Доказательство единственности и структуры расширения 12:38

Для одномерного случая ($m=1$) теорема LDE превращается в классическую интерполяцию Лагранжа. В этом случае расширение $\tilde{f}(x)$ представляется в виде явной суммы произведений значений функции на полиномы-селекторы $\chi_h(x)$, которые равны 1 при совпадении аргумента с $h$ и 0 во всех остальных точках множества $H$.

Для многомерного пространства формула расширения аналогична:

$$\tilde{f}(Z) = \sum_{h_1, \dots, h_m \in H^m} f(h_1, \dots, h_m) \cdot \chi_{h_1, \dots, h_m}(Z)$$

Где многомерный селектор представляет собой простое произведение одномерных полиномов Лагранжа $\prod_{i=1}^m \chi_{h_i}(x_i)$.

Единственность такого расширения доказывается от противного. Предположим, существуют два различных расширения. Их разность даст ненулевой полином $g$, который на всем гиперкубе $H^m$ равен нулю, имея при этом степень по каждой переменной не выше $|H|-1$. Поскольку $g$ не равен нулю тождественно во всем поле, найдется точка $(t_1, \dots, t_m) \in F^m$, где $g(t_1, \dots, t_m) \neq 0$.

Двигаясь поочередно по каждой координате с помощью индукции и опираясь на единственность интерполяции Лагранжа, исследователи неизбежно находят точку внутри малого гиперкуба $H^m$, где функция $g$ также не равна нулю. Это создает явное противоречие с исходным допущением.

В ходе лекции один из студентов предлагает альтернативный комбинаторный метод доказательства через подсчет коэффициентов полиномов, с чем Калаи соглашается. Другой студент (Винод) замечает, что если исходная функция $f$ не имеет структуры, вычисление расширения $\tilde{f}$ потребует колоссального времени порядка $|H|^m$. Калаи подтверждает этот вывод: платой за универсальность метода LDE становится его высокая вычислительная сложность в общем случае, однако в конкретных интерактивных сценариях эта избыточность успешно преодолевается.

🔺 Практический пример: подсчет треугольников в графе 32:47

Чтобы продемонстрировать совместную силу LDE и Sumcheck, профессор разбирает задачу подсчета треугольников в графе $G$. Традиционный детерминированный алгоритм требует времени $O(n^3)$, перебирая все тройки вершин. Представим верификатора, чьи ресурсы ограничены временем $O(n^2)$ (что сопоставимо с размером матрицы смежности), из-за чего он физически не способен запустить кубический перебор. Доказывающий может прийти на помощь и убедить верификатора в том, что число треугольников в графе равно в точности $\beta$.

Для построения протокола матрица смежности графа кодируется как функция $f: {0,1}^{\log n} \times {0,1}^{\log n} \to {0,1}$. Значение $f(i,j)$ равно 1, если между вершинами $i$ и $j$ есть ребро, и 0 в противном случае. Математически число треугольников выражается формулой:

$$\text{Triangles} = \frac{1}{6} \sum_{i,j,k} f(i,j) \cdot f(j,k) \cdot f(i,k)$$

Поскольку булева функция $f$ изначально не имеет алгебраической структуры, к ней применяется мультилинейное расширение $\tilde{f}$. Формула суммы при этом не меняется, так как на элементах исходного куба значения $\tilde{f}$ и $f$ эквивалентны. Полученное выражение представляет собой полином степени 2 по каждой переменной, к проверке которого напрямую применяется протокол Sumcheck.

В конце протокола верификатору нужно лишь вычислить значение полинома в одной случайно выбранной точке поля. Это требует всего около $O(n^2)$ шагов. Время работы самого доказывающего возрастает до полиномиального (около $O(n^5)$), но требования двойной эффективности соблюдаются.

Студент по имени Гейб предлагает альтернативный, еще более простой протокол, где доказывающий присылает матрицы $A^2$ и $A^3$, а число треугольников вычисляется через след (trace) матрицы $A^3$. Проверка корректности перемножения матриц осуществляется черезReed-Solomon кодирование. Калаи отмечает изящество этой идеи, ссылаясь также на фундаментальную работу RRR (Ротблум, Вадхан, Вигдерсон), предлагающую константную раундовую сложность для подобных проверок.

⚡ Протокол GKR: верификация неглубоких вычислений 48:50

Главный триумф связки LDE и Sumcheck раскрывается в протоколе GKR (названном в честь авторов Гольдвассер, Калаи и Ротблума). Протокол позволяет верифицировать любые вычисления, представимые в виде «неглубоких» (shallow) схем с малой глубиной $d$, но огромным количеством элементов (размером $S$). Цель протокола — позволить верификатору убедиться, что результат вычисления схемы на входе $x$ равен 1. При этом верификатор затратит время, линейно зависящее от глубины $d$ и полилогарифмическое от размера $S$, а доказывающий выполнит работу за полином от $S$.

Чтобы верификатор мог работать быстрее, чем размер самой схемы $S$, схема должна обладать свойством единообразия (logspace uniformity) — то есть описываться лаконичной машиной Тьюринга, позволяющей вычислять структуру связей между гейтами на лету.

Для простоты накладываются следующие структурные допущения:

Идея GKR состоит в последовательном сведении утверждения о корректности слоя $i$ к утверждению о слое $i+1$. Простая погейтовая проверка (gate-by-gate) неэффективна: если верификатор будет случайно выбирать один из двух входов для проверки гейта ИЛИ, то на каждом слое вероятность поймать обманщика будет падать вдвое, превращая общую надежность в ничтожно малую величину $1/2^d$.

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

🧩 Анатомия шага GKR и проблема удвоения утверждений 1:14:54

В начале вычислений доказывающий переводит схему в арифметический вид, заменяя логические гейты операциями сложения и умножения. Значения всех гейтов на слое $i$ кодируются в виде функции $V_i: H^m \to {0,1}$, где размер гиперкуба $|H|^m = S$. Калаи объясняет тонкий выбор параметров: вместо привычного двоичного базиса ($H={0,1}$), для будущих применений в теории PCP (доказательств, проверяемых вероятностно) критически важно выбирать размер множества $H = \log S$, а число переменных $m = \log S / \log \log S$. Это связано с тем, что размер поля $F$ должен быть полиномиально связан с $H$, иначе размер объектов вырастет сверх меры.

Протокол стартует с утверждения о выходе схемы в некоторой точке $Z_0$: доказывающий заявляет, что значение мультилинейного расширения равно $V_0(Z_0) = 1$. Пользуясь определением LDE, значение функции в любой точке $Z_i$ для слоя $i$ можно расписать через сумму по исходному гиперкубу:

$$\tilde{V}i(Z_i) = \sum{P \in H^m} V_i(P) \cdot \chi(P, Z_i)$$

Чтобы связать текущий слой со слоем ниже, Калаи вводит предикаты связей (wiring predicates) — полиномы $add_i(P, w_1, w_2)$ и $mult_i(P, w_1, w_2)$. Они возвращают 1, если гейт $P$ на слое $i$ является соответственно сложением или умножением гейтов $w_1$ и $w_2$ на слое $i+1$, и 0 в противном случае. Значение гейта $V_i(P)$ подменяется масштабным алгебраическим выражением:

$$V_i(P) = \sum_{w_1, w_2} \left[ add_i(P, w_1, w_2)(\tilde{V}{i+1}(w_1) + \tilde{V}{i+1}(w_2)) + mult_i(P, w_1, w_2)(\tilde{V}{i+1}(w_1) \cdot \tilde{V}{i+1}(w_2)) \right]$$

Подставляя это в исходную формулу, верификатор получает гигантскую сумму по переменным $P, w_1, w_2$ (размерность пространства $3m$), к которой запускается интерактивный протокол Sumcheck. В финале раунда Sumcheck верификатор заменяет переменные суммирования на случайные точки поля $(Z_0, Z_1, Z_2)$. Для успешного завершения проверки ему необходимо вычислить значения предикатов связей $\widetilde{add}i$ и $\widetilde{mult}_i$, а также два значения расширения для нижнего слоя: $\tilde{V}{i+1}(Z_1)$ и $\tilde{V}_{i+1}(Z_2)$.

В рамках «чистого» (bare bones) протокола предполагается, что верификатор имеет оракульный доступ к структуре графа схемы и может сам посчитать расширения предикатов $\widetilde{add}_i$ и $\widetilde{mult}_i$. Но возникает фундаментальное препятствие: вместо одного исходного утверждения о слое $i$, верификатор получает два независимых утверждения о слое $i+1$ в точках $Z_1$ и $Z_2$.

Если на каждом из $d$ слоев число проверяемых точек будет удваиваться, к концу вычислений верификатору придется проверять $2^d$ значений, что полностью уничтожает идею эффективности. «Это идеальный момент, чтобы прерваться на перерыв», — подводит итог Яэль Калаи, оставляя интригу разрешения этой проблемы для следующей части лекции.

💬 Цитаты

«Протокол Sumcheck, просто чтобы резюмировать, — это способ доказать, что сумма многочлена от нескольких переменных по небольшому множеству равна некоторому значению.»

Яэль Калаи 02:43

«Этот протокол — действительно хлеб с маслом систем доказательств. Почти каждая система доказательств использует этот протокол.»

Яэль Калаи 03:23

«В классической среде интерактивных доказательств все внимание уделялось эффективной верификации. Никого не волновало время работы доказывающего.»

Яэль Калаи 04:33
👥 Спикер
🔗 Упомянутые сайты и проекты
📖 Термины
Расширение низкой степени (LDE)
Метод кодирования произвольного набора данных в уникальный многочлен, степень которого по каждой переменной ограничена.
Протокол Sumcheck
Интерактивный протокол, позволяющий проверить корректность суммы значений полинома без полного перебора точек.
Протокол GKR
Интерактивный метод верификации вычислений, сводящий проверку всей схемы к послойному анализу полиномов.
Арифметизация
Процесс преобразования логической булевой схемы (состоящей из И/ИЛИ) в систему алгебраических уравнений над полем.
Предикаты связей (Wiring predicates)
Математические функции, описывающие топологию схемы и определяющие, какие гейты нижнего слоя соединены с верхним.
📊 Цифры
🗓 Хронология
  1. 29 сентября Лекция исследовательницы Рейчел в MIT на время отсутствия профессора Калаи.
  2. 6 октября Специальный доклад Одеда Регева о новом квантовом алгоритме факторизации, улучшающем алгоритм Шора.
⚖️ Другая сторона
Технологии и IT Протокол GKR Протокол Sumcheck Расширение низкой степени Яэль Калаи MIT OpenCourseWare