От решателей к исследователям: LLM и формальная математика на переднем крае

Развитие больших языковых моделей (LLM) в качестве средств автоматического доказательства теорем уже принесло заметные успехи в генерации формальных доказательств для чётко поставленных задач. Однако эти системы всё ещё далеки от работы с математикой исследовательского уровня — открытием новых теорем или разрешением открытых гипотез.

В чём ограниченность текущих подходов

Современные системы, опирающиеся на языки интерактивного доказательства теорем (ITP), эффективны преимущественно в условиях, когда задача заранее определена. Исследовательская математика, напротив, часто является открытой, недоспецифицированной и многоуровневой по абстракции.

Авторы выделяют несколько ключевых проблем существующих решений:

• недостатки датасетов для обучения и оценки;
• слабая поддержка реляционных структур в математическом контексте;
• ограниченные возможности математического исследования и поиска;
• неразвитая экосистема инструментов;
• неэффективное взаимодействие человека и ИИ.

Предлагаемый сдвиг

Главный тезис работы — необходимость перехода от предопределённых «решателей» к исследовательским агентам, способным применять строгую формальную математическую аргументацию к задачам переднего края науки.

В статье представлен систематический обзор области, охватывающий датасеты, автоформализацию и синтез доказательств, а также сформулирована стратегическая дорожная карта дальнейшего развития AI4Math.

Источник: cs.CL updates on arXiv.org