ИИ доказал девять открытых математических задач Эрдеша
9 октября. ПРАВМИР. Система искусственного интеллекта Google DeepMind смогла доказать девять открытых математических задач из списка математика Пала Эрдеша. Две из них оставались нерешенными 56 лет.
Исследование опубликовано в журнале Science. Всего ученые предложили системе 353 открытые задачи Эрдеша. С девятью она справилась.
Главная особенность эксперимента в том, что система не просто выдавала текст, похожий на математическое доказательство. Каждый логический шаг проверялся автоматически, поэтому незаметно пропустить ошибку или придумать несуществующее обоснование было значительно сложнее.
Система получила название AlphaProof Nexus. Ее разработали исследователи Google DeepMind вместе с коллегами из других научных организаций.
Одна из главных проблем современных языковых моделей в математике хорошо известна: они способны построить убедительное рассуждение, внутри которого окажется небольшая логическая ошибка.
В обычном тексте такую ошибку порой трудно заметить даже специалисту.
Разработчики AlphaProof Nexus выбрали другой подход. Математические задачи и доказательства записывались на формальном языке Lean.
Это система, в которой компьютер может проверить каждый этап рассуждения. Если одно утверждение не следует из предыдущих или для него не хватает доказательства, программа его не принимает.
ИИ предлагал очередной вариант решения, Lean проверял его и сообщал об ошибках. После этого система могла искать другой путь.
Таким образом, итогом становился не просто ответ нейросети, а формальное доказательство, которое можно проверить независимо.
Для одного из главных экспериментов ученые взяли задачи Пала Эрдеша.
Венгерский математик, умерший в 1996 году, был одним из самых известных исследователей XX века. Он работал в теории чисел, комбинаторике и других областях и оставил после себя сотни задач, многие из которых оказались чрезвычайно сложными.
Часть из них математики решали десятилетиями, а некоторые остаются открытыми до сих пор.
В эксперименте успех составил девять задач из 353, то есть всего около 2,5%.
Авторы и сами отмечают, что значительная часть исследовательской математики пока остается для таких систем недоступной.