RedactorНа Международной математической олимпиаде 2024 года произошёл уникальный инцидент: среди работ, получивших серебряные медали, оказалось решение, созданное искусственным интеллектом. Это стало первым случаем, когда ИИ достиг таких результатов на подобном уровне, сопоставимом с сильными школьниками. Система AlphaProof, разработанная Google DeepMind, предназначена для решения математических задач с использованием строгих формальных доказательств. В отличие от обычных языковых моделей, AlphaProof проводит формальную проверку всех рассуждений, используя систему Lean.
Подготовка AlphaProof включала три ключевых этапа: обучение на 300 миллиардах токенов, загрузка 300 тысяч готовых доказательств и выполнение 80 миллионов формализованных задач с использованием обучения с подкреплением. Команда также внедрила Test-Time Reinforcement Learning для улучшения подходов к решению сложных задач. Результаты не только впечатляют, но и открывают новые горизонты для использования технологии в математике и других областях.
