IMO 2025 Gold 🥇

Как можно было увидеть из предыдущих постов, за последний год модели начали показывать очень хорошие результаты в областях, где легко проверить правильность ответа. Например, на большинстве математических бенчмарков, где нужно выбрать правильный ответ, или где ответ это одно число/короткая формула, топовые модели набирают 90%+.

Дела обстоят хуже в областях, где сложно автоматически проверить ответ. Например, модели все еще плохо придумывают шутки. И они все еще плохо решают математические задачи, где нужно написать доказательство, а не только посчитать итоговый ответ. Одной из олимпиад, где нужно так делать, является IMO (International Math Olympiad).

В прошлом году DeepMind показал, что если перевести задачи в "проверяемый" язык, и вместо человеко-читаемых доказательств просить доказательтва на Lean (где можно автоматически проверить, правильное оно или нет), то специализированные модели уже могли получить серебрянную медаль на IMO.

В этом году наша новая экспериментальная модель смогла полностью решать 5 из 6 задач IMO (соответствует золотой медали) и привести доказательства на обычном языке, без использования Lean. Вот тут можно почитать больше подробностей, а тут сами доказательства.