Дешевые LLM судят математические доказательства лучше Claude Opus 4.7

Проблема стоимости оценки

Автоматическая оценка математических доказательств на естественном языке — узкое место в тестировании систем математического мышления. Использование передовых (frontier) LLM-судей, таких как Claude Opus 4.7 или Gemini 3.1 Pro, обеспечивает высокую точность, но создает неприемлемые затраты. Исследователь Бенджамин Грейцель (Benjamin Grayzel) поставил задачу: можно ли заменить дорогие модели дешевыми открытыми аналогами, сохранив надежность оценки.

Эксперимент на IMO-GradingBench

Для проверки гипотезы был использован валидационный набор данных из 200 примеров бенчмарка IMO-GradingBench. В эксперименте участвовали три «бюджетные» модели, которым предоставлялись кандидаты на доказательство, эталонное решение и рубрика оценки. Результаты их согласования с человеческими оценками сравнивались с эталонными моделями.

Стратегия консенсуса: правило «All-Three-Pass»

Изначально предполагалось, что большинство голосов (majority vote) среди трех дешевых моделей даст лучший результат. Однако на полном наборе из 1000 примеров исследователи обнаружили, что правило unanimous agreement (все три модели должны одобрить доказательство) дает наилучшие показатели. Этот подход обеспечивает максимальное совпадение с человеческой оценкой (pass-agreement) и высокую точность (precision), а также минимальную дисперсию результатов между запусками.

Выводы для индустрии

Главный вывод исследования: дешевые модели способны конкурировать с лидерами рынка в задачах оценки доказательств, снижая затраты на один-два порядка. Авторы рекомендуют использовать стратегию «all-three-pass» в качестве стандартного решения для развертывания, хотя и отмечают, что это правило было выявлено постфактум и требует независимой репликации.

Источник: arXiv cs.CL ↗