AI Axiom solved all Putnam competition problems

[ny_quant]

using the formal verification language Lean, 8 of which within the exam time

По ссылке приводятся все решения. Впечатляет.

Из комментариев на LinkedIn (дать ссылку не получается):

Looking at the GitHub repo, problem B5 took 354 minutes and 18M tokens. B6 took 494 minutes and 21M tokens.

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

Comments

[lemberger]

Как всегда в таких случаях, непонятно, что делала машина, а что люди.

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

У меня есть с этим делом некоторый опыт: я наблюдал вживую, как ИИ используют для решения математических задач. Банальны упражнения оно делает. Чуть менее банальные - гонит белиберду.

[ny_quant]

У меня тоже есть и в общем согласен. Хотя "банальные" понятие относительное. Как говорится, one person's signal is another person's noise. Вы считаете, что все эти задачи банальные?

Тем не менее, я пользовался chatgpt, grok and claude, а не эту систему. Вы наверное тоже. Прогресс не стоит на месте.

[lemberger]

Что все - не считаю (и во все не вчитывался). Из двух названных - одна тривиальное упражнение на обязательном курсе, другая несложная и скучная. Но главное - они не говорят, каков там вклад людей. Полагаю, что весьма не маленький - вот как Святогородский ниже объясняет.

Сам я, кстати, никаким ИИ ни разу не пользовался.