Новый бенчмарк MA-ProofBench: даже GPT-5.5 решает лишь 16% задач по матанализу
Исследователи представили MA-ProofBench — первый формальный бенчмарк, предназначенный для оценки больших языковых моделей (LLM) в области автоматического доказательства теорем математического анализа. Работа опубликована в репозитории arXiv.
Бенчмарк включает 200 формализованных теорем, охватывающих 6 ключевых тем и 27 подкатегорий: теория меры и интегрирования, комплексный анализ, функциональный анализ и другие. Задачи разделены на два уровня сложности: 100 задач уровня бакалавриата (Level I) и 100 задач уровня квалификационного экзамена PhD (Level II).
Каждая задача прошла трёхэтапную верификацию: формулировка человеком с помощью LLM, формализация и независимая экспертная проверка. Это обеспечивает соответствие формальных утверждений оригинальным математическим постановкам.
На MA-ProofBench протестировали несколько современных моделей общего назначения и формальных доказывателей теорем. Результаты оказались скромными: лучший результат показала модель GPT-5.5 — 16% успешных решений на Level I и всего 5% на Level II. Большинство моделей на уровне PhD показали результат, близкий к нулю.
Анализ ошибок выявил две основные проблемы: галлюцинации при работе с библиотекой Mathlib и неполные доказательства. При этом на естественноязыковой версии задач модели справлялись заметно лучше, что указывает на разрыв между неформальными и формальными рассуждениями.
Авторы подчёркивают, что MA-ProofBench призван стать надёжным ориентиром для отслеживания прогресса в формальных математических рассуждениях в продвинутых областях. Бенчмарк доступен для сообщества и может стимулировать развитие более мощных методов автоматического доказательства.
