150-річна загадка на мільйон доларів: 650 ідей ШІ Anthropic
Нейромережа в Anthropic отримала завдання перевірити математичну гіпотезу й майже півтори доби працювала над ним автономно. За цей час система перебрала сотні підходів, розподілила роботу між десятками спеціалізованих субагентів і підготувала результат, який згодом перевірили люди та формалізували в Lean.
Як нейромережа шукала доведення
Завдання моделі сформулював співробітник Anthropic, який не мав спеціальної математичної підготовки. Після отримання інструкції нейромережа самостійно організувала подальшу роботу та координувала її приблизно 36 годин.
У процесі система перевірила близько 650 різних ідей. Для цього вона згенерувала приблизно 31 мільйон вихідних токенів і залучила 60 субагентів, кожен із яких виконував окрему функцію.
Як розподілили роботу між субагентами
Усередині системи завдання поділили на кілька напрямів — від пошуку математичних підходів до перевірки обчислень і підготовки тексту.
- 2 субагенти розробляли основні математичні ідеї;
- 13 субагентів генерували додаткові варіанти розв’язання для цієї групи;
- 30 субагентів намагалися сформулювати нові концепції, але не досягли успіху;
- 13 субагентів перевіряли розрахунки та шукали помилки;
- 2 субагенти допомагали оформити первинну версію наукової роботи.
Підсумковий результат додатково перевірили двоє штатних математиків Anthropic. Після цього висновки перевели у формальний вигляд за допомогою Lean — системи інтерактивного доведення теорем, яка дає змогу поетапно перевірити коректність математичних міркувань.
ШІ дедалі частіше використовують у математиці
Цей випадок став частиною ширшої тенденції: нейромережі вже допомагають дослідникам працювати над складними математичними завданнями. Протягом року алгоритми розв’язали кілька проблем Ердеша, модель Astra від OpenAI довела десять важливих наукових результатів, а команда Anthropic заявила про спростування відомої гіпотези Якобі.
Водночас роль штучного інтелекту в науці залишається предметом дискусій. Частина математиків побоюється, що активне використання ШІ розмиває поняття особистого авторства та ускладнює визначення відповідальності за відкриття.
Іншу позицію висловлює лауреат Філдсівської премії Тімоті Ґоверс. На його думку, штучний інтелект може позитивно вплинути на розвиток математики, якщо використовувати його як інструмент для пошуку ідей, перевірки гіпотез і формалізації доказів, а не як заміну науковцям.
Отже, нейромережі вже здатні самостійно організовувати складні математичні пошуки, але остаточна перевірка людьми та формальні системи на кшталт Lean залишаються важливими для підтвердження надійності результатів.
