В минувшие выходные Нил Сомани, инженер-программист, бывший количественный исследователь и основатель стартапа, тестировал математические возможности новой модели OpenAI и сделал неожиданное открытие. После того, как он вставил задачу в ChatGPT и дал ей подумать 15 минут, он вернулся к полному решению. Он оценил доказательство и формализовал его с помощью инструмента Harmonic — и всё оказалось в порядке.
«Мне было любопытно установить базовый уровень, когда студенты магистратуры в области права эффективно решают открытые математические задачи, и определить, в каких областях они испытывают трудности», — сказал Сомани. Неожиданным оказалось то, что, используя новейшую модель, границы прогресса начали немного расширяться.
Логическая цепочка рассуждений ChatGPT еще более впечатляет, в ней быстро перечисляются математические аксиомы, такие как формула Лежандра, постулат Бертрана и теорема о звезде Давида. В конце концов, модель нашла сообщение на Math Overflow от 2013 года, где математик из Гарварда Ноам Элкис предложил элегантное решение аналогичной проблемы. Но окончательное доказательство ChatGPT существенно отличалось от работы Элкиса и давало более полное решение версии проблемы, поставленной легендарным математиком Полем Эрдошем, чья обширная коллекция нерешенных задач стала полигоном для ИИ.
Для тех, кто скептически относится к машинному интеллекту, это удивительный результат — и не единственный. Инструменты ИИ стали повсеместными в математике, от ориентированных на формализацию моделей лингвистического анализа, таких как Aristotle от Harmonic, до инструментов обзора литературы, таких как Deep Research от OpenAI. Но после выпуска GPT 5.2 — которую Сомани описывает как «по неофициальным данным, более совершенную в математическом мышлении, чем предыдущие версии» — огромный объем решенных задач стало трудно игнорировать, что поднимает новые вопросы о способности больших языковых моделей расширять границы человеческих знаний.
Сомани изучал проблемы Эрдоша — набор из более чем 1000 гипотез венгерского математика, которые поддерживаются в режиме онлайн. Эти проблемы стали заманчивой целью для математических вычислений с использованием ИИ, поскольку они значительно различаются как по тематике, так и по сложности. Первая партия автономных решений появилась в ноябре от модели AlphaEvolve, работающей на базе Gemini, — но совсем недавно Сомани и другие обнаружили, что GPT 5.2 удивительно хорошо справляется с математикой высокого уровня.
С Рождества 15 задач на сайте Erdős были переведены из категории «открытые» в категорию «решенные», и в 11 из решений конкретно указано участие моделей искусственного интеллекта в этом процессе.
Известный математик Теренс Тао на своей странице в GitHub более подробно рассматривает достигнутый прогресс, перечисляя восемь различных задач, в решении которых модели ИИ добились значительного автономного прогресса в задаче Эрдоша, а также шесть других случаев, когда прогресс был достигнут за счет поиска и развития предыдущих исследований. До того, чтобы системы ИИ могли выполнять математические вычисления без вмешательства человека, еще далеко, но ясно, что большие модели играют важную роль.
В своей работе о Mastodon Тао предположил, что масштабируемость систем искусственного интеллекта делает их «более подходящими для систематического применения к „длинному хвосту“ малоизвестных проблем Эрдоша, многие из которых на самом деле имеют простые решения».
«Таким образом, многие из этих более простых проблем Эрдоша теперь с большей вероятностью могут быть решены исключительно с помощью методов, основанных на искусственном интеллекте, чем с помощью человеческих или гибридных средств», — продолжил Тао.
Еще одной движущей силой является недавний сдвиг в сторону формализации — трудоемкой задачи, которая упрощает проверку и расширение математических рассуждений. Формализация не требует использования ИИ или даже компьютеров, но новый набор автоматизированных инструментов значительно упростил этот процесс. Открытый программный «помощник по доказательствам» Lean, разработанный в Microsoft Research в 2013 году, получил широкое распространение в этой области как способ формализации доказательств, а такие инструменты ИИ, как Aristotle от Harmonic, обещают автоматизировать большую часть работы по формализации.
Для основателя Harmonic Тудора Ахима внезапный скачок в количестве решенных задач Эрдоша менее важен, чем тот факт, что величайшие математики мира начинают серьезно относиться к этим инструментам. «Меня больше волнует тот факт, что профессора математики и информатики используют [инструменты ИИ]», — сказал Ахим. «Эти люди должны защищать свою репутацию, поэтому, когда они говорят, что используют Aristotle или ChatGPT, это реальное доказательство».
Источник: techcrunch.com
