Крах парадигмы «решателя»
Недавние прорывы в области AI4Math, основанные на больших языковых моделях (LLM), позволили автоматизировать генерацию формальных доказательств для четко определенных проблем. Однако, как отмечают авторы, текущие системы остаются фундаментально ограниченными. Они не способны справляться с математикой на переднем крае науки (frontier research), где задачи открыты, плохо специфицированы и требуют многоуровневой абстракции.
Ключевой тезис работы: следующий скачок в развитии ИИ для математики требует перехода от предопределенных решателей (solvers) к агентам-исследователям (research agents), способным вести строгое формальное рассуждение в условиях неопределенности.
Ключевые ограничения существующих систем
Авторы систематизируют барьеры, мешающие ИИ стать полноценным научным сотрудником. В таблице ниже приведены основные категории проблем, выявленные в исследовании:
| Категория | Суть проблемы |
|---|---|
| Данные (Datasets) | Нехватка качественных датасетов, отражающих процесс открытия, а не только финальные доказательства. |
| Реляционная структура | Сложность моделирования связей между различными областями математики и абстракциями. |
| Математическое исследование | Неспособность генерировать новые гипотезы или конъектуры без внешней подсказки. |
| Инструментальная экосистема | Ограниченная интеграция с внешними вычислительными инструментами и базами знаний. |
| Человек-ИИ коллаборация | Отсутствие эффективных протоколов взаимодействия, где ИИ выступает соавтором, а не просто калькулятором. |
Стратегическая дорожная карта
В работе представлен обзор текущих методов автоформализации и синтеза доказательств. Авторы подчеркивают, что для перехода к «исследовательскому» уровню необходимо пересмотреть архитектуру взаимодействия между LLM и интерактивными системами доказательства теорем (ITP). Это включает в себя создание систем, которые могут самостоятельно формулировать задачи, проверять их на непротиворечивость и предлагать новые направления исследований.
Значимость для сообщества
Участие в работе таких фигур, как Теренс Тао, придает исследованию особый вес. Оно сигнализирует о том, что сообщество формальной математики начинает воспринимать ИИ не как инструмент для автоматизации рутины, а как потенциального партнера в решении нерешенных проблем. Это меняет фокус разработки с повышения точности на бенчмарках (вроде MiniF2F) на создание гибких агентов, способных работать с «грязными» и неполными данными реального научного процесса.
Источник: arXiv cs.CL ↗