Модель Anthropic продвинулась в решении гипотезы Римана

· Искусственный интеллект
Неопубликованная модель Anthropic не доказала гипотезу Римана, но заметно расширила границу, до которой её справедливость подтверждена. Работу проверили штатные математики компании и формализовали в Lean.

cover.svg

Гипотеза Римана остаётся одной из главных нерешённых задач математики уже более 150 лет: речь идёт о распределении простых чисел, а за общее доказательство назначена награда в 1 миллион долларов, до сих пор не востребованная. Современные ИИ-модели её тоже не решили — но, как выяснилось, способны продвинуться дальше, чем можно было ожидать.

В понедельник Anthropic сообщила, что её ещё не выпущенная модель существенно расширила нижнюю границу значений, для которых гипотеза подтверждена. Результат подтвердили двое штатных математиков компании, а само рассуждение формализовали с помощью открытого пруф-ассистента Lean.

Как это было сделано

Не менее любопытен сам процесс. Сотрудник Anthropic без серьёзной математической подготовки предложил модели «всерьёз попытаться» доказать гипотезу, после чего оставил её координировать работу на протяжении полутора суток. За это время модель перебрала 650 различных идей, распределив задачу между 60 субагентами и израсходовав в общей сложности 31 миллион выходных токенов.

В сноске к статье приводится показательная «раскладка ролей»: из 60 субагентов двое отвечали за ключевые математические идеи, 13 подбрасывали им подсказки, ещё 30 пытались (безуспешно) придумать что-то новое, 13 выступали проверяющими, а последние двое написали первоначальный черновик работы.

Не первый и не единственный случай

Это лишь очередной результат в череде математических достижений больших языковых моделей. За год ИИ решил ряд задач Эрдёша, OpenAI представила десяток результатов, доказанных её внутренней моделью «Astra», а другая команда Anthropic опровергла давнюю гипотезу Якобиана.

Накопившиеся успехи вызывают в математическом сообществе одновременно восторг и тревогу. В опубликованном в июне заявлении группа видных математиков предупредила, что ИИ может подорвать важные ценности дисциплины — прежде всего представление о том, что доказательство должно принадлежать конкретным авторам, которые ставят своё имя под открытием и отвечают за его правильность.

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


Источник: TechCrunch

Комментарии

Войдите, чтобы комментировать.

  • Пока нет комментариев.