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

[svyatogorodski]

Думаю, что простым смертным понять. Я как раз в IAS слушал лекцию про какое-от число результатов доказанных ИИ, там в одной статье и Тау был в соавторах (И Элленберг из известных людей). В общем-то все это было про довольно простые комбинаторные задачи. Деталей не помню, но что-то от Эрдоша, что-то еще откуда-то. И от ИИ там требовали не прям таки гениальныйход найти, а улучшить известную оценку (типа, (с потолка говорю) в задаче покрытия чего-то чем-то лучшая известная оценка 3n^2-5n+27 а он улучшил ее на константу, или линейный фактор или еще что). Ему скормили кучу таких (может сложных, но элементарных и вряд ли хорошо мотивированных) задач, где-то он улучшил, где-то нашел в литературе лучшую известную, где-то не нашел/ухудшил. Короче, это скорее тестирование нового средства, а не прям "Тау решает то, что 20 лет хотел но не мог"...

[ny_quant]

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

[svyatogorodski]

На 10 лет я б бутылку поставил. На данный момент он сам не знает, решил он или нет. Как студент, кторый приходит на экзамен, повторяет что-то что запомнил, но без понятия то он повторяет, или не то (и кстати большой филисофский вопрос, что надо ставить, если он повторяет правильно, но ясно, что не понимает...)

Первый шаг будет формализовать доказательство хоть в том же lean. Дальше прочитать, что люди печатали и формализовать или найти ошибки, и только потом можно ждать что он что-то там начнет делать сам, а не на уровне "где-то нашел вам идею", а дальше вы думайте. Кстати уже это может сделать переворот в работе, когда печатать будут только формализованные доказательства, а доводить будет ИИ, но и до этого пока как до луны. Хотя тут возможно у ИИ есть шанс в среднесрочной перспективе.