Исследователи объединили AlphaProof с большими языковыми моделями, чтобы находить решения сложных задач и проверять математические доказательства.
Исследователи Google DeepMind усовершенствовали систему математического искусственного интеллекта AlphaProof, научив ее эффективнее искать решения нерешенных математических задач и формировать доказательства, которые можно проверить автоматически. С помощью обновленной системы ученые решили девять открытых проблем, сформулированных венгерским математиком Палом Эрдешом. Результаты работы опубликованы в журнале Science.
Разработку возглавил научный сотрудник Google DeepMind Сварат Чадхури. За основу исследователи взяли AlphaProof — систему, способную решать сложные математические задачи на уровне участников Международной математической олимпиады. Ее особенность заключается в использовании языка Lean, который позволяет формализовать математические доказательства и проверять их корректность.
Чтобы расширить возможности AlphaProof, ученые объединили ее с большими языковыми моделями Google. Новая система анализирует условие задачи, представленное на языке Lean, и распределяет поиск решения между множеством независимых ИИ-агентов. Они предлагают различные идеи, формулируют их в виде математических конструкций и проверяют полученные результаты.
Такой подход помогает справиться с одной из главных проблем языковых моделей — склонностью к галлюцинациям и логическим ошибкам. Вместо того чтобы полагаться исключительно на способность нейросети генерировать правдоподобные рассуждения, система использует формальные методы для проверки каждого доказательства.
Источник: hi-tech.mail.ru