Формально или неформально? Вот в чём вопрос для ИИ в области доказательства теорем

Оригинал: https://xenaproject.wordpress.com/2025/10/22/formal-or-not-formal-that-is-the-question-in-ai-for-theorem-proving/

Итак, сейчас интересное время для того, чтобы «компьютеры занимались математикой». За последние несколько дней произошло несколько любопытных событий, которые вдохновили меня написать об этом вопросе в более общем ключе.

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

Но независимо от того, обгонят ли они нас или просто будут нам помогать, всё равно можно спросить, как вообще будет выглядеть автономный инструмент для доказательства теорем. Давайте для начала сделаем гигантский шаг вниз от исследовательской математики и поговорим вместо этого о задачах, которые могут решать толковые школьники, а именно о задачах Международной математической олимпиады (IMO). Я недавно писал о попытках ИИ на IMO 2025, но всё, что вам нужно знать здесь, — это что было четыре публично известных попытки: две из них использовали языковые модели для написания доказательств на английском (которые затем проверялись людьми); давайте называть это «неформальным подходом». Две другие использовали гибридную связку «языковая модель + Lean»; назовём это «формальным подходом». Lean — это компьютерный проверщик доказательств, или интерактивный доказатель теорем; он проверяет математические аргументы на сверхчеловеческом уровне. В такой гибридной схеме языковая модель пишет доказательства на языке Lean, а затем Lean автоматически их проверяет; как только Lean говорит, что доказательства корректны, людям остаётся только проверить, что сами формулировки теорем были правильно переведены на язык Lean, хотя это важная часть процесса.

Опасения по поводу неформального подхода

Больше всего в неформальном подходе меня волнуют истории ужасов, которые я слышу от редакторов журналов. Математические журналы заваливают статьи, сгенерированные LLM, которые выглядят всё более и более правдоподобно, и иногда использование LLM даже не раскрывается в тексте. Я хочу подчеркнуть некоторые различия между математическими статьями, написанными LLM, и написанными людьми:

LLM — подхалимы. Вы хотите услышать, что аргумент, сгенерированный LLM, действительно доказывает теорему? Конечно хотите — и именно поэтому LLM заверит вас, что это так, даже если в аргументе есть галлюцинация (и помните: одной галлюцинации достаточно, чтобы сломать математическое рассуждение). По моему опыту, математические исследователи, работающие традиционными методами, практически никогда не отправят в журнал статью, утверждая, что они что‑то доказали, если сами считают, что на самом деле этого не сделали. «Застрять» — это нормальное состояние для математика‑исследователя. LLM же куда более склонна писать правдоподобный мусор, чтобы скрыть свои следы; в каком‑то смысле её обучают вводить в заблуждение. Поэтому к статье, сгенерированной LLM, нужно относиться с заметно большей подозрительностью, чем к статье, написанной человеком.
LLM не говорят «я не знаю». Мы ожидаем, что они будут очень хорошо работать «на распределении», то есть на данных, похожих на те, на которых они обучались (а это, несомненно, включает все техники, нужные для решения задач IMO). Но что происходит «вне распределения» — скажем, с теоремами, доказательств которых никто из людей не знает? Правильный ответ на множество промежуточных вопросов, возникающих в процессе исследования, — «я не знаю — да и вообще никто не знает». В то время как ответ LLM будет: «Я уверенно попробую». Помните: одна галлюцинация ломает аргумент.

Вкратце: я пока не доверяю математическим текстам, написанным LLM. Несколько математиков, с которыми я беседовал, поддержали меня в этом: они пробовали вводить сложные исследовательские задачи в языковые модели и получали бессмысленный вывод, насквозь видимый для специалиста. Станут ли LLM когда‑нибудь на 100 % надёжными вне обучающего распределения (то есть при попытке делать оригинальные исследования)? Этого сейчас никто не знает, и всякий, кто утверждает обратное, либо просто гадает, либо подогревает хайп. Позорная история последних дней про OpenAI и десять задач Эрдёша — показательный пример. Люди, похоже, очень быстро готовы поверить, что «всё уже произошло»; в действительности сейчас ничего близко подобного не происходит.

Одна из вещей, которые становятся популярными в рамках неформального подхода, — это тестировать системы на задачах, где ответ — не длинное доказательство (на самом деле большинство настоящих прорывов в математике сопровождаются 30‑страничными доказательствами или даже более длинными), а вместо этого — на сложных задачах, где ответом является число. Примером такого подхода служит набор данных Frontier Math Tier 4 от Epoch AI. На этой неделе меня позабавило, что мне прислали данные о том, что происходит, если попросить множество агентов решать эти задачи и считать задачу решённой, если хотя бы один агент хотя бы раз дал правильный ответ. Я хотел бы предложить свой собственный, основанный на ИИ, подход к набору Tier 4, раз уж теперь такая система оценивания: он написан на Python.

i = 0
while True:
    print(i)
    i = i + 1

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

Опасения по поводу формального подхода

Удивительная история про задачу Эрдёша № 707, появившаяся сегодня утром (коротко: два исследователя нашли решение одной задачи Эрдёша и «по вайбу» закодировали всё доказательство в Lean с помощью ChatGPT‑5, хотя сами не имели ни малейшего представления о том, как писать код на Lean; вот статья Алексеева и Миксона, где и Lean, и ChatGPT указаны как соавторы), может заставить людей думать, что Lean теперь становится действительно пригодным для математики исследовательского уровня. И, безусловно, эта история показывает, что его уже можно использовать для некоторой исследовательской математики. Но для всей? Не так быстро.

Мои опасения по поводу формального подхода связаны с тем, что даже лучшие на сегодняшний день библиотеки формальной математики не содержат тех определений, которые нужны, чтобы понимать большую часть того, что происходит в современной исследовательской математике. Благодаря гранту Renaissance Philanthropy AI for Math я просматривал свежие выпуски Annals и пытался выяснить, какие определения нужно формализовать, чтобы мы могли хотя бы формально сформулировать основные результаты в этих статьях. Примеры того, что я там видел: группы Тейта–Шафаревича, многообразия Калаби–Яу, алгебраические стеки, автоморфные представления, этальные когомологии с компактным носителем, якобианы, формы Мааса. Это повседневные объекты, с которыми работают аспиранты на математических факультетах по всему миру; ни один существующий доказатель теорем не знает, что это за объекты. Если Lean и остальные системы не могут даже понять формулировки большинства современных теорем исследовательского уровня, как они вообще могут помочь математикам их доказывать?

Чья это задача — всё исправить?

Как, наверное, уже ясно, я сейчас скептически отношусь к тому, что система предсказания следующего токена когда‑нибудь дойдёт до состояния, в котором она сможет быть на 100 % точной при генерации 50 и более страниц текста «вне обучающего распределения» (а именно такого порядка сложности обычно требуют новые прорывы в исследовательской математике). Гибрид LLM/Lean выглядит для меня куда более правдоподобным (и мы только что видели, насколько хорошо он сработал в истории с задачей Эрдёша 707 — хотя именно люди в этом случае придумывали идеи, а не машины). Обучение Lean множеству современных определений, как мне кажется, является узким местом; это, безусловно, не нерешимая проблема, но она потребует времени, и её решение, на мой взгляд, — фундаментальная задача. Но кто вообще находится в положении, чтобы решать эту проблему? Давайте посмотрим на некоторых вероятных кандидатов.

Математик‑исследователь. Это те люди, которые до сих пор обучили Lean практически всем нетривиальным математическим определениям в его библиотеке mathlib. Например, я научил mathlib тому, что такое эллиптические кривые, а Крис Биркбек — тому, что такое модулярные формы, так что мы теперь можем формулировать гипотезу Шимуры–Таниямы–Вейля, связывающую эллиптические кривые с модулярными формами; именно эта гипотеза была частично доказана Уайлсом и Тейлором–Уайлсом и влекла за собой Великую теорему Ферма. Большая проблема масштабирования этот подхода в том, что математик‑исследователь живёт в среде «публикуйся или пропадёшь», и работа такого рода не вписывается в традиционную модель публикаций: текущая система поощряет новые доказательства, а не формализацию уже известных результатов, даже если их раньше никогда не формализовали.
LLM. Этот подход продвигает Кристиан Сегеди и его коллеги из math.inc. Моё опасение здесь в том, что прямо сейчас LLM генерируют очень неидиоматичный и слабый код, и плохие определения в перспективе могут вылиться в огромный технический долг, когда система начнёт масштабироваться. Ещё одно опасение, связанное с определениями, сгенерированными LLM, состоит в том, что, в отличие от доказательств, Lean не может проверить, совпадает ли данное определение с человеческой концепцией, которую оно должно описывать; если LLM забудет или исказит какую‑то аксиому, входящую в определение, то код, скорее всего, по‑прежнему скомпилируется, он просто не будет означать то, что должен означать.
Mathlib Initiative. Это новая организация, целью которой является поддержка математической библиотеки Lean. У них уже и так много задач, что видно из их дорожной карты, но проблема, о которой я говорю — научить Lean понимать современные определения, — прямо там не упоминается. Возможно, простое решение заключалось бы в том, чтобы расширить их деятельность и в эту сторону, но это, конечно, потребует появления дополнительного финансирования откуда‑то.

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

О проекте

Xena — проект по формализации математики в Lean, который помогает математикам, особенно студентам, переводить обычные теоремы и задачи в формальные доказательства, проверяемые компьютером. Его цель — сделать доказательные помощники удобным рабочим инструментом для обучения и исследований, а не только узкоспециализированной системой.imperial+1

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