LLM: генерация гипотез против проверки доказательств

Где-то между второй и третьей чашкой кофе многие специалисты по теории сложности недавно прочитали фразу, которую никак не ожидали увидеть: детерминированный алгоритм, который считает выполняющие назначения произвольной булевой формулы за время примерно 2^(n/√(log n)) — субэкспоненциальное, в точном техническом смысле, опровергающем Гипотезу об экспоненциальном времени (ETH), одно из несущих допущений области. Заявление появилось не от университетской группы на arXiv. Его выпустила AI-лаборатория, а доказательство разработали совместно с большой языковой моделью. Что бы вы ни думали об анонсе, он отмечает момент, когда генерация гипотез — машины, которые предлагают новую математику, а не только оценивают чужую — вышла из стадии демо.

Лаборатория объединила три результата: упомянутый выше сенсационный результат по теории сложности, заявленное доказательство гипотезы Какейи во всех размерностях и результат по физике, описанный как унифицированное завершение Стандартной модели, который придержали до формальной верификации. Реакция раскололась по знакомой схеме: искреннее восхищение содержанием и искреннее раздражение упаковкой. Критики сравнили это с производителем велосипедов, который объявляет о своих победах в велогонках. Метко — но содержание заслуживает более медленного взгляда, ведь в этом анонсе скрыт реальный урок о двух очень разных способах, которыми языковые модели сейчас касаются математики, и о том, какому из них стоит доверять.

Что на самом деле заявляет AI-анонс в математике

Начнём с результата по сложности, у него самые понятные ставки. Гипотеза об экспоненциальном времени утверждает, грубо говоря, что 3-SAT нельзя решить за время 2^o(n) — ни один алгоритм не может быть существенно субэкспоненциальным по числу переменных. Сотни работ в параметризованной и тонкой теории сложности опираются на ETH при доказательстве нижних оценок; это то допущение, на которое складывают целую карьеру теорем вида «при условии ETH». Новая препринт-работа описывает детерминированный алгоритм подсчёта для k-CNF формул, который использует полиномиальную память и работает за время 2^(n/(log n)^(1/2+o(1))), умноженное на полиномиальный множитель. Показатель степени равен o(n), а это ровно то, что ETH запрещает. Алгоритм по-прежнему чудовищно медленный — на реальном примере его не запустит никто — но асимптотически это решающий результат. Если доказательство выдержит проверку, гипотеза, на которой двадцать лет держались нижние оценки, просто перестаёт существовать.

Второе утверждение касается гипотезы Какейи — задачи геометрической теории меры о наименьших множествах, которые содержат единичный отрезок в каждом направлении. Трёхмерный случай был решён лишь в 2025 году в нашумевшем доказательстве Хун Ванга и Джошуа Залла, которое многие сочли венцом карьеры. Анонс заявляет о доказательстве во всех размерностях, что полностью поглотило бы этот прорыв. Третий результат, из квантовой теории поля, самый расплывчатый: его описывают как «унифицированное завершение Стандартной модели», но его ещё не опубликовали, предположительно он ждёт машинно проверенной формализации. Физики, читающие тизеры, подозревают что-то из семейства великих объединённых конструкций, а не буквальную теорию всего, и формулировки заслуженно вызывают прищур.

Две вещи в подаче заслуживают похвалы. Лаборатория привлекла работающих математиков и физиков до публикации — прямой ответ на волну критики после более раннего, неуклюжего математического анонса, после которого Терренс Тао и другие публично добивались именно такого взаимодействия. А результат по физике придержали до завершения формализации, и это правильный порядок приоритетов. Но остаются жёсткие вопросы без ответа: никто снаружи не знает счёт за вычисления, не знает, дали бы те же теоремы аналогичные деньги, направленные на людей-исследователей, и будет ли коммерческая лаборатория финансировать работу ради любопытства, когда у акционеров появится право голоса. Есть и неудобная петля, на которую критики указали сразу: эти модели частично обучались на вопросах, черновиках и постах на форумах того самого исследовательского сообщества, которое теперь просят аплодировать результату.

Проверка доказательств против генерации гипотез: две разные работы

Если убрать хайп, любая система ИИ для математики выполняет одну из двух задач. Первая — проверка доказательств: дан кандидат в аргументацию, решить, корректна ли она. Вторая — генерация гипотез: дана область задачи, предложить, что стоит попробовать — лемму, конструкцию, алгоритм, контрпример. Звучит как две половины одного навыка. Это не так. Это разные вычислительные задачи с разными оракулами, разными режимами отказа и совершенно разными профилями доверия, и смешивать их — значит либо переоценить пресс-релиз, либо отмахнуться от настоящего прогресса.

У проверки есть оракул. Доказательство на Lean либо компилируется против ядра, либо нет, и ядро не интересует, насколько уверенно звучал автор. Проверка падает громко — отвергнутый блок тактик однозначен. У генерации оракула нет. Предложенная гипотеза может быть верной, ложной, тривиально верной или верной, но опубликованной в 1987 году в других обозначениях. Генерация ломается тихо, и её сбои носят социальный характер: правдоподобная чушь или настоящие результаты, выданные за новизну. Качество здесь измеряется важностью и оригинальностью — свойствами, которые задаёт человеческий вкус, а не какой-либо разрешимый критерий.

Почему генерация внезапно стала достаточно хорошей, чтобы иметь значение? Потому что современные модели рассуждений обучаются на длинных цепочках рассуждений, а не только подталкиваются к ним промптами — обучение с подкреплением на проверяемых наградах, в основном на математике и коде, где ответы можно проверить механически, научило эти системы действительно перебирать пространство шагов, а не просто автодополнять один. Аналогию, которую я бы держал в голове: проверяющий — это компилятор, генератор гипотез — это дизайнер. Оба полезны. Но вы никогда и ни за что не позволите дизайнеру самому подписывать свою работу.

Доказательство, которое нельзя проверить, — это проповедь; гипотеза, которую нельзя проверить, — это слух.

Где выигрывает автоматическая проверка доказательств

Проверяющий выигрывает там, где есть формальная истина, а проверяемый артефакт слишком длинный или утомительный, чтобы человек проверял его построчно. Lean 4 и его общественная библиотека Mathlib стали де-факто ареной: вы пишете определения и доказательства на языке программирования, а небольшое, отдельно проверяемое ядро решает, легален ли каждый шаг вывода. Доверяемая база вычислений крошечная по сравнению с горой математики, построенной на ней, и именно эта асимметрия вам и нужна.

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

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

Обратите внимание, что пример показывает о разделении труда. Творческий ход — выбрать свидетеля k + l; проверочный ход — это ring, проверяющий алгебру. Люди и модели оба неплохо справляются с первым. Доверять можно только ядру во втором, и оно не устаёт, не пролистывает и не оценивает на глаз. Самый убедительный элемент всего анонса — как раз этот шлюз: утверждение, что статью по физике придержали до завершения формализации на Lean. Если это соответствует действительности, то работает именно задуманный процесс: машина предлагает, машина выносит решение, а пресс-релиз ждёт своей очереди.

Где выигрывает генерация гипотез

Генерация выигрывает там, где пространство поиска комбинаторно, а оценка дешёвая. DeepMind FunSearch задал шаблон ещё в 2023 году: языковая модель предлагает гипотезы в виде программ, быстрый оценщик их ранжирует, а эволюционный цикл сохраняет лучшие. Так были получены новые конструкции для cap sets и эвристики упаковки в контейнеры, превзошедшие десятилетия ручной настройки. AlphaEvolve развил ту же идею дальше и, среди прочего, сократил одно умножение в алгоритме умножения матриц 4×4, который держался со времён Штрассена. Никто не утверждает, что эти системы понимают геометрию. Им это не нужно. Им нужно предлагать, а оценщику нужно быть честным.

Алгоритм ETH вписывается в этот шаблон почти подозрительно хорошо. Пространство «алгоритмических идей» огромно, а человеческие исследователи исследуют его с сильными априорными представлениями — что вежливо означает слепые пятна. Конструкция, требующая сочетания конкретного приёма представления со специфической структурой рекурсии, может тридцать лет оставаться неисследованной просто потому, что путь поиска никого не привёл рядом. Исчерпывающий, свободный от априорных предубеждений, немного глуповатый поиск — именно то, что приносят машины. Та же логика лежит в основе циклов «генерируй и опровергай»: предложить гипотезу и сразу попытаться её убить вычислительным поиском контрпримеров на малых случаях. Большинство гипотез гибнет за считанные минуты, и это нормально — каждое опровержение уточняет следующее предложение, а выжившие — те, ради которых стоит потратить послеобеденное время человека.

Есть и психологическая асимметрия, которую стоит уважать. Трёхмерное доказательство Ванга и Залла по Какейе потребовало многих лет сосредоточенных усилий на самом верху области. Если поиск с участием модели действительно породил аргумент для всех размерностей, то он почти наверняка нашёл другой маршрут через ландшафт — не обязательно более глубокий, но другой. Разнообразие — это ровно то, для чего существует поиск. Опасность не в том, что машины генерируют гипотезы; она в том, что кто-то публикует сгенерированную гипотезу без механизмов, которые её подкрепляют. Это подводит нас к части конвейера, которую вам действительно нужно построить.

Построение петли верификации для доказательств, созданных ИИ

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

1. Генерируйте широко и дёшево. На этом этапе разнообразие важнее глубины; вам нужно покрытие пространства идей, а не одна отполированная попытка.
2. Дедуплицируйте по литературе. Поиск по arXiv и MathOverflow ловит самый частый провал: «новую» гипотезу, которая оказывается известным результатом в непривычных обозначениях.
3. Примените дешёвые эмпирические фильтры. Проверяйте малые случаи численно, ищите контрпримеры вычислительно и дайте очевидно ложным утверждениям умереть быстро.
4. Формализуйте выжившие. Lean, Isabelle или Rocq — выбирайте ассистента доказательств, но помните, что это самый дорогой шаг, а доказательство на естественном языке — это набросок, а не результат.
5. Человеческая проверка новизны и постановки. Это важно? Правильное ли утверждение вообще сформулировано? Модели оптимизируют то, что доказуемо; люди решают, что стоит доказывать.

Заявленная совместная работа примерно следовала этой схеме: исследователей привлекли до публикации, по сути, они укомплектовали пятый шаг. Это реальное улучшение по сравнению со старым подходом «выложить препринт и пусть соцсети его рецензируют». Но обратите внимание на асимметрию конвейера: шаги с первого по третий дешёвые и масштабируются с вычислениями, четвёртый шаг — узкое место, а пятый вообще не масштабируется. Если вы строите инструменты в этой области, тратьте деньги на узкое место — на лучшую автоформализацию, на лучшую обратную связь по ошибкам в генератор, — а не на более крупный и уверенный генератор.

Почему математики-люди всё ещё контролируют корректность

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

Затем есть вопрос происхождения. Эти модели обучались на собственных вопросах, черновиках и постах на форумах сообщества, что поднимает неприятную возможность: прославленное «открытие» может оказаться рекомбинацией того, что будущие рецензенты уже написали сами. Страх обогнать собственный инструмент — не паранойя, а проблема происхождения данных, и пока лаборатории не могут показать происхождение, человеческие рецензенты остаются единственными работающими детекторами плагиата. Добавьте политику признания — кого приглашают проверять, чьи имена стоят в анонсе, обвинения в фаворитизме — и станет понятно, почему человеческий шлюз не убрать. Выбрать пять выдающихся учёных, чтобы благословить результат, — это в такой же степени политический акт, как и эпистемический.

Ещё одно предостережение для тех, кто готов принимать турнирные таблицы за исследовательскую способность: золотые медали на олимпиадах измеряют результативность на задачах, спроектированных так, чтобы их можно было решить за часы. Исследования — противоположное распределение: задачи выбраны именно потому, что никто не знает, разрешимы ли они вообще. Та же причина, по которой бенчмарки пропускают большую часть реальной работы в разработке ПО: метрика вознаграждает выверенную задачу, а не запутанную. Модель, которая щёлкает олимпиадные задачи, продемонстрировала нечто настоящее. Но она не продемонстрировала суждения.

Рекомендация: доверяйте петле, а не модели

Вот моя позиция, сформулированная прямо. Генерация гипотез реальна, полезна и будет только лучше; непроверенная генерация гипотез ничего не стоит, а доказательства на естественном языке без формальной поддержки стоит считать маркетингом, пока не доказано обратное. Проверка доказательств побеждает всякий раз, когда артефакт должен быть признан верным. Генерация побеждает всякий раз, когда узкое место — воображение, а не строгость. Значимые анонсы — это те, где два подхода скреплены вместе.

Поэтому относитесь к модели как к плодовитому младшему коллеге с неистощимой энергией и без суждения: всё, что она вам приносит, проходит через ассистента доказательств, прежде чем попасть в статью, и через человека со вкусом, прежде чем попасть во введение. Если вы исследователь, освойте один ассистент доказательств по-настоящему: формализация — узкое место, и люди, которые умеют им управлять, скоро будут очень заняты. Если вы строите инструменты, стройте петлю, а не демо. А когда выйдет следующий громкий анонс, пропустите пресс-релиз, откройте препринт и проверьте, существует ли репозиторий на Lean. Выживают те утверждения, которые приходят уже машинно проверенными.