ИИ и перспективы математики и математического образования

[ozheredov]

vpb в сообщении #1724800 писал(а):

А аспирантские задачи --- они, по большому счету, не ради науки, а ради того, чтобы обсиранты на этих задачах умственно развивались.

Есть два принципиально разных подхода:

а) аспирант = ребёнок, из которого вырастет будущий учёный;
б) аспирант = временный раб, поюзал и выкинул.

Сейчас повсеместно распространён вариант б), не в последнюю очередь по причине того что аспирант смотрит не в дом, а из дому, получит корочку и свалит в коммерцию

[Ende]

Выделена тема«Человеческое мышление vs. LLM»

[dsge]

Шутливая дистопия, взятая с другого форума и написанная 2 года назад. Специально для "гениальных аспирантов" ввел текст в гугл-переводчик. Может в самом деле не надо изучать ни языки, ни математику, а осваивать профессию сантехника?

Цитата:

«На прошлой неделе я получил известие о закрытии Принстонского института перспективных исследований, где я работаю, потому что ChatGPT 8 доказал все проблемы тысячелетия всего за несколько часов работы на суперкомпьютере. Доказательства впоследствии были подтверждены бывшими аспирантами-математиками (которые сейчас работают в OpenAI). Черт возьми. Просто черт возьми. Я вырос, делая *все* правильно. Меня признали лучшим теоретиком алгебры чисел за последние несколько десятилетий, и я заслуженно получил Филдсовскую премию. Я думал, что все мои открытия навсегда останутся в учебниках истории.

Теперь моя жизнь выглядит мрачной. MBA-специалисты планируют снести институт перспективных исследований вместе со всеми остальными университетами и превратить их в комплексы быстрого питания.

А потом все рухнуло на прошлой неделе. Было много других опытных математиков, многие из них намного старше меня, которые (как и я) просто не имеют другого источника дохода. Они могут научиться программировать, но…» Это тоже автоматизировано. Что касается тех немногих математиков, которые действительно работают в OpenAI, им не нужно больше, поскольку всё, что они делают, это проверяют доказательства, созданные ИИ.

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

Когда я упаковывал свои офисные вещи в коробки и переезжал, выпускник MBA, который закрыл мой исследовательский институт — тем самым оборвав мой спасательный круг — прошёл мимо меня и назвал меня «трансгендером», сказав, что «математика — это буквально только гейство». Я не могу в это поверить. Как этот полуграмотный «MBA» с IQ всего 60 может так со мной разговаривать? Весь мой мир рушится.

Вся моя жизнь, полная достижений, вела к этому моменту. К этому тупику.

— ок. 2029 г.

[Rasool]

Booker48 в сообщении #1724678 писал(а):

Mikhail_K
А следующие задачи такого рода уже некому будет ставить. Из сапиенсов, имею в виду.

Да, может возникнуть следующая цивилизация, уже машинная, более умная, чем человеческая. Но это уже тема для другого треда.

[MoonWatcher]

С Телеграм-канала Machinelearning:

Цитата:

AlphaProof Nexus: формальные доказательства начинают превращаться в инженерный пайплайн

Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.

Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.

Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.

Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.

Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.

Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.

Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.

Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.

Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.
Формальная проверка отсекает галлюцинации. Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.

Интересное дополнение на другом Телеграм-канале, Data Secrets:

Цитата:

Но есть нюанс: на самом деле DeepMind прогоняли через агента все 353 формализованные открытые задачи Эрдеша и сожгли гораздо больше ресурсов. Решение останавливали, если агент выходил за рамки 3000 итераций, и в итоге полностью решенных задач оказалось 9.

Advancing Mathematics Research with AI-Driven Formal Proof Search

[Rasool]

MoonWatcher в сообщении #1724697 писал(а):

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

Вот сейчас стоит действительно интересный вопрос: будет ли ИИ решать задачи Арнольда через 15 лет? И если будет, то какую структуру он будет иметь?

[dsge]

Demis Hassabis: "Doesn't matter how many Erdős problems you solve...I think it's far, far from what a true invention or someone like Ramanujan would have been able to do."

https://www.reddit.com/r/singularity/comments/1tn9s9s/demis_solving_erdos_problems_are_far_from_true/

Вики:

Цитата:

Sir Demis Hassabis is a British artificial intelligence researcher and entrepreneur. He is the chief executive officer and co-founder of Google DeepMind and Isomorphic Labs and a UK Government AI Adviser. In 2024, Hassabis and John M. Jumper were jointly awarded the Nobel Prize in Chemistry for their AI research contributions to protein structure prediction.

В отличие от Альтмана этот парень хорошо знает и понимает как все это работает.

[Booker48]

dsge в сообщении #1724923 писал(а):

В отличие от Альтмана этот парень хорошо знает и понимает как все это работает.

Бог с ним, с Альтманом. Критерий-то всё же есть какой-нибудь?
ОК, задачи Эрдёша - не true invention.
А что - true invention?
Есть ли граница в оценке работы?
Если бы задачу Эрдёша решил практикующий математик во время кофе-брейка - это было бы щитово? (Но ведь не решил).
Или всё же задача Эрдёша - это норм, но её решение следует "закрепить" за теми ребятами, которые создали промпт?
Подобно тому, как решение задачи четырёх красок "закреплено" за Аппелем и Хакеном?

[dsge]

Booker48 в сообщении #1724926 писал(а):

Если бы задачу Эрдёша решил практикующий математик во время кофе-брейка - это было бы щитово? (Но ведь не решил).

Часть этих задач решили естественные интеллекты. История умалчивает при каких обстоятельствах - во время кофе-паузы или пивной вечеринки. Нет интереса и желания проверять уровень математиков, которые решили задачи Эрдёша, достаточно того, что среди них нет ни Тао, ни Арнольда.

Booker48 в сообщении #1724926 писал(а):

Или всё же задача Эрдёша - это норм, но её решение следует "закрепить" за теми ребятами, которые создали промпт?

У тех ребят в трудовом контракте с OpenAI прописано чтобы они помалкивали по поводу того как на самом деле решены задачи Эрдёша.

[ozheredov]

Booker48 в сообщении #1724926 писал(а):

А что - true invention?

True invention - это, внезапно, true invention. Это если ИИ, обученный на материалах по хвизике до 1900 года, изобретет квантовую механику. Или комплексные числа. Инвеншон и решение задачи Эрдёша соотносятся между собой так же, как колбаса на рынке и суррогат колбасы в пятерочке.

[realeugene]

ozheredov в сообщении #1724945 писал(а):

Это если ИИ, обученный на материалах по хвизике до 1900 года, изобретет квантовую механику.

Люди для этого много экспериментировали.

[mihaild]

dsge в сообщении #1724942 писал(а):

Нет интереса и желания проверять уровень математиков, которые решили задачи Эрдёша, достаточно того, что среди них нет ни Тао, ни Арнольда

Тао есть https://arxiv.org/abs/1509.05363.

[Booker48]

ozheredov в сообщении #1724945 писал(а):

True invention - это, внезапно, true invention. Это если ИИ, обученный на материалах по хвизике до 1900 года, изобретет квантовую механику. Или комплексные числа.

Такого рода изобретения делаются, наверное, раз в десятилетие. Сколько таких изобретений в математике сделано, пусть в текущем веке?
Я правда не знаю.

[MoonWatcher]

Booker48 в сообщении #1724952 писал(а):

Такого рода изобретения делаются, наверное, раз в десятилетие.

Раз в истории науки, нет? Причем в случае комплексных чисел это не было разовым открытием.

[dsge]

mihaild в сообщении #1724950 писал(а):

Тао есть https://arxiv.org/abs/1509.05363 .

Ох! Тао вычеркиваем.

realeugene в сообщении #1724948 писал(а):

ozheredov в сообщении #1724945 писал(а):

Это если ИИ, обученный на материалах по хвизике до 1900 года, изобретет квантовую механику.

Люди для этого много экспериментировали.

А если КМ заменить на ОТО и год до 1914.