Через три года сможет ли ИИ-"Гений математики" стать соавтором доказательств?

Новый проект DARPA под названием expMath "нацелен на ускорение инноваций в математике с помощью искусственного интеллекта", пишет The Register. "Агентство передовых исследовательских проектов" США полагает, что математика развивается недостаточно быстро, согласно их статье.

Чтобы ускорить – или "экспоненциально увеличить" – темпы математических исследований, DARPA на этой неделе провела мероприятие Proposer's Day, чтобы привлечь техническое сообщество в надежде, что участники подготовят предложения для подачи после публикации официального запроса предложений (Broad Agency Announcement).

Существует проблема в том, что искусственный интеллект пока недостаточно умен. Он может решать математические задачи школьного уровня, но не задачи высшего уровня. Одна из презентаций от менеджера программы DARPA Патрика Шафто (Patrick Shafto) отметила, что OpenAI o1 "продолжает испытывать серьезные трудности даже с базовой математикой, несмотря на заявления о способностях к рассуждениям". Тем не менее, цель expMath – создать модели искусственного интеллекта, способные на:

• автоматическое разложение – автоматически разбивать утверждения на естественном языке на переиспользуемые леммы (доказанное утверждение, используемое для доказательства других утверждений); и
• автоматическую (ин)формализацию – переводить лемму на естественном языке в формальное доказательство, а затем переводить доказательство обратно на естественный язык.

“Как добиться более быстрого прогресса с помощью технологий и ИИ-агентов, решающих новые математические задачи?” – спрашивает бывший научный сотрудник DARPA Робин Роу (Robin Rowe), также давний читатель Slashdot robinsrowe.

DARPA заявляет, что "целью проекта Exponentiating Mathematics является радикальное ускорение прогресса в чистой математике путем разработки ИИ-соавтора, способного предлагать и доказывать полезные абстракции".

Роу цитируется в статье как основатель и генеральный директор исследовательского института искусственного интеллекта "Fountain Adobe". (Он сообщает The Register, что "тот факт, что это трехлетняя программа, говорит об озабоченности DARPA сложностью задачи. Это нетипично для DARPA.")

Роу настроен оптимистично. "Я думаю, мы добьемся успеха, честно говоря. Я думаю, что на это не потребуется три года. Но, возможно, потребуется три года, чтобы сделать это с использованием больших языковых моделей (LLM). Тогда возникает вопрос, насколько радикальных изменений готовы все?"

“Мы будем активно взаимодействовать с математическим и ИИ-сообществами, чтобы фундаментально изменить практику математики математиками”, – объясняет главная страница проекта. Они уже загрузили часовое видео с мероприятия Proposer's Day.

“Совершенно неясно, что современные системы искусственного интеллекта смогут успешно справиться с этой задачей...", – говорит менеджер программы Шафто в коротком видео, представляющем проект. Но...

“В математическом сообществе существует большой энтузиазм по поводу возможности изменений в том, как практикуется математика. Это открывает принципиально новые возможности для математиков. Но, конечно, они не являются исследователями в области искусственного интеллекта. Одной из мотиваций этой программы является объединение двух разных сообществ – людей, работающих над искусственным интеллектом для математики, и людей, занимающихся математикой – чтобы они решали одну и ту же проблему.

В своей основе это очень сложная и техническая проблема. И это хлеб с маслом DARPA – пытаться изменить мир. И я думаю, что это имеет потенциал для этого.”