ИИ в математике: подходы Anthropic, OpenAI и DeepMind

Бедные, бедные математики…. Мало им публикаций бойких OpenAI и Anthropic, посвященных решениям сложных и важных математических проблем топовыми ИИ-моделями, так тут еще и DeepMind туда же. На самом деле, подходы трех компаний разнятся: 1. Anthropic постарался сохранить human-in-the-loop: Клод предложил центральную идею для опровержения двух давних гипотез, после чего компания привлекла и оплатила работу двух исследователей; они подготовили понятное людям изложение доказательства.(Впрочем, математики все равно громко обиделись и потребовали запретить ИИ лезть в их уютную песочницу) 2. OpenAI на днях опубликовала более 700 математических рукописей, созданных ИИ и сгруппированных вокруг 372 проблем — по сути, завалила математиков грудой черновиков “а теперь сами с этим разбирайтесь”. Неудивительно, что такой шаг просто выбесил математиков. 3. А вот у Deep Mind вчера вышла статья в Science с результатами работы представленной еще в мае системы AlphaProof Nexus. Авторы сообщают о решении девяти задач из каталога проблем Эрдёша. Это уже выглядит как нормальная исследовательская математика, причем с малым процентом успехов (с первого захода решены 9 задач из 343). С другой стороны, реши человек эти 9 из 343 — он заслужил бы от коллег немало хвалебных эпитетов. Реакцию матсообщества на этот третий удар я еще уду читать ближайшие несколько дней, но восторгов там не жду:) В итоге становится очевидно: налицо острый дефицит: ответы вдруг посыпались как из рога изобилия, и оказалось, что категорически не хватает людей и институтов, способных превратить/интегрировать эти ответы в общее знание. Для математиков, многим из которых процесс неспешных поисков ответа много важнее самих ответов, это представляется катастрофой. В уютную посудную лавку забрело семейство очень проактивных слонов. Прекрасно, что ИИ-лабы очень конкретно и убедительно ставят вопрос о сути науки; над ним предстоит серьезно думать, потому что старые ответы (типа “суть в том, чтобы несколько человек могли понимать происходящее”) уже явно не годятся. Как отмечают авторы статьи в Science,

Bridging the generative power of large language models (LLMs) with the rigor of formal verification could fundamentally redefine mathematical research practice.

https://www.science.org/doi/10.1126/science.aej2213