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

[DieselMachine]

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

А поросячий восторг исходит от малоизвестного математика, Radziwiłł, на которого внезапно обрушилась слава, только потому что ИИ использовал идеи метода, который он разработал. Поэтому он немного лучше других понимает эти "галлюцинации", но сам не подтвердил корректность доказательства, сказал только, что может набросать идею доказательства. Но последнее не обязанно быть верным.
Удивляет почему Quantamagazine публикует такие статьи до подтверждения правильности доказательства специалистами.

Строго говоря, да, доказательство пока ещё не выложили, подождём немного.
Вот ещё один результат от OpenAI - доказательство отсутствия нулей Зигеля. Его уже точно разобрали: Recently, various digestions and simplifications of the argument have been produced by Banks, by Kerr, and by Green.

[Ende]

Выделена тема «О научно-популярных СМИ»

[vpb]

Прочитал статью в Quanta. Как там написано, несколько математиков переизложили доказательство по-человечески, каждый по-своему, в текстах длиной от 7 до 13 страниц. Судя по этому, там всё в порядке: не могло же быть так, что сразу несколько человек что-то просмотрели. Точнее, могло, но это крайне маловероятно... ну крайне. Т.е. с правильностью вопроса нету. Однако же, реплика участника Diesel выше была про другое.

-- добавлено через 17 минут --

DieselMachine в сообщении #1736723 писал(а):

Это ещё ответ тем математикам, которые писали, что ИИ-доказательства не дают им понимания.
Стоило поковырять доказательство от OpenAI и сразу понимания прибавилось.

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

Кстати говоря, эта ситуация вообще не специфическая для ИИ, она и с людьми бывает. Как шутил Лиувилль,

Ж.Лиувилль писал(а):

Длинные доказательства хороши тем, что они длинные, а короткие --- тем, что короткие.

Это, как я понимаю, про это самое.

[Brizon]

Цитата:

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

Короче, в итоге коммуникация между математиками сводится к нулю. Результат немного предсказуем: остановка (научного) прогресса. Вот затем, чтоб такого не было, и нужны журналы, публикации и рецензенты. Искренне Ваш, К.О.

Я бы еще так добавил: если результат работы математика не становится известен научному сообществу, за пределами узкого ведомства, его работа почти теряет смысл. От чего и руки могут опуститься, кстати. Но бывают, конечно, ситуации, когда приходится обходиться без публикаций.

Множество открытий теро вер, численных вычислений, электроники и т.п. как раз результат конкуренции, в том числе между странами, и т.п. И параллельная работа над теми же задачами часто приводит к разным результатом, которые затем так или иначе узнают конкуренты.

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

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

[ozheredov]

Brizon в сообщении #1737242 писал(а):

циркл джеркин

А как надо, расскажите?
Упраздняем все учёные звания, и объявляем открытый для всех конкурс по решению ряда задач. И какой-нибудь в глаза не видевший учебника математики читоклоун, которому повезло с наворовавшимся папочкой, в перерыве между катками в escape from tarkov за час решает все эти задачи благодаря мощному компу и неограниченной возможности жечь токены. Читоклоуну выдают 1000000usd и пожизненный контракт с Nvidia с правом получать 10000usd в месяц, просто играя в escape from tarkov, а посвятивших всю свою жизнь изучению математики профессоров изгоняют из институтов мокрыми дурно пахнущими тряпками. Так?

[Aelteste]

Brizon в сообщении #1737242 писал(а):

циркл джеркинг,

Про это еще Крылов писал.

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

А как надо, расскажите?

Проблема в системе. Как мне кажется надо разделять образование и науку. Преподавательская деятельность должна оцениваться по своим критериям: победы в олимпиадах и конкурсах, средний балл по ГИА и т.д. и здесь должно быть полное финансирование государством, никаких там тебе платников, которых ты должен бояться отчислить за неуспеваемость, тотальный контроль за учебным процессом со стороны государства, в смысле за опозданиями, качеством подаваемого материала и т.д., соответственно и достойная зарплата. А научная деятельность должна быть большей частью на самообеспечении. Т.е. какой-то минимум оплачивает государство, грубо говоря за НИР со студентами на гос. предприятиях, а кому мало - ищите гранты, заказы от кампаний и проводите исследования, которые вам готовы оплатить. Ну и пусть хвалят там друг друга за выдуманную и никому не нужную ерунду, за которую никто ничего не платит. А кто занимается серьезной наукой, тому на нее дадут и оборудование, и деньги, и работу оплатят частные заказчики. Продвижение по карьерной лестнице должно учитывать ценность открытий и изобретений, А это больше не про ссылки друг на друга, а про то, сколько денег было выплачено за лицензию на патент. А то у многих туалеты оклеены патентами от которых пользы 0, зато звездность и ЧСВ от этого повышенные и добавка к зарплате, повышение по карьерной лестнице и прочие плюшки, а этих плюшек за симуляцию быть не должно, иначе они ее стимулируют. То же самое с публикациями, ценность статей тоже должна измерятся не просто индексом цитирования, т.к. это стимулирует как раз цирклджерк, Но признанием и оценкой результатов в научном сообществе. Например есть фуфломициновая статья важного гуся ни о чем. Если люди используют ее в своих работах и ссылаются на нее, то значит якобы признают ее результат. Надо сделать невыгодным ссылаться на нее, например сделать так, что они платили за это деньги на счет государства в определенный фонд, а если они липовую статью гуся разоблачают и на это разоблачение ссылаются тоже люди, которые тоже платят деньги за ссылки на разоблачение, то за это разоблачение платится премия разоблачителю. Т.е. необходимо сделать круговое цитирование невыгодным и дорогим, чтобы оно могло оправдываться только выгодами от практической пользы, принесенной статьями, и от индекса признания в научном сообществе, который выражается в деньгах от цитирования. Например цитирование стоит 2000- 5000 руб. И вся система находилась под контролем государства. Не каждый захочет рисковать и платить за ссылку на липовую статью, есть ведь тогда шанс потерять эти деньги в случае выявления циклджеркинга или разоблачения. Они так и останутся в фонде государства или уйдут разоблачителям или авторам других, более признанных статей. Или вернутся лишь частично им, т.е. можно в такой системе произвести тонкие настройки и модифицировать. Не человек оценивает признанность сообществом и важность результатов, а автоматизированная система в целом. И человеку невыгодно влиять на систему, создавать липу, т.к. затраты на такое влияние не оправдываются выгодами от него.

[Mihaylo]

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

Так?

Примерно. В этом и заключаются риски революции ИИ. В качестве примера я могу привести мой личный случай - разработка ПО сервера для мониторинга удалённых объектов. Результат получен в сжатые сроки, при этом я не умею делать подобное, нет бюджета для найма профильного разработчика. Теперь я, конечно, подковался, но это не главное. Главное, что компания получила продукт за две недели, расходуя ~1500 рублей в месяц на помощника (ИИ).

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

[Mihaylo]

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

[ozheredov]

Aelteste в сообщении #1737258 писал(а):

Про это еще Крылов писал.

Ага, "кукушка хвалит петуха, за то что хвалит он кукушку". А еще Крылов писал: "Свинья под дубом вековым наелась желудей до сыта, до отвала. Наевшись, выспалась под ним, и рылом подрывать у дуба корни стала... Невежда также в ослепленье бранит науки и ученье, и все ученые труды, не чувствуя, что он вкушает их плоды".

Mihaylo в сообщении #1737270 писал(а):

А так мы имеем возможность вносить необходимые изменения в ПО за пять минут, сделав пару промптов, это тоже очень сильный результат.

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

Mihaylo в сообщении #1737273 писал(а):

ИИ применил распределение Пуассона для построения модели. Я, конечно, знаком с математикой, но я совершенно не вникал. И дело не в том, что я ленивый или некомпетентный. Просто сказывается тотальная нехватка времени.

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

[mathpath]

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

Aelteste в сообщении #1737258 писал(а):

Совмещать эту деятельность - стремление благородное (я и сам пытался, и думаю что минимум две третьих форума тоже), но не всегда доступное.

Бесплатное ии доступно всем
И при определенных условиях оно способно творить чудеса

[Anton_Peplov]

Kuga в сообщении #1737490 писал(а):

а человек где тут в эту схему вписывается?

Кратко: никто пока не знает, как и куда вписывается человек. Возможности ИИ меняются слишком быстро, чтобы делать прогнозы. Десять лет назад ИИ не мог задачу из школьного задачника решить, а нынче, эвон, решил "проблему тысячелетия" (нашел нефизичное решение уравнений Навье-Стокса). Может быть, где-то тут рост и остановится. А может быть, пойдет дальше, и тогда вопрос, насколько дальше. В зависимости от этого и роль человека будет разной. Если ИИ останется примерно там, где он есть сейчас, то он будет соавтором человека. А если уйдет сильно дальше, то человек окажется исключительно в роли заказчика и потребителя математических результатов. Разумеется, останутся "спортсмены", которые из принципа все будут доказывать сами, но это будет повторение результатов, уже достигнутых ИИ. Повторяю, если он уйдет намного дальше, чем он есть сейчас.

Есть и такой нюанс. Доказательство устанавливает, что утверждение верно. Но его ценность не только в этом. Хорошее доказательство еще и объясняет, почему утверждение верно. То есть углубляет наше понимание математики. Поэтому важно научить ИИ не только доказывать теоремы, но и доказывать их понятным для человека способом. Полагаю, это вполне возможно.

[Brizon]

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

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

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

[SomePupil]

Прорыв в формальной верификации Alphaproof Code от Deepmind: ИИ-агентов научили систематически выделять в математических доказательствах Lean "узкие места" для независимой проверки экспертами-людьми.

В качестве демонстрации возможностей нового фреймворка с его помощью доказали безопасность широко используемого протокола Signal для обмена сообщениями в мессенджерах (Ватсап, Гугл-почта). Для этого сначала требования безопасности Signal перевели в формальные математические спецификации, каждая из которых прошла проверку экспертами-людьми. Затем агенты на базе Gemini Carbon выполнили доказательства, создав более шести миллионов строк кода на языке Lean.

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

P.S. I wonder, если применить технологию к доказательству Wiles ВТФ, какие участки выделят ИИ-агенты для дополнительной проверки людьми? Какие-нибудь кусочки коммутативной алгебры? Ключевые ходы доказательства знаменитой теоремы R=T? Многие специалисты выражали сомнения в существующих доказательствах Lean ВТФ, дескать, доказывать-то она (Lean) доказывает, только вот соответствуют ли её теоремы среди этих миллионов строк кода в точности соответствующим математическим утверждениям из доказательства? Применение таких технологий, как описано выше, должно избавить нас от подобных сомнений при формальной верификации "огромных" доказательств, ведь эксперты наглядно могут сопоставлять утверждения из "узких мест" (которые занимают значительно меньше места, чем миллионы строк общей кодовой базы) непосредственно с текстом в доказательстве.

[Sender]

SomePupil в сообщении #1738169 писал(а):

Многие специалисты выражали сомнения в существующих доказательствах Lean ВТФ, дескать, доказывать-то она (Lean) доказывает, только вот соответствуют ли её теоремы среди этих миллионов строк кода в точности соответствующим математическим утверждениям из доказательства?

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

[Ende]

Обсуждалось здесь: «Формальные доказательства с помощью моделей». Конкретно вопрос о том, соответствует ли формальное доказательство неформальному - на второй странице.