DARPA планирует «дать толчок математическим инновациям с помощью ИИ» в рамках проекта expMath

Управление перспективных исследовательских проектов Министерства обороны США (DARPA) запустило проект, получивший название expMath. Проект направлен на то, чтобы дать толчок математическим инновациям с помощью искусственного интеллекта ^[1].

«Цель Exponentiating Mathematics (expMath) — радикально ускорить темпы прогресса в области чистой математики ^[2] путём разработки ИИ-помощника, способного предлагать и доказывать полезные абстракции», — пишет ^[3]DARPA.

Согласно исследованию, которое провели в 2021 году Лутц Борнманн, Робин Хауншильд и Рюдигер Мутц, общий темп роста научных публикаций в различных дисциплинах составляет 4,1%. При этом, по словам ^[4]менеджера программы DARPA Патрика Шафто, математика прогрессировала в период с 1878 по 2018 год очень медленно.

Толчком к прогрессу, как правило, служат открытия и инновации, напомнил Шафто. Например, в области естественных наук в период с 1806 по 1848 год (эпоха Жана-Батиста Ламарка и Чарльза Дарвина) темп роста публикаций составил 8,18%. А в области физических и технических наук рост составил 25,41% между 1793 и 1810 годами (период, который последовал за публикацией работы Жозефа-Луи Лагранжа «Аналитическая механика»).

«Таким образом, эти области претерпели изменения, а математика — нет, и мы хотим эти изменения в математику привнести», — заявил Шафто.

Предлагаемый DARPA ускоритель инноваций — искусственный интеллект — пока плохо справляется с математикой. Как отмечает Шафто, «OpenAI o1 (Strawberry) терпит полную неудачу в базовой математике, несмотря на заявления о возможностях рассуждать». 

Цель expMath — создать модели ИИ, способные к автоматической декомпозиции (разложение утверждений из естественного языка на леммы естественного языка) и автоматической (не)формализации (перевод леммы естественного языка в формальное доказательство, а затем перевод доказательства обратно на естественный язык).

«Совершенно неясно, смогут ли нынешние системы ИИ преуспеть в этой задаче. Но в математическом сообществе много энтузиазма по поводу изменений в математических практиках. Это открывает принципиально новые возможности для математиков. Конечно, они не исследователи ИИ. И мы хотим объединить два разных сообщества — людей, которые работают над инструментами ИИ для математики, и людей, которые занимаются математикой, — чтобы мы решали одну и ту же проблему», — заключил Шафто.