ИИ за несколько дней решил задачу, над которой математики бились более 10 лет.

Китайский искусственный интеллект самостоятельно решил открытую задачу, предложенную более десяти лет назад американским математиком, сообщает команда разработчиков из Пекинского университета.

Гипотезу о свойствах квазиполных нетеровых локальных колец (абстрактных алгебраических структур) сформулировал покойный бывший профессор Университета Айовы Дэн Андерсон в 2014 году. С тех пор доказать ее не удалось.

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

«Используя эту структуру, мы успешно решили открытую задачу коммутативной алгебры и автоматически завершили доказательство практически без вмешательства человека», — пишут они. «Эта работа служит конкретным примером того, что математические исследования можно значительно автоматизировать с помощью ИИ».

Математики все чаще обращаются к большим языковым моделям (LLM), чтобы помочь им в своих исследованиях, и ИИ добился впечатляющих успехов в этой области знаний. Но склонность к галлюцинациям затрудняет получение надежных результатов.

Однако выполнение задач исследовательского уровня с помощью искусственного интеллекта по-прежнему требует большого контроля со стороны человека, отмечают китайские ученые: «Математические доказательства требуют абсолютной строгости, но даже доказательства, написанные экспертами, могут содержать незначительные ошибки, а результаты LLM, склонных к галлюцинациям, гораздо менее надежны».

Как это работает

Первый компонент их системы — это неформальный агент рассуждения под названием Rethlas. Он использует поисковую систему математических теорем Matlas для поиска стратегий решения и построения возможных доказательств, моделируя деятельность человека.

Когда Ретлас находит кандидата на доказательство, используется инструмент проверки — формальный агент проверки Архон. Используя формальную поисковую систему теорем LeanSearch, он превращает неформальные доказательства в полностью проверенные проекты в Lean 4. Lean 4 — это интерактивный инструмент проверки теорем и язык программирования. Он поставляется с поддерживаемой сообществом библиотекой Mathlib, содержащей сотни тысяч теорем и определений.

Как они проверяли

Разработчики протестировали свою систему на открытой задаче Андерсона, результаты которой были опубликованы в препринте на arXiv. ИИ нашел контрпример, опровергающий гипотезу, и проверил ее. На все это ушло около 80 часов работы. Единственным вмешательством человека была загрузка файлов с платного доступа, которые Archon не мог получить самостоятельно.

Независимость ИИ-математика не отменяет широких возможностей вмешательства в его работу. Пользователь может руководить процессом почти так же, как он объясняет аспиранту доказательства, позволяющие ускорить процесс.

«В целом наши результаты показывают, что для реальной открытой задачи в математике неформальные рассуждающие агенты и формальные агенты могут эффективно сотрудничать», — заключает статья.