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

[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 писал(а):

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

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