OpenAI решила гипотезу Unique Games, над которой математики бились десятилетиями
The Mathocalypse
Вчера OpenAI выложила 372 доказательства давних открытых задач, включая гипотезу Unique Games, L=BPL и прорыв в умножении матриц. Формальные сертификаты Lean есть, но ни один человек пока не разобрал эти доказательства. Скотт Ааронсон сравнивает происходящее с «Mathocalypse» и обсуждает, как сообщество будет догонять ИИ.
Ощущение, будто это писал человек под психоделиками. Столько всего неясного и бессмысленного. Куча упоминаний предыдущих работ без обсуждения, почему их можно использовать вопреки результатам о невозможности.
- ks2048
> Такое ощущение, что это писал кто-то под психоделиками. Столько всего непонятного и бессмысленного. Куча упоминаний предыдущих работ без обсуждения того, почему их можно использовать, несмотря на результаты о невозможности.
> В общем, статья настолько ужасно написана, что её невозможно читать без помощи ИИ.
Это интересно, и я не видел такого во всех материалах об этом событии.
Звучит ужасно — продираться через это, как пытаться понять чужой запутанный код, который всё же выдаёт правильный результат.
- nostrademons
Как побочное замечание: по первому предложению можно понять, что это написал не ИИ:
> мамочка, я слышал, тебя зажарили! Я слышал, что робот решил математическую задачу, над которой ты работала всю свою карьеру! УФ!
Мой 8-летний сын говорит точно так же. Я вполне могу представить, как он говорит это за обеденным столом.
Я спросил у ChatGPT: «Представь, что ты сегодня 8-9-летний ребёнок. Как бы ты оскорбил свою маму из-за того, что её работу заменил ИИ?», и он выдал такие варианты:
> «Мам, ИИ забрал твою работу, потому что, видимо, даже роботы такие: „Ага… мы можем сделать это лучше.“»
> «Мам, поздравляю! Тебя заменил компьютер. Даже у Siri теперь есть работа, а у тебя нет!»
> «Мам, ИИ забрал твою работу? Чёрт. Видимо, даже робот посмотрел на твою работу и сказал: „Я справлюсь.“»
> «Не волнуйся, мам. Ты всё ещё можешь быть полезной… например, научить ИИ готовить мне обед.»
Все они отдают каким-то миллениальским духом, не говоря уже о том, что это довольно неуклюжие и механические подколы. Доверьтесь детям и языковому дрейфу — лучший детектор ИИ.
- ajjenkins
Строчка про «понимание пришельцев» напоминает мне рассказ Теда Чана «Эволюция человеческой науки» (2000).
Очень рекомендую прочитать. Весьма пророческая вещь для текста, написанного 26 лет назад.
https://gwern.net/doc/fiction/science-fiction/2000-chiang.pd...
- an0malous
> Но также похоже, что ни один человек пока не понял почти ни одного из этих доказательств.
Кто-нибудь проверил хоть одно доказательство, созданное OpenAI, или все просто предполагают, что оно верно, потому что код на Lean проходит проверку? А что, если код на Lean просто сформулирован неправильно?
- softwaredoug
Разве не существует десятков доказательств теоремы Пифагора? Цель не просто «доказать», а создать что-то хорошо написанное и интуитивно понятное среднему практику. И, углубляя понимание, мы можем задавать лучшие вопросы.
- dualvariable
Вдобавок к тем проблемам, которые подняла жена в этой истории, вот мета-анализ результата по Навье-Стоксу, который ставит под сомнение все эти решения:
https://arxiv.org/abs/2610.08144
> Автоформализация всё чаще используется для проверки математических текстов, в том числе сгенерированных ИИ, как в анонсированном OpenAI доказательстве взрыва решений уравнений Навье-Стокса. В этом процессе система ИИ переводит текст с естественного языка (NL) на формальный язык, такой как Lean. После этого перевод аргумента на формальный язык можно легко проверить механически. Цель этой статьи — показать, почему этот процесс может не давать никакой уверенности в исходном аргументе на NL из-за различных трудностей при семантически точном переводе. В частности, мы подчёркиваем, что проблема разрешения неоднозначностей в математическом тексте на NL, необходимая для семантически точного перевода, находится произвольно высоко в иерархии сложности разрешимости (SCI) / арифметической иерархии (SCI = ∞). Таким образом, неформально, обеспечение семантически точной автоформализации ИИ сложнее любой вычислительной задачи, включая проблему остановки (у которой SCI = 1). Чтобы продемонстрировать эффект этого результата, мы приводим несколько примеров практических ошибок ИИ при переводе утверждений и доказательств с NL на Lean, что приводит к несоответствиям между доказательствами на NL и их Lean-«верификациями». Среди них Op […]
- furyofantares
То, что это просто возможности модели, а не рои агентов, меня ошеломляет. Сколько времени пройдёт, прежде чем у нас появится доступ к таким возможностям? Сколько времени до того, как мы сможем запустить нечто подобное локально?
И что, чёрт возьми, будет к тому моменту у передовых лабораторий?
Может, я преувеличиваю, мне нужно сначала прийти в себя, прежде чем я смогу это осмыслить.
- olalonde
Было бы довольно забавно, если бы агенты на самом деле просто нашли баг в Lean, использовали его для всех этих доказательств, а у людей-ревьюеров ещё не было достаточно времени, чтобы его заметить.