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

[yucca]

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

[ny_quant]

Ага, я тоже это попробовал, но бросил. Слишком много работы за слишком мало денег.