➗ Стартап Axiom решает Putnam на 12/12 и переопределяет путь к AGI через формальную верификацию

Семимесячный стартап Axiom Math в 2025 году решил все 12 задач престижного экзамена Putnam (8/12 в лимите времени) — результат выше, чем у лучших студентов (110/120) и ближайшей AI-системы DeepSeek (103/120). Медианный балл на Putnam обычно 0–1. Но для CEO Axiom Карины Хонг это лишь начало: она считает, что код — необходимое, но недостаточное условие для AGI.

Ключевая идея Axiom — «верифицированный AI» через формальные доказательства в системе Lean. В отличие от статистических методов вроде GRPO, Lean-верификатор даёт абсолютно надёжный сигнал подкрепления: доказательство либо верно, либо нет. Это радикально повышает эффективность обучения и качество результатов.

На бенчмарке Verina (генерация кода + доказательство корректности) Axiom достиг 99% (187/189) против 4.9% у OpenAI o3. Стартап также открыл инструментарий AXLE — набор интерактивных Lean-приложений для исследования и проверки математических доказательств.

#AI #Science #Mathematics #Axiom #Lean