Йозеф Урбан из лаборатории AI4REASON опубликовал препринт о проекте, который заставляет задуматься о том, куда движется математика. Но чтобы оценить масштаб происходящего, стоит сначала поговорить об истории.
Долгая дорога к автоформализации
Идея проверки математических доказательств компьютером стара почти как сами компьютеры. Ещё в 1962 году Джон Маккарти писал, что это “потенциально одно из самых интересных и полезных применений вычислительных машин”. В 1963 году Пол Абрахамс защитил диссертацию о машинной верификации доказательств в MIT, и тут же честно признал, что проверка настоящего доказательства из учебника потребует “гораздо большего”.
Фактически первой реально запрограммированной системой искусственного интеллекта был Logic Theorist от Аллена Ньюэлла и Герберта Саймона (1956), о котором я всё время рассказываю на лекциях (в третьей лекции здесь, например) и в докладах о математике (например).
С тех пор появилось много систем для автоматического доказательства и верификации: Mizar в 70-х, Isabelle/Isar в 2000-х, а сейчас самый популярный прувер — Lean, появившийся в 2013 году. Но все они требовали, чтобы человек вручную переводил математику на формальный язык. Это кропотливая работа, ведь формальное доказательство может быть в десятки, а то и сотни раз длиннее оригинала, и любой переход вроде “очевидно, что”, действительно очевидный человеку, может внезапно оказаться большой проблемой.
Роль личности: кто такой Урбан
Йозеф Урбан — один из пионеров идеи автоматической формализации с помощью машинного обучения. В 2004 году он написал письмо одному из авторов “Compendium of Continuous Lattices” с предложением использовать автоматические пруверы как “семантический фильтр” для парсеров естественного языка. Тогда это казалось безумием.
В 2014 году на конференции CICM Урбан (по его словам, именно тогда он ввёл сам термин auto-formalization в этом контексте) представил программу исследований: накопить корпусы параллельных текстов (неформальная математика + формальные доказательства), обучить на них статистические модели перевода, а затем соединить это с автоматическими доказателями для семантической проверки.
Тогда же он сделал несколько публичных ставок. Одна из них: через 25 лет 50% утверждений из учебников уровня магистратуры будут автоматически парситься с корректной формальной семантикой. Урбан тогда осторожно добавил: “возможно, это произойдёт быстрее, чем я ожидал”.
Прошло чуть больше десяти лет, и похоже, что он был прав насчёт “быстрее”.
Что такое формализация и что сделал Урбан
Обычные математические доказательства — это текст на естественном языке, который читают и проверяют другие математики. Но люди ошибаются, и история знает случаи, когда “доказанные” теоремы оказывались неверными спустя годы. Формализация — это перевод доказательств на строгий машиночитаемый язык, где каждый шаг проверяется компьютером. Если программа-верификатор приняла доказательство — оно гарантированно корректно.
В препринте Урбан запустил простой цикл: большая языковая модель (в основном ChatGPT 5.2, но Claude через Claude Code он тоже пробовал) пишет формальные доказательства, верификатор их проверяет, модель получает обратную связь и исправляет ошибки. И так по кругу — почти без участия человека.
За две недели система произвела около 130 тысяч строк формализованной топологии по учебнику Манкреса. Полностью доказаны серьёзные теоремы: лемма Урысона (3 тысячи строк), теорема метризации Урысона (2 тысячи строк), теорема Титце о продолжении (более 10 тысяч строк).
Последняя, кстати, потребовала от системы самостоятельно восполнить пробел в учебнике — там использовались факты о полных метрических пространствах, которые в книге вводятся только через 8 глав. GPT думал долго, но в итоге справился.
Что здесь удивительного?
Во-первых, стоимость. Весь проект обошёлся примерно в $100 на подписки на LLM.
Во-вторых, система доказательств. Урбан использовал не какой-нибудь Lean, с которым LLM работают давно, а Megalodon — разработанный той же группой AI4REASON малоизвестный верификатор на основе теории множеств высшего порядка, на котором современные LLM почти не обучались. И это совершенно ничему не помешало, GPT и Claude прекрасно справлялись и с Megalodon. В своё время Урбан экспериментировал с вероятностными контекстно-свободными грамматиками именно потому, что не хотел полагаться на “чёрные ящики”. Теперь оказалось, что чёрные ящики работают даже там, где их специально не учили.
В-третьих, степень автономности. Один и тот же промпт подавался системе примерно 1000-2000 раз, и она сама решала, что делать дальше. Вот очень милая цитата из работы Урбана про его workflow:
Before December 22, I was “babysitting” the command-line interface, i.e., looking every now and then if the agent has finished its work and waits for another prompt. This was manageable, because my early $20/month LLM subscriptions would quickly run out of credits anyway and most of the time would be spent waiting for the weekly credit limit to be reset. With the $200/month ChatGPT Pro subscription the limits on usage got much higher and automating the prompting became necessary. I have implemented it by writing the following script that watches the tmux session and feeds it the prompt followed by “Enter” whenever there has not been any change in the session for 60 seconds
Куда всё это катится?
В своём докладе 2024 года Урбан цитировал манифест QED 1994 года, где сетовали, что “многие, кто мог бы внести вклад в проект QED, отвлеклись на соблазнительную приманку AI”. Тридцать лет спустя AI, похоже, возвращается к проекту QED, но уже в роли главной движущей силы, а не отвлекающего фактора.
Урбан осторожно предполагает, что в 2026 году мы можем увидеть автоформализацию большинства стандартных учебников. Или не увидеть — возможно, система упрётся в какие-то пределы. Но сам факт, что это теперь “дёшево и доступно каждому”, меняет многое.
Будущее, как водится, предсказать трудно, но опять кажется, что движемся мы туда значительно быстрее, чем ожидали.
Сергей Николенко
P.S. Прокомментировать и обсудить пост можно в канале «Sineкура»: присоединяйтесь!
Leave a Reply