Команда исследователей во главе с Зэю Чжэном (Zeyu Zheng) представила ReuF2F — новый бенчмарк, предназначенный для оценки способности AI-агентов решать открытые математические задачи. В отличие от существующих наборов данных, которые часто содержат уже решенные или слишком известные проблемы, ReuF2F фокусируется на задачах уровня исследовательских стажировок для студентов (REU), которые остаются нерешенными и менее изученными.
Суть и методология
Ключевая идея ReuF2F заключается в использовании формальной математики (язык Lean 4) для создания строго проверяемых условий. Это позволяет избежать субъективности при оценке решений. Для каждого из 244 включенных в бенчмарк проблем агентам предоставляется проект в Docker-контейнере, содержащий саму задачу и ее логическое отрицание. Это симулирует реальные условия работы coding-агентов, где система должна не просто написать код, а доказать корректность решения.
Для обеспечения справедливого сравнения разработчики создали Leanimum-agent на базе mini-SWE-agent, который служит унифицированной платформой для запуска различных моделей.
Результаты тестирования
Эксперименты показали, что даже самые продвинутые современные модели демонстрируют скромные результаты. Лучший из протестированных AI-агент смог корректно решить и формально доказать лишь около 40% задач. Это указывает на значительный разрыв между текущими возможностями AI и необходимостью для надежного автоматизированного решения открытых научных проблем.
| Параметр | Значение / Описание |
|---|---|
| Название бенчмарка | ReuF2F |
| Язык формализации | Lean 4 |
| Количество задач | 244 |
| Источник задач | Research Experiences for Undergraduates (REU) |
| Результат лучшего агента | ~40% решенных задач |
| Инфраструктура | Docker-контейнеры, Leanimum-agent (на базе mini-SWE-agent) |
Почему это важно
По мере того как AI-системы начинают претендовать на роль соавторов в научных исследованиях, критически важным становится наличие надежных механизмов верификации. ReuF2F закрывает пробел в оценке именно открытых проблем, а не рутинных упражнений. Низкий процент успешных решений (40%) служит четким индикатором того, что текущие модели требуют существенных улучшений в области логического вывода и долгосрочного планирования для работы с нетривиальной математикой.
Источник: arXiv cs.AI ↗