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