ИИ-агент Google DeepMind справился с 9 нерешёнными задачами Эрдёша, две из которых оставались без ответа 56 лет

Исследовательский агент AlphaProof Nexus от Google DeepMind справился с 9 из 353 открытых математических задач, которые связывают с именем венгерского математика Пала Эрдёша. Две из них оставались без решения 56 лет. Вычисления для каждой решённой задачи Эрдёша обходились системе в несколько сотен долларов. Помимо этого, агент доказал 44 из 492 открытых гипотез, собранных в Онлайн-энциклопедии целочисленных последовательностей (OEIS), где хранятся математические числовые последовательности.

Эти результаты изложены в работе о применении больших языковых моделей к поиску формальных доказательств. Авторы выясняли, годится ли такой подход не только для олимпиадных задач, но и для открытых проблем исследовательского уровня.

От обычного чат-бота систему отличает использование Lean — языка и среды для формализации математических доказательств. ИИ формулирует доказательство в формальном виде, а Lean проверяет каждый логический шаг. Если в проверке находится ошибка, агент получает обратную связь и продолжает поиск. Правдоподобно написанного объяснения здесь мало: результат обязан пройти машинную проверку по строгим логическим правилам.

В AlphaProof Nexus несколько ИИ-агентов одновременно ищут решения, оценивают разные подходы и шлифуют доказательства. В самой сложной версии системы их работой управляет эволюционный алгоритм, а на отдельных этапах поиска подключается AlphaProof — разработанная в Google DeepMind система автоматического доказательства теорем на основе обучения с подкреплением.

Отдельно исследователи сопоставили эту многосоставную архитектуру с более простым агентом, в котором генерация доказательств языковой моделью чередуется с проверкой в Lean. Когда заново разобрали девять решённых задач Эрдёша, выяснилось, что простой агент осилил все девять. Но на самых трудных задачах он обходился дороже. Отсюда следует, что итог зависит не только от возможностей самой языковой модели, но и от того, как выстроен поиск доказательства.

Применение AlphaProof Nexus не ограничивается задачами Эрдёша и гипотезами OEIS. Система помогла решить открытую задачу в алгебраической геометрии, уточнить оценку в выпуклой оптимизации и найти ошибки в формализации математических утверждений, попадавшихся в научной литературе. Кроме того, её применяют в исследованиях по теории графов и квантовой оптике.

Вместе с тем большинство открытых задач Эрдёша агенту не поддалось. Нынешние успехи приходятся на области, где уже есть развитая библиотека формализованных результатов и где сложные рассуждения можно разбить на отдельные подзадачи. Кроме того, система унаследовала ограничения языковых моделей: результаты поиска сильно колеблются от попытки к попытке, а задачи, для которых нужно создавать обширную новую теорию, пока ей не по силам.

По мнению авторов, формальные доказательства способны сделать ИИ полноценным участником математической работы, а не просто источником готовых ответов.

Источник: iXBT