ИИ за несколько дней решил задачу, над которой математики бились больше 10 лет
Китайский искусственный интеллект самостоятельно решил открытую проблему, предложенную более десяти лет назад американским математиком, сообщает команда разработчиков из Пекинского университета.
Гипотезу о свойствах квазиполных нетеровых локальных колец (абстактных алгебраических структур) сформулировал ныне покойный бывший профессор Университета Айовы Дэн Андерсон в 2014 году. С тех пор доказать ее не могли.
Исследователи объединили в одну систему двух агентов ИИ. Один выполняет рассуждения на естественном языке, другой занимается формальной машинной верификацией.
«Используя этот фреймворк, мы успешно решили открытую проблему в коммутативной алгебре и автоматически оформили доказательство практически без вмешательства человека, — пишут они. — Эта работа служит конкретным примером, что математические исследования можно существенно автоматизировать с помощью ИИ».
Математики все чаще обращаются к большим языковым моделям (LLM) за помощью в своих изысканиях, и надо сказать, ИИ достиг впечатляющих успехов в этой области знаний. Но склонность к галлюцинациям мешает получать надежные результаты.
Однако выполнение искусственным интеллектом задач исследовательского уровня по-прежнему требует большого контроля со стороны человека, отмечают китайские ученые: «Математические доказательства требуют абсолютной строгости, но даже доказательства, написанные экспертами, могут содержать тонкие ошибки, а результаты LLM, склонных к галлюцинациям, гораздо менее надежны».
Как это устроено
Первый компонент их системы — агент неформальных рассуждений под названием Rethlas. Он использует поисковую систему математических теорем Matlas, чтобы находить стратегии решения и строить возможные доказательства, имитируя работу человека.
Когда Rethlas находит кандидата в доказательство, в дело инструмент проверки — агент формальной верификации Archon. С помощью поисковой системы формальных теорем LeanSearch он превращает неформальные доказательства в полностью верифицированные проекты на Lean 4. Lean 4 — это интерактивный верификатор теорем и язык программирования. К нему прилагается библиотека Mathlib, поддерживаемая сообществом и содержащая сотни тысяч теорем и определений.
Как проверяли
Разработчики протестировали свою систему на открытой проблеме Андерсона, результатами чего поделились в препринте на arXiv. ИИ нашел контрпример, опровергающий гипотезу, и проверил его. На все ушло около 80 часов работы. Единственным вмешательством человека стала загрузка файлов с платного доступа, которые Archon не мог получить самостоятельно.
Самостоятельность ИИ-математика не отменяет широких возможностей для вмешательства в его работу. Пользователь может руководить процессом примерно так же, как объяснял бы доказательства аспиранту, чтобы ускорить процесс.
«В целом наши результаты показывают, что для реальной открытой проблемы в математике агенты неформальных рассуждений и формальные агенты могут эффективно сотрудничать», — заключается в статье.
