Недавно инженер-программист и основатель стартапа Нил Сомани провел эксперимент по тестированию математических возможностей новой модели OpenAI. Он ввел сложную задачу в ChatGPT, оставив ее на 15 минут, и получил полноценное решение. Сомани проверил и формализовал доказательство с помощью инструмента Harmonic — результат оказался верным.
Об этом сообщает ProIT
AI модели уже решают задачи из списка Эрдеша
“Мне было интересно установить базовый уровень, когда LLMs эффективно способны решать открытые математические задачи по сравнению с тем, где они испытывают трудности,” сказал Сомани. Удивительно, что, используя последнюю модель, граница начала немного сдвигаться вперед.
Особенно впечатляет ход мыслей ChatGPT, который оперировал такими математическими аксиомами, как формула Лежандра, постулат Бертрана и теорема Звезды Давида. Модель также нашла публикацию на Math Overflow за 2013 год, где математик из Гарварда Ноам Элкис предложил элегантное решение подобной задачи. Однако конечное доказательство от ChatGPT существенно отличалось от подхода Элкиса и содержало более полное решение версии задачи, поставленной легендарным mathematician Паулем Эрдешем. Коллекция его нерешенных задач давно стала полигоном для испытаний интеллектуальных систем.
Распространение инструментов искусственного интеллекта в математике уже стало повседневностью: от специализированных LLM, ориентированных на формализацию доказательств, таких как Aristotle от Harmonic, до инструментов для анализа научной литературы. Однако с появлением GPT 5.2, которую Сомани характеризует как «существенно более сильную в математических рассуждениях, чем предыдущие версии», объемы решенных задач стали невозможными для игнорирования — это открывает новые вопросы о роли больших языковых моделей в продвижении человеческих знаний.
Формализация и авторитет математиков меняют подходы
Сомани исследовал задачи Эрдеша — более тысячи гипотез венгерского математика, которые доступны онлайн. Они существенно различаются по тематике и сложности, что делает их привлекательной целью для систем с искусственным интеллектом. Первые автономные решения появились еще в ноябре от модели AlphaEvolve на базе Gemini, но сейчас GPT 5.2 демонстрирует выдающиеся результаты в сложной математике.
С Рождества на сайте задач Эрдеша 15 задач переместили в категорию «решенных», и в 11 случаях решающую роль сыграли именно AI-модели. Известный математик Терренс Тао ведет собственную статистику на GitHub: он насчитал восемь задач, в которых AI самостоятельно сделал значительный шаг вперед, и еще в шести случаях — развил идеи на основе предыдущих исследований. Хотя полной автономии еще не достигнуто, роль больших языковых моделей в математике становится все более важной.
На Mastodon Тао предположил, что масштабируемость AI-систем позволяет им эффективно работать над многочисленными малоизвестными задачами Эрдеша, многие из которых имеют относительно простые решения. По его мнению, такие задачи теперь с большей вероятностью будут решены именно автоматизированными методами, а не людьми или гибридными командами.
Еще одной движущей силой является новый акцент на формализации, которая позволяет легче проверять и расширять математические доказательства. Хотя эта работа не всегда связана с AI, новые автоматизированные инструменты значительно упростили процесс. Среди них — открытый «ассистент доказательств» Lean, созданный в Microsoft Research в 2013 году, и Aristotle от Harmonic, который обещает автоматизировать значительную часть рутинной формализации.
Тудор Ахим, основатель Harmonic, считает, что резкий рост количества решенных задач Эрдеша менее важен, чем тот факт, что ведущие математики мира все чаще применяют AI-инструменты в своей работе. “Меня больше волнует тот факт, что профессора математики и информатики используют [AI инструменты],” сказал Ахим. “Эти люди имеют репутацию, которую нужно защищать, так что когда они говорят, что используют Aristotle или ChatGPT, это реальные доказательства.”