➕ MathAtlas: новый бенчмарк для автоформализации математики

Исследователи представили MathAtlas — первый крупномасштабный бенчмарк для автоформализации математики на уровне graduate и research. Датасет включает ~52 тыс. теорем, определений, упражнений, примеров и доказательств, извлечённых из 103 учебников по математике для магистров и аспирантов.

Уникальная особенность MathAtlas — граф математических зависимостей с ~178 тыс. связей. Это первый бенчмарк, учитывающий такие зависимости, что позволяет тестировать системы автоформализации, способные работать с контекстом.

Эксперименты показали, что MathAtlas крайне сложен: лучшие модели достигают лишь 9,8% корректности на теоремах и 16,7% на определениях. На подмножестве MA-Hard (700 объектов с самыми глубокими деревьями зависимостей) точность падает до 2,6%.

#Tech #Ai #Science #MathAtlas