ИИ-система стартапа, существующего 4 месяца, решила 9/12 задач в одном из самых сложных в мире экзаменов по математике
Putnam (полное название William Lowell Putnam Mathematical Competition) – это ежегодная очень сложная математическая олимпиада для студентов бакалавриата университетов США и Канады. Она считается сложнейшей на этом уровне. Средний результат часто составляет примерно 0–1 балл из 120.
В этом году олимпиада проходила на этих выходных. А сегодня никому неизвестный очень молодой стартап Axiom объявил о том, что их система AxiomProver решила 9/12 задач конкурса (8 из них в течение самого соревнованию, и одну после его окончания).
Это очень высокий результат. По прошлогодней шкале это было бы абсолютное первое место среди ~4000 участников + статус Putnam Fellow (топ‑10 за несколько лет). В этом году место пока неизвестно, потому что ранг зависит от общего распределения баллов.
Интересно, что модель не просто доказала утверждения на естественном языке, а формализовала их в Lean. То есть каждое решение уже дано в виде машинно-проверяемого proof‑скрипта.
Интересно, участвовали ли Google и OpenAI
Putnam (полное название William Lowell Putnam Mathematical Competition) – это ежегодная очень сложная математическая олимпиада для студентов бакалавриата университетов США и Канады. Она считается сложнейшей на этом уровне. Средний результат часто составляет примерно 0–1 балл из 120.
В этом году олимпиада проходила на этих выходных. А сегодня никому неизвестный очень молодой стартап Axiom объявил о том, что их система AxiomProver решила 9/12 задач конкурса (8 из них в течение самого соревнованию, и одну после его окончания).
Это очень высокий результат. По прошлогодней шкале это было бы абсолютное первое место среди ~4000 участников + статус Putnam Fellow (топ‑10 за несколько лет). В этом году место пока неизвестно, потому что ранг зависит от общего распределения баллов.
Интересно, что модель не просто доказала утверждения на естественном языке, а формализовала их в Lean. То есть каждое решение уже дано в виде машинно-проверяемого proof‑скрипта.
Интересно, участвовали ли Google и OpenAI
