Математика всегда была фундаментом технологического прогресса, лежащим в основе многочисленных инноваций и научных открытий. Тем не менее, развитие самой математики зачастую происходит сравнительно медленно, что обусловлено характеристиками и сложностями процесса доказывания новых теорем и разработкой общих абстракций. Программа ExpMath, инициированная DARPA, нацелена на преодоление этих ограничений с помощью искусственного интеллекта, который сможет стать настоящим соавтором математиков, значительно ускоряя процесс открытия новых знаний. Одним из ключевых барьеров в прогрессе чистой математики является трудоёмкий процесс разбиения сложных задач на полезные леммы — небольшие утверждения, которые затем объединяются в доказательства более сложных теорем. Этот этап требует от исследователя глубокого понимания и опыта, часто сопровождается интуитивным поиском и проверкой разных вариантов.
Леммы при этом должны иметь достаточно универсальный характер, чтобы быть применимыми не только в контексте текущей задачи, но и в будущих исследованиях. Кроме того, даже выявив кандидатные леммы, доказательство их полноты и корректности остаётся сложной, многоэтапной и длительной работой. Известны примеры попыток доказательств, где изначально были обнаружены ошибки или пробелы, как в случае с оригинальной версией доказательства теоремы Ферма Эндрю Уайлза, требовавших значительных усилий и времени для исправления. Современные формальные системы, такие как Lean, позволяют частично формализовать математические доказательства в виде программного кода, что может способствовать автоматизации проверки и даже поиска доказательств. Однако перевод математических рассуждений в формальную символику и обратно всё ещё представляет собой серьёзный вызов.
Прогресс в области искусственного интеллекта открывает новые перспективы для чистой математики. Современные модели, включая крупные языковые модели, показывают впечатляющие способности в обработке текста и решении некоторых математических задач, однако их потенциал в фундаментальных математических исследованиях остаётся ограниченным. Программа ExpMath поставила амбициозную цель — создать ИИ, который не просто будет рассчитывать или проверять математические факты, а станет полноценным соавтором, способным формулировать обобщённые абстракции и проводить доказательства на профессиональном уровне. Для достижения этой цели комплексный подход предусматривает несколько направлений разработки. Одно из них связано с автоматическим разбиением математических проблем на составные части, что позволит ИИ самостоятельно находить полезные леммы и формировать иерархии математических понятий.
Другое направление — работа с автоформализацией и умеренной автоинформализацией, то есть превращение классических математических рассуждений в формальный язык доказательств и обратно, что важно для интеграции традиционной математики с компьютерными системами. Важной особенностью программы является её тесное сотрудничество с профессиональным сообществом математиков. Чтобы добиться значимых результатов, необходимо не просто создавать технологии, но и проводить тщательную оценку их эффективности на реальных сложных задачах, до сих пор нерешённых или решавшихся с большим трудом. Оценка системы будет вестись не только на количественных критериях, но и с привлечением профессионалов — аспирантов и опытных исследователей в области математики. ExpMath делает особый акцент на технологической и методологической новизне.
Участникам программы предоставляется широкая свобода в выборе подходов и математических направлений. Они могут предложить решения, выходящие за рамки классической теории множеств и традиционных систем, изучать новые типы структур и разработать метамодели, ориентированные на рекурсию и нелинейные иерархии. Главное — чтобы решения были инновационными, реализуемыми и способными внести ощутимый вклад в ускорение математических исследований. Программа, в отличие от многих других проектов, не концентрируется на прикладных аспектах, таких как производительность компиляторов или применение в смежных областях науки и техники. Её фокус — только на чистой, доказательной математике.
Это делает ExpMath уникальным предприятием с чётким научным профилем и высокими требованиями к точности и глубине разработок. Важен и аспект открытости. DARPA призывает участников открывать исходные коды и методики, распространять их на условиях либеральных лицензий, таких как Apache или MIT. В то же время предусмотрены разумные исключения, связанные с сохранением научной валидности, например, держать закрытыми наборы вопросов для оценки работы систем, чтобы избежать искажения результатов из-за преждевременного доступа. Такой баланс направлен на обеспечение широкой коллаборации и при этом честную проверку методов.
Важный фактор успеха в ExpMath — междисциплинарные команды. Опыт в математике должен гармонично сочетаться с компетенциями в области искусственного интеллекта и автоматического рассуждения. Это связано с тем, что разработка эффектного ИИ-инструмента требует тщательного проектирования архитектуры, алгоритмов и пользовательских интерфейсов, способных удовлетворить жёсткие критерии профессиональной математики. Период реализации программы запланирован на тридцать шесть месяцев с регулярными оценками каждые полгода. В рамках этого времени предлагается достичь значительных успехов в автоматизации доказательств, формализации и создании полноценных инструментов, способных работать с разнообразными математическими классами задач.
Разрешается широкое географическое участие, включая иностранных специалистов и организации, при условии соблюдения правил безопасности и законодательства об экспорте технологий. Это дополнительно расширяет потенциал коллаборации и привлечения лучших умов мира к решению поставленных вызовов. ExpMath стремится радикально изменить устоявшиеся практики в математическом сообществе. В будущем такие ИИ-системы смогут существенно повысить продуктивность исследователей, освободив их от рутинных и технических аспектов, давая больше времени и ресурсов для креативных и концептуальных поисков. Это может стать прорывом не только для математики, но и для смежных наук, где роль математических методов растёт.
В целом, ExpMath — это попытка объединить лучшие достижения искусственного интеллекта с глубокой человеческой экспертизой для создания новых инструментов, способных ускорить и расширить горизонты чистой математики. Если программа достигнет поставленных целей, мы сможем наблюдать новую эру в развитии одной из старейших и самых фундаментальных наук человечества.
