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

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

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

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

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

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

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

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