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

[juan_gandhi]

Wow, this is impressive. I couldn't believe. And Lean seems to be the right language to formulate all this.

[lemberger]

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

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

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

[ny_quant]

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

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

[lemberger]

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

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

[svyatogorodski]

Я ему недавно дал упражнение по теории полей классов (неожиданно возникшее у меня в реале). Гнал пургу и гпт и грок. Пишешь ему -- пурга, неверно уже для умеренного ветвления, да-да ты прав, а вот так? Опять пурга. Да, да а так -- блин, опять умеренное ветвление не проходит. В конце спросил, аможет ли это быть Х (тоже неверно, но очень хотелось) -- гпт сказал да, грок -- нет, оба дали липовое обоснование.

Коллеги говорят, что сразу он (почти) никогда ничего толкового не отвечает. Но если много раз переспросить, объяснить, и т.д. то иногда может подкинуть интересную идею. ЭЖто все что можно пока выловить на серьезном уровне (не низовая комбинаторика, алгебра и т.п.)

[ny_quant]

Недавно читал что сам Терренс Тао использовал какой-то ИИ для чего-то, что простым смертным не понять.

Кто знает, может быть через пару итераций эта система станет полезной для профессионалов.

[svyatogorodski]

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

[ny_quant]

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

[svyatogorodski]

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

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