Модель Anthropic, о которой компания пока не раскрывает подробностей, добилась заметного прогресса по гипотезе Римана — одной из самых известных нерешённых задач математики. Речь не идёт о полном доказательстве, однако модель смогла существенно повысить нижнюю границу числа случаев, для которых гипотеза подтверждается.
Гипотеза Римана остаётся нерешённой более 150 лет. Она связана с распределением простых чисел, а за общее доказательство по-прежнему обещана награда в $1 млн.
По данным Anthropic, работу запустил сотрудник компании без серьёзной математической подготовки. Он предложил модели «по-настоящему взяться» за доказательство, после чего оставил её работать на полтора дня.
За это время система проверила 650 разных идей, задействовала 60 субагентов и суммарно потратила 31 миллион токенов.
- 2 субагента выработали ключевые математические идеи;
- 13 помогали им дополнительными предложениями;
- 30 пытались найти новые идеи, но без результата;
- 13 выступали проверяющими и оценивали корректность рассуждений;
- ещё 2 помогли подготовить начальную версию статьи.
Как сказано в сноске к статье Anthropic: «Из 60 субагентов двое отвечали за разработку ключевых математических идей». Далее компания уточняет, что 13 агентов вносили вклад в эти идеи, 30 не смогли предложить новые подходы, 13 проверяли корректность аргументов, а последние двое участвовали в подготовке первого варианта работы.
Результат проверили два математика Anthropic. Формализация доказательной части была выполнена с помощью Lean — открытого инструмента для формальной проверки математических доказательств.
Это продолжает серию результатов, в которых большие языковые модели показывают заметный прогресс в математике. В этом году ИИ-системы уже использовались при решении ряда задач Эрдёша. OpenAI также недавно представила десять крупных результатов, доказанных её внутренней моделью Astra, а отдельная работа Anthropic ранее опровергла давнюю гипотезу Якобиана.
Рост числа таких работ вызвал в математическом сообществе и интерес, и тревогу. В публичном заявлении, подписанном в июне, группа известных математиков предупредила, что ИИ может поставить под вопрос важный принцип дисциплины: математические доказательства должны быть связаны с конкретными авторами, которые получают признание за открытие и несут ответственность за его корректность.
При этом единого мнения нет. В ответном посте лауреат Филдсовской премии Тимоти Гауэрс допустил, что влияние ИИ может изменить математику более неоднозначно и, возможно, полезно.
Гауэрс написал: «Если мы придём к ситуации, в которой математические теоремы больше не связаны с именами математиков, возможно, это будет не более проблемно, чем то, что звёзды не называют в честь астрономов и большинство вообще никак не называют».
Источник: Anthropic, The Verge.
