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

[Ghost_of_past]

(Оффтоп)

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

Это политика всего бигтеха (как минимум). Любое не прошедшее 50 этапов согласования высказывание должно помечаться как личное мнение сотрудника*.
[*] это моё личное мнение, которое может отличаться от официальной позиции компании

Не только бигтеха и даже не только коммерческого сектора. У меня и в университете нельзя давать журналистам/блогерам ответы на вопросы с пометкой, что являешься сотрудником университета, без согласования с пресс-службой университета.

[MoonWatcher]

Цитата:

Долго ждать не пришлось: OpenAI выложили результаты, полученные моделью Astra (официально подтвердили название). Блогпост называется «Десять достижений в математике и теоретической информатике»

Мне трудно осознать всю сложность этих задач. Я не то что математик, у меня диплома-то даже нет 😀 и я не вижу разницы, скажем, между 3-м и 10-м результатами.

Поэтому я попросил GPT-5.6 Sol Pro и Fable 5 Max (чтоб не было позитивного биаса на OpenAI) классифицировать их, используя систему критериев задач в бенчмарке OpenMath от EpochAI:

🟢 «Значимый результат» (Solid Result): Сильный исследователь в данной области был бы рад, если бы его среднестатистическая работа решала задачи такого уровня. Тем не менее, за пределами узкой специализации эта проблема вряд ли вызвала бы большой резонанс.
🟡 «Крупное достижение» (Major Advance): Среднестатистический специалист, работающий в широкой области математики (в масштабах теории чисел или теории графов), обратил бы на это внимание и, скорее всего, нашел бы время, чтобы вникнуть хотя бы в общую суть решения.
🔴 «Прорыв» (Breakthrough): Среднестатистический математик захотел бы узнать об этом результате, даже если он выходит за рамки его специализации. Такая работа стала бы кандидатом на звание одного из лучших результатов года во всей математике.

Обе модели — и Fable, и Sol — сошлись во мнении, что результат №3 — это «Прорыв» (что объясняет, почему сотрудник OpenAI из всех выделяет именно его в своём твите).

Они также согласны, что как минимум 7 решений из 10 относятся к категории «Крупное достижение».

Что еще интересно, в официальных критериях EpochAI сказано следующее:
«Когда для задачи подходили сразу несколько уровней оценки, мы склонялись к более консервативному варианту. Было бы неприятно понижать статус задачи уже после того, как она решена, в то время как мы всегда можем подчеркнуть любые неожиданно интересные элементы в самом решении».

И Fable 5 считает, что как минимум три результата находятся на грани «Прорыва» (№1, №4 и №9).

Все решения проверены в Lean — языке программирования для доказательства теорем. Если решение компилируется без ошибок, то оно либо правильное, либо есть баг в самом ядре (такое тоже бывало, но маловероятно, что все 10 результатов — результат бага проверки).

Суммарно на решение 10 задач потратили ~$2000 по API-ценам Sol (то есть скорее всего будет в 2 раза больше)

[worm2]

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

Суммарно на решение 10 задач потратили ~$2000 по API-ценам Sol (то есть скорее всего будет в 2 раза больше)

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

[MoonWatcher]

worm2
А как можно посчитать нечестно? Учет затраченных на решение задачи токенов ведется - остается только умножить их количество на расценки.

[worm2]

MoonWatcher
Ну, может быть, они на одну задачу пробовали сто подходов, один из них привёл к результату и обошёлся в 200 долларов, а 99 других к результату не привели, но токены сжигали исправно.
Может быть, они тысячу задач пробовали, получилось десять, и каждая решённая обошлась в 200 долларов, а про остальные (нерешённые) ничего не написали.
Не, по-любому, дёшево получилось, я не спорю, но настолько ли дёшево?

[MoonWatcher]

worm2 в сообщении #1729749 писал(а):

Ну, может быть, они на одну задачу пробовали сто подходов, один из них привёл к результату и обошёлся в 200 долларов, а 99 других к результату не привели, но токены сжигали исправно.
Может быть, они тысячу задач пробовали, получилось десять, и каждая решённая обошлась в 200 долларов, а про остальные (нерешённые) ничего не написали.

Это был бы откровенный мухлеж. Уверен, что речь идет о стоимости ВСЕХ затраченных токенов. Собственно, OpenAI у себя в блоге так и пишет (автоперевод):

Цитата:

Общее количество токенов, необходимых для нахождения решений этих задач, составило бы примерно 2000 долларов США по курсам Sol API.

[realeugene]

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

Я подозреваю, что почти любой человек, если ему объяснить известный Эйнштейну диффгем и посадить в лифт, вывести ОТО не сможет. Значит Эйнштейн умел что-то еще, помимо знания диффгема и опыта поездок в лифте.

Эйнштейн очевидно решал проблему несовместимости ньютоновской гравитации с СТО, причём, плотно сотрудничая с другими физиками и математиками, в частности, переписываясь с Гильбертом, который вывел те же уравнения как пишут другим методом и чуть позже, но до публикации Эйнштейна. Уравнения Эйнштейна иногда называются уравнениями Эйнштейна-Гильберта. Разработка ОТО заняла больше 10 лет. Если бы LLM вывела ОТО на основании знаний физики и диффгеометрии того времени за пару часов, это бы означало, что она как физик-теоретик гораздо-гораздо-гораздо сильнее Эйнштейна.

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

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

Обе модели — и Fable, и Sol — сошлись во мнении, что результат №3 — это «Прорыв» (что объясняет, почему сотрудник OpenAI из всех выделяет именно его в своём твите
).

Тоже не могу оценить значимость для математики, но могу оценить объём доказательства: формальное доказательство на языке Lean лежит на гитхабе. Формальное доказательство этого третьего результата на языке Lean состоит из 1.4 миллиона символов, 34 тысячи строк или 1061 теоремы. Впечатляет.

[ozheredov]

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

Если бы LLM вывела ОТО на основании знаний физики и диффгеометрии того времени за пару часов, это бы означало, что она как физик-теоретик гораздо-гораздо-гораздо сильнее Эйнштейна.

Только Эйнштейн сам допетрил, что нужно выводить. А LLM бы подсказали (да ещё и замели 100500 неудачных попыток вывода под ковёр)

[Sender]

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

Формальное доказательство этого третьего результата на языке Lean состоит из 1.4 миллиона символов, 34 тысячи строк или 1061 теоремы. Впечатляет.

Б. Паскаль писал(а):

Это письмо получилось таким длинным потому, что у меня не было времени написать его короче

[realeugene]

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

Только Эйнштейн сам допетрил, что нужно выводить.

Думаю, то что ньютоновская гравитация не стыкуется с СТО было всем очевидно.

[dsge]

https://www.seangoedecke.com/llms-reward-expertise/

Цитата:

Tao’s messages are very short and to-the-point. He doesn’t respond point-by-point to the model, just to the gist
The model outputs are much more concise than when I try and talk to GPT-5.6 Sol about mathematics. By signalling expertise, Tao shunts the model into “talking-to-mathematicians” mode, not “explaining-to-amateurs” mode
Tao pushes back when the model’s responses look wrong, but he doesn’t directly contradict; instead, he says things like “this looks more complex than I was hoping for”
Tao makes several leaps and suggestions himself. He almost never takes the model’s advice about where to go next

Для невежд, планирующих доказывать проблемы тысячелетий с помощью LLMs. Ну и для тех кто полагает , что LLMs сами решат все математические проблемы.
Надо также добавить, что OpenAI, скорее всего, хорошо платит Тао за "экспертизу" и обеспечитает его самой последней молелью бесплатно, без ограничений на колличество токенов и запросов.

[Anton_Peplov]

(Оффтоп)

У меня английский не беглый, так что скормил этот текст гугл-переводчику. Умиляет его манера переводить LLMs как "магистры права".

[dsge]

Anton_Peplov в сообщении #1731020 писал(а):

Умиляет его манера переводить LLMs как "магистры права".

Кстати, хороший пример, подтверждающий неспособность этих моделей к логическому мышлению, reasoning. LLMs - это множественное число моделей. Магистры права - это уже будет LL.M - Master of Laws. Двойное L в латыне означает тоже множественное число, только в данном случае законов - Laws.
Так что модель не знает даже как она зовется.

[mihaild]

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

Надо также добавить, что OpenAI, скорее всего, хорошо платит Тао за "экспертизу"

А в мире есть хоть один человек (кроме меня и Вас), которому OpenAI не платит?

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

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

Непонятно откуда это взято. Более того, обычно очень стараются ничего конкретного про не запущенные модели не показывать - конкуренты не дремлют.

Какие у Вас основания считать, что переписка по ссылке Тао не сгенерирована наиболее очевидным образом - Тао пошел, заплатил (или воспользовался оплаченной, например, институтом подпиской) и написал все сообщения той же модели, которой мог бы написать (если бы обладал квалификацией Тао в задании вопросов) и любой другой человек?

В целом Вы явно совершаете ошибку подтверждения - тщательно выбираете свидетельства про ограничения LLM, и игнорируете обратные.

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

Двойное L в латыне означает тоже множественное число, только в данном случае законов - Laws.

Легко находятся примеры, где точку не ставят. А если сказать, что LLM допустимо читать как "магистр права", то с s получится множественное число не хуже чем для моделей.

Но в целом я не понимаю, как google translate ухитряется в 2026 году добиться такого результата.

google translate писал(а):

Сегодня каждый может написать более-менее приличный CSS, поручив эту задачу магистру права (LLM).

Gemini 3.5 Flash-Lite писал(а):

Сегодня каждый может написать вполне сносный CSS, делегировав задачу LLM.

Gemini 3.7 Flash писал(а):

Сегодня каждый может написать более-менее сносный CSS, просто перепоручив задачу большой языковой модели (LLM).

[ozheredov]

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

в целом я не понимаю

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

Надо попробовать перевести то же самое в Квен и Дипсик