Агент Google DeepMind решил 9 открытых математических задач Эрдёша — 2 из них не могли решить 56 лет
iXBT.com ·
Исследовательский агент AlphaProof Nexus, разработанный Google DeepMind, решил 9 из 353 открытых математических задач, связанных с именем венгерского математика Пала Эрдёша. Две из них оставались нерешёнными 56 лет. На каждую решённую задачу Эрдёша система тратила на вычисления несколько сотен долларов. Кроме того, агент доказал 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS), содержащей математические последовательности чисел.
Результаты представлены в исследовании, посвящённом применению больших языковых моделей для поиска формальных доказательств. Его авторы проверили, насколько такой подход пригоден не только для олимпиадных задач, но и для открытых математических проблем исследовательского уровня.
Ключевое отличие системы от обычного чат-бота — использование Lean, языка и среды для формализации математических доказательств. ИИ предлагает доказательство в формальном виде, после чего Lean проверяет каждый логический шаг. Если проверка обнаруживает ошибку, то агент получает обратную связь и продолжает поиск. Убедительно написанного объяснения недостаточно: результат должен пройти машинную проверку по строгим логическим правилам.
В AlphaProof Nexus несколько ИИ-агентов параллельно ищут решения, проверяют подходы и уточняют доказательства. В наиболее сложной версии системы их работу координирует эволюционный алгоритм, а для отдельных этапов поиска используется AlphaProof — разработанная Google DeepMind система автоматического доказательства теорем, основанная на обучении с подкреплением.
Авторы отдельно сравнили эту сложную архитектуру с более простым агентом, который чередует генерацию доказательств языковой моделью и проверку в Lean. При повторном анализе девяти решённых задач Эрдёша простой агент тоже справился со всеми девятью. Однако на наиболее трудных задачах его использование обходилось дороже. Это указывает на то, что результат зависит не только от возможностей самой языковой модели, но и от организации поиска доказательства.
Возможности AlphaProof Nexus не ограничиваются задачами Эрдёша и гипотезами OEIS. Система помогла решить открытую задачу в алгебраической геометрии, улучшить оценку в выпуклой оптимизации и обнаружить ошибки в формализации математических утверждений, встречавшихся в научной литературе. Её также используют в исследованиях по теории графов и квантовой оптике.
При этом большинство открытых задач Эрдёша агент решить не смог, а нынешние успехи сосредоточены в областях, для которых уже существует развитая библиотека формализованных математических результатов и сложные рассуждения удаётся разбить на отдельные подзадачи. Система также наследует ограничения языковых моделей: результаты поиска могут сильно различаться от попытки к попытке, а задачи, требующие разработки обширной новой теории, остаются за пределами её возможностей.
Авторы считают, что формальные доказательства могут стать способом включить ИИ в настоящую математическую работу, а не просто получать от него ответы.