ИИ под названием AlphaProof был разработан командой Google DeepMind. Он способен не только решать сложные задачи, но и автоматически проверять свои решения. Для этого используется среда Lean, которая выступает в роли строгого «учителя», проверяющего каждый логический шаг алгоритма.

Процесс обучения AlphaProof включал три этапа. Сначала системе предоставили 300 млрд токенов общего кода и математического текста для понимания логики, математического языка и структуры программирования. На втором этапе ИИ получил 300 тыс. формальных доказательств, созданных экспертами в среде Lean, чтобы изучить проверенные подходы к доказательствам.

На заключительном этапе AlphaProof начал решать задачи самостоятельно. Система обработала порядка 80 млн формальных математических задач, используя обучение с подкреплением. Алгоритм проб и ошибок позволял ИИ усваивать сложные стратегии рассуждений, выходящие за рамки простого копирования человеческих примеров.

Для самых сложных задач исследователи применяли метод Test-Time RL (TTRL), при котором создаются и решаются миллионы упрощенных версий целевой задачи, пока не будет найдено верное решение.

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