AlphaProof Nexus от Google Deepmind решает математические задачи, над которыми учёные бились десятилетиями, за несколько сотен долларов
Новый фреймворк Google Deepmind AlphaProof Nexus автономно решил 9 из 353 открытых проблем Эрдёша, включая две задачи, остававшиеся нерешёнными 56 лет. Система также доказала 44 из 492 гипотез из онлайн-энциклопедии целочисленных последовательностей (OEIS) и закрыла 15-летний вопрос о функциях Гильберта в алгебраической геометрии. Стоимость вычислений составила всего несколько сотен долларов за задачу.
В отличие от чистых LLM-подходов, AlphaProof Nexus использует Gemini 3.1 Pro для генерации шагов доказательства на формальном языке Lean, а компилятор проверяет каждый шаг. Сообщения об ошибках напрямую подаются обратно в модель для следующей попытки. Это позволяет избежать типичных для языковых моделей проблем с логическими рассуждениями. Человек вмешивается только на финальной проверке результатов.
Система включает четыре варианта агентов: от простейшего (A), работающего в цикле «LLM → компилятор», до полного (D), объединяющего эволюционный компонент и запросы к AlphaProof. Удивительно, но простейший агент (A) также смог решить все девять задач Эрдёша, хотя на самых сложных это обошлось дороже. Исследователи отмечают, что это указывает на общий тренд: по мере улучшения LLM специализированные обученные системы уступают место простым агентным циклам.
Система уже применяется в исследованиях по квантовой оптике и теории графов. Все доказательства на Lean доступны на GitHub.
#Ai #Google #Tech #Deepmind #AlphaProof #FrameWork
Новый фреймворк Google Deepmind AlphaProof Nexus автономно решил 9 из 353 открытых проблем Эрдёша, включая две задачи, остававшиеся нерешёнными 56 лет. Система также доказала 44 из 492 гипотез из онлайн-энциклопедии целочисленных последовательностей (OEIS) и закрыла 15-летний вопрос о функциях Гильберта в алгебраической геометрии. Стоимость вычислений составила всего несколько сотен долларов за задачу.
В отличие от чистых LLM-подходов, AlphaProof Nexus использует Gemini 3.1 Pro для генерации шагов доказательства на формальном языке Lean, а компилятор проверяет каждый шаг. Сообщения об ошибках напрямую подаются обратно в модель для следующей попытки. Это позволяет избежать типичных для языковых моделей проблем с логическими рассуждениями. Человек вмешивается только на финальной проверке результатов.
Система включает четыре варианта агентов: от простейшего (A), работающего в цикле «LLM → компилятор», до полного (D), объединяющего эволюционный компонент и запросы к AlphaProof. Удивительно, но простейший агент (A) также смог решить все девять задач Эрдёша, хотя на самых сложных это обошлось дороже. Исследователи отмечают, что это указывает на общий тренд: по мере улучшения LLM специализированные обученные системы уступают место простым агентным циклам.
Система уже применяется в исследованиях по квантовой оптике и теории графов. Все доказательства на Lean доступны на GitHub.
#Ai #Google #Tech #Deepmind #AlphaProof #FrameWork
🔥1
Новое исследование Google DeepMind, опубликованное в Science, описывает систему AlphaProof Nexus, которая самостоятельно справилась с рядом нерешённых математических проблем. Она закрыла 9 из 353 открытых задач Эрдёша - две из них оставались нерешёнными 56 лет. Решения были выложены в открытый доступ ещё до выхода статьи.
В основе системы - Gemini 3.1 Pro, который пишет и правит доказательства на формальном языке Lean. Lean проверяет каждый черновик после правки, а сообщения об ошибках задают направление следующей попытки. Для сложных подзадач система может обращаться к специализированному инструменту AlphaProof, хотя, по данным DeepMind, 9 задач Эрдёша были решены и без него. Помимо этого AlphaProof Nexus доказал 44 гипотезы из базы целочисленных последовательностей OEIS, закрыл открытый вопрос в алгебраической геометрии и улучшил известную границу в min-max оптимизации - методе, применяемом при обучении некоторых ИИ-моделей.
Работа вышла на фоне спора о роли ИИ в математике: OpenAI ранее выложила сотни ИИ-доказательств на GitHub вместо отправки в журналы, а Ассоциация человеческой математики во главе с Теренсом Тао призывала к бойкоту. DeepMind, в отличие от этого, провёл свои результаты через рецензирование.
🎨 qvabo.studio/tg · картинки и видео
#AI #GoogleDeepMind #AlphaProof #Mathematics #Lean
Please open Telegram to view this post
VIEW IN TELEGRAM
🎉1👨💻1