Мало им публикаций бойких 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