Математические прорывы ИИ, о которых все говорят, — это контрпримеры, а не доказательства

Контрпример и доказательство — это не одно и то же достижение. Доказательство показывает, что что-то верно всегда. Контрпример же доказывает, что утверждение, считавшееся всегда верным, таковым не является, путем демонстрации хотя бы одного объекта, на котором оно терпит крах.

Оба варианта закрывают вопрос. Но от того, кто их ищет, они требуют разного. Первый подразумевает аргумент, охватывающий каждый случай. Второй — единственный объект и право продолжать догадки, пока вы его не получите.

Этому различию посвящена запись в блоге кембриджского математика Тимоти Гауэрса, которую он опубликовал 12 августа. Гауэрс получил Филдсовскую премию в 1998 году. К тому же он прочитал научные работы, чего не сделали большинство комментаторов, рассуждающих об ИИ и математике.

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

«Большие языковые модели хороши не только в поиске контрпримеров: они также способны находить доказательства сложных утверждений», — пишет он.

Что общего у знаменитых результатов

OpenAI объявила о <решении> десяти открытых проблем в математике и теоретической информатике. Два результата привлекли наибольшее внимание. Первым стала конструкция несофической группы. Гауэрс присутствовал на обсуждениях и называет это «одной из важнейших нерешенных проблем теории групп». Вторым стала нижняя оценка, показывающая, что многоцветное число Рамсея растет суперэкспоненциально.

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

Затем следует наблюдение, которое новостные агрегаторы обошли стороной. Самые известные достижения больших языковых моделей, отмечает Гауэрс, почти всегда представляли собой контрпримеры, а не доказательства. Он перечисляет два вышеупомянутых, а также гипотезу Иакоби и гипотезу единичного расстояния. Третий пункт его выводов сформулирован очень аккуратно. Модели прекрасно справляются с доказательством универсальных утверждений. Однако самые весомые вещи, которые они доказали, не идут ни в какое сравнение с самыми весомыми вещами, которые они опровергли.

Два результата, которые он переквалифицирует

Контрпример оправдывает свое название, если он разрушает то, во что у людей были веские основания верить. Исходя из этого критерия, Гауэрс переквалифицирует два главных результата, причем один из них идет вразрез с официальной документацией авторов.

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

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

Почему примеры подходят машинам

Гауэрс перечислят восемь способов, с помощью которых математики ищут примеры. Попробовать стандартные готовые примеры. Построить его из знакомых элементов. Оставить части неопределенными и заполнять их по мере необходимости в ходе доказательства. Попробовать доказать противоположное и посмотреть, что сломается. Угадать, потерпеть неудачу, провести диагностику, угадать снова. Построить объект шаг за шагом. Выбрать один случайный. Выбрать типичный.

Четыре из этих методов задействуют то, чем машина уже обладает: обширные знания и способность выполнять огромное количество попыток. Готовые проверки, пошаговое построение, вероятностные аргументы и типичные примеры вознаграждают объем вычислений. Три других подхода требуют чего-то иного. Оставление частей неопределенными, попытки доказать противоположное и метод последовательных приближений — всё это требует суждения о том, стоит ли продолжать текущий подход.

Именно здесь Гауэрс видит пробел, и дело вовсе не в чистой вычислительной мощности. Он называет это «чутьем» — способностью понимать, когда вы приближаетесь к цели, а когда пора бросить бесперспективную ветку. Именно это позволяет человеку отсекать ветви дерева поиска, которые никакой компьютер не смог бы исчерпать полностью.

Пять редукций и никакого прогресса

Свои доводы относительно этого пробела он частично подтверждает личным опытом, о чем и заявляет. Работая с GPT-5.6 Pro над нерешенными задачами, он часто получает подходы, которые выглядят многообещающе, но не выдерживают проверки. Он также описывает узнаваемый паттерн поведения.

Модель сообщает, что не ответила на вопрос, но свела его к более узкой и точной задаче, «что звучит весьма обнадеживающе, пока это не повторяется пять раз подряд без какого-либо видимого прогресса».

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

Его объяснение того, почему такое «чутье» у ИИ может не сформироваться само по себе, — пожалуй, самое интересное в этой публикации. Опубликованная математика скрывает процесс поиска. Модели видят, по его словам, «причесанные доказательства, в которых скрыт ход мысли их первооткрывателей».

Тупиковые ветви никогда не попадают в научную литературу. Поэтому обучающие данные практически не содержат информации о том, какие направления были отброшены и почему. Он добавляет вторую причину. У системы, способной перебрать всё с огромной скоростью, мало стимулов учиться хоть какому-то отсесечению лишнего.

Тест, который он готов принять

Гауэрс предлагает проверяемый на практике критерий, что уже больше, чем могут предложить большинство комментаторов. Он признает победу ИИ, когда модель выдаст доказательство столь же удивительное, как решение задачи о cap-set (множествах без арифметических прогрессий) 2016 года, когда старые границы были стерты, а метод не был похож ни на что из того, что он сам рассматривал.

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

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

Именно поэтому пересказы его поста заслуживают внимания.

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

За последние три недели его уже дважды записали в скептики.

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

У теста с cap-set нет дедлайна, в чем и заключается вся суть. Рано или поздно кто-то опубликует доказательство. После этого начнется дискуссия о том, не лежал ли этот метод все это время в обучающей выборке.