Comments 10
Значит, все сводилось к простому перебору, и проблема четырех красок вовсе не заслуживала названия хорошей проблемы
На сколько у меня сложилось впечатление из публикаций, решение для Навье-Стокса тоже свелось к подбору контрпримера?
Честно, не знаю, я доказательства от OpenAI не читал "но осуждаю"). Ждем реакции сообщества математиков - во-первых, подтверждения, что доказательство верное, во-вторых, разъяснение, что именно там нарыли агенты.
У четырёх красок компьютер проверял на редуцируемость около 1900 конкретных конфигураций по методу разрядки – это логически структурированная процедура, а не сплошной перебор раскрасок. В 2005 году Жорж Гонтье формально верифицировал всё доказательство в Coq, так что вопрос доверия к коду там закрыт. С Навье–Стоксом иначе: численно находят кандидата в особую точку решения, а доказательством это становится только после проверки интервальной арифметикой с гарантированными границами ошибки.
Все ИИ-открытия в математике объединяет одно, открытия по сути это перебор гипотез+верификатор. То есть LLM работает внутри заданного пространства представлений. Это позволяет улучшать нижние и верхние границы, находить точки опровержения и так далее.
Что это значит для математики? Если учёные пойдут по лёгкому пути, большая их часть превратится в поставщика промптов для LLM, и из учёных они превратятся в оптимизаторов, технических ассистентов науки.
А математику будут двигать такие гики как Перельман или Гротендик. Работающие не с известными паттернам, а меняя или иногда даже разрывая пространство представлений. Как Лобачевский с неевклидовой геометрией или Кантор с бесконечностями.
А я себе представляю по другому. На пример математик занимается некоторой проблемой. Он разбивает ее на несколько подпроблем. Он зовет к себе аспиранта и говороит: Петя, проверь, посмотри, что здесь можно сказать. И получает ответ через некоторое время. Чем здесь аспирант отличается от ИИ? В добавок, эта подпроблема может быть уже решена. Но у него нет в доступа к специалисту о этой конкретной проблеме. И все. Что ему желать?
А с ИИ все хорошо. Математик может грамотно (!!!) разделить задачу над подзадачи и спросить ИИ проверить,протестировать их. А самому заняться интересными с его точки зрения задачами.
Конечно не хорошо воровать и присваивать чужие идеи, исследования. Но это уже не относится к математике! Это человеческие отношения. Не более.
Кстати, у Станислава Лема есть повесть, "Осмотр на месте". Там перед тем, как что-нибудь открыть, нужно было обращаться в специальный институт, чтобы убедиться, что это не было открыто. Видимо к этому все и идет!
Разве решение вообще было бы возможно без промежуточного решения сделанного живыми математиками?
Получается они, эти математики, смогли бы сами без нейросетей сделать решение и для Навье — Стокса, чуть позже. А вот смогла бы OpenAI сделать открытие без них - вопросик, скорее всего нет.
Может случится, что и не смогли бы. Например: всякое решение задачи, это грубо говоря строка на языке математики. Ну там плюсы минусы, кванторы всякие. Эта строка имеет некоторую длинну. У задачи существуют разные решения. Выберем из этих решений самое короткое. Предположим что его длинна N. Если N маленькое, то они могут за время его найти. А если большое, ну типа 10 в 10 степени, то не факт, что они его найдут. И здесь компьютеры и ИИ имеют бесспорное преимущество. И было бы ошибкой не восользоваться компьютером или ИИ!
Правда возникает задача верификации. Но мне кажется над этим работают. Но и тут не без проблем.
Но они могут быть неполноценными, поскольку не дают никакого понимания.
Они могут быть некорректными и исходить из неправильных аксиом или триггерить какие-нибудь баги компилятора/солвера, однако цепочка понимания никуда не девается - у вас есть набор теорем, которые вполне реально записать в человекочитаемом виде. Оно конечно страшно для новичка, когда доказательство сводится к тексту а ля by linarith, grind, или вызов какой-нибудь иной тактики, но Lean (да наверняка и не только он) позволяют вывести конкретную цепочку для таких вызовов до самого низкого уровня. Так что данных для понимания доказательств предостаточно.
что без всяких компьютеров и LLM в математике уже давно имеются доказательства, которые вообще никто не понимает, потому что это выше сил человеческих:
это неправда. никто не проверял все части некоторых доказательств вручную, но не "не понимал" доказательства.
Проблема была, однако, не только в том, что проверить доказательство, выданное машиной, было нельзя без использования других машин
тоже неправда. распечатать граф и пораскрашивать вершины не сказать чтобы невозоможная задача, просто без роботов велик шанс ошибиться с выбором краски и проверять полторы тысячи графов - задача экстремально нудная.
Точнее, его работу пришлось потом долго разбирать на протяжение нескольких лет различным авторам, чтобы понять, так сказать, "всю глубину наших глубин".
Не совсем так. Советская школа математики часто пренебрегает описаниями промежуточных шагов для некоторых операций, считая что они уж совершенно точно доказаны в каком-нибудь малоизвестном издании про которое никто уже не вспомнит и вспоминать это не стоит. Поэтому Гриша доказал общую форму теперь уже теоремы Пуанкаре, а остальные авторы заполняли пробелы-цепочки, чтобы можно было проследить полную последовательность. С SAT-солверами эта проблема как раз и исчезает, потому что неизбежно понадобится доказать всю цепочку лемм и поэтому иишные пруфы лучше человеческих в данной категории. Но есть другая проблема - велик шанс, что шаги выбранные ИИ не оптимальные. Уже были примеры, как геометрические построения людей для нахождения какого-нибудь угла или площади занимали едва ли не в 10 раз меньше шагов чем аналогичные построения у ИИ.
Уже были примеры, как геометрические построения людей для нахождения какого-нибудь угла или площади занимали едва ли не в 10 раз меньше шагов чем аналогичные построения у ИИ.
И в сущности это не так и страшно. Про гипотезу 4х красок: сначала было много вариантов, затем при исследовании доказательства список вариантов сократился.
Более сложные построения делают понимание доказательств сложнее для людей. Учитывая, что половина статьи строится на том "как сложно понимать" этот аргумент как раз получается не в пользу ИИ, но да, с точки зрения науки результат он и в Африке результат, красоту можно и позднее навести. Так было и с четырьмя красками или с пруфом Перельмана и с прочими задачами, которыми полнится условный Polymath.
Чем плохи доказательства от ИИ с точки зрения математиков?