На недавней Международной математической олимпиаде 2024 года произошел уникальный случай: искусственный интеллект AlphaProof, разработанный Google DeepMind, смог достичь результатов, сопоставимых с серебряной медалью, что ранее не удавалось ни одной ИИ-системе. AlphaProof предназначен для решения математических задач, используя строгие формальные доказательства. В отличие от обычных языковых моделей, которые могут допускать ошибки в выводах, AlphaProof проходит формальную проверку в системе Lean, обеспечивая корректность своих рассуждений.

Для создания AlphaProof потребовалось три этапа: обучение на 300 миллиардах токенов, загрузка 300 тысяч готовых доказательств и выполнение 80 миллионов формализованных задач с использованием обучения с подкреплением. Это позволило ИИ разрабатывать собственные стратегии поиска решений. В дополнение к этому, для сложнейших задач была добавлена система Test-Time Reinforcement Learning, которая генерирует упрощенные версии задач для обучения.

Исследователи отметили, что AlphaProof может не только участвовать в олимпиадах, но и помогать в проверке математических текстов и разработке новых теорий.