Нейросеть Google DeepMind доказала девять открытых задач Эрдёша

Система искусственного интеллекта AlphaProof Nexus, созданная исследователями Google DeepMind, нашла и формально доказала решения девяти открытых математических задач из каталога венгерского математика Пала Эрдёша. Всего алгоритм проверил 353 задачи из этого списка, сообщает «Мел». Результаты опубликованы на портале EurekAlert!.

Какие задачи решил ИИ

Помимо задач Эрдёша, система доказала 44 из 492 открытых гипотез, связанных с Онлайн-энциклопедией целочисленных последовательностей. Две из девяти задач Эрдёша не поддавались математикам более 50 лет, однако возраст остальных был меньше, и говорить, что все они ждали решения десятилетиями, неверно.

Как устроена проверка доказательств

AlphaProof Nexus построена на основе прежних математических инструментов Google DeepMind, в том числе AlphaProof, которая в 2024 году вместе с AlphaGeometry 2 решила четыре из шести задач Международной математической олимпиады. В новой системе большие языковые модели объединены с инструментами формального доказательства: сначала ИИ анализирует условие, записанное на языке Lean, затем ищет решение. Lean автоматически проверяет каждый логический шаг; если в рассуждении есть пробел или ошибка, проверка не проходит. Это важно, поскольку нейросети иногда выдают правдоподобные, но неверные доказательства. По данным эксперимента, даже более простая схема, где модель предлагает доказательство, а Lean проверяет его и возвращает замечания, справилась с теми же девятью задачами.

Где ещё может применяться метод

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