Комментарии 22
ну все равно крутой уровень у ИИ, конечно...Будущее уже здесь)
Интересно, а не был ли обучен этот ИИ на тех же задачах, которые ему подсунули впоследствии для решения?
Ну и перевод на формальный язык - хорошая фора, обдумать условия олимпиадной задачки и уложить в голове - это половина пути к решению :)
Вроде его обучали до выхода комплекта межнара этого года, так что все честно) Если же машина видела подобную задачу в процесссе обучения, это тоже честно, т.к у членов нац сборной (в России и в Китае точно) есть и тренера и особенная учебная программа (к олимпиаде), где наверное уж наиболее вероятные/интересные задачи давались к рассмотрению и ученикам.
Новость на уровне, ИИ в уме посчитал сколько будет 3746537 умножить на 5674392.
задачи были предварительно переведены на язык Lean людьми
для некоторых более 60 часов
Очень по описанию и цифрам напоминает идею языков типа prolog, где есть аксиомы, правила, цель. А уже интерпретатор языка пытается брутфорсом накомбинировать правила, чтоб дойти от аксиом до цели.
Только пролог был придуман в 1972 году и быстро был похоронен под предлогом, что комбинаций правил слишком много, современные процессоры не способны их всех перебрать. Теперь, видимо, способны.
В течении 1-4 лет ИИ будет как минимум на одном уровне с лучшими математиками мира.
Сначала мы будем поражаться решениям задач тысячелетия, найденными ИИ. Потом некоторое время общаться с ним на троих смогут только Гриша Перельман и Эндрю Уайлз. Но и это быстро закончится этапом: "папа, а с кем ты сейчас разговаривал"?... Ли Седоль не даст соврать.
И только осеннюю листву в парке по-прежнему будут мести кожаные мешки.
И программистами, походу, тоже...
Откуда такие прогнозы?
Довольно пристально слежу за развитием ИИ. Поскольку охватить весь невероятный прогресс не хватит никакого времени, я не пропускаю ролики на YouTube-канале 'AI Explained'.
задачи были предварительно переведены на язык Lean людьми
А вот это интересно. Означает ли это (поскольку не удалось заставить нейросеть сделать это автоматом), что эти люди применяли какие-то неявные знания о задачах, которыми нейросеть не обладает? Выглядит пока что как "Компьютер смог решить все задачи олимпиады ... после того, как программист написал программу, решающую все эти задачи".
Возможно, стоит подождать, пока нейросеть научат переводить задачи в этот язык Lean, скажем, на основе хотя бы этой выборки задач, которая переведена в lean уже сейчас?
Соберут нейросеть Lean-AI, которая будет подбирать перевод на язык Lean. Число комбинаций резко подскочит и соберут нейросеть-арбитра, чтобы отсеивать варианты от Lean-AI. Короче, надо строить еще 2 датацентра.
Нет, не после того как написал решение, а после того как написал условие задачи.
Формализовать из естественного языка -- это конечно тоже задача для ИИ и её решение тоже продвигается, но в конкретном случае фокус был на решении уже формализованной задачи.
Автор статьи упустил важную деталь. Демис Хассабис, глава DeepMind, написал в своём Твиттере, что скоро все эти передовые разработки появятся в моделях Gemini. Даже если это займёт год, хотя я думаю, что это произойдет до конца этого года, Gemini станет на порядки более полезным сервисом.
Мы давно лидируем в разработке таких нейросимволических систем, начиная с AlphaGo в 2016 году и до AlphaZero. Скоро все лучшее из AlphaProof и AlphaGeometry 2 появится в наших основных моделях #Gemini. Не пропустите!
Спасибо, об этом уже все писали
Ну так они видимо сейчас будут CVC/DreamCoder представлять хомякам (уже 3 года ждем).
Увы, у этих солверов на GPU IQ в районе 500 (в типичных тестах) )
И, ждем сравнений с CVC )
P.S. Я успел представить свою Ground Braking модификацию солверов аж в kaist, пока в Google пытались создать свой солвер (который вышел даже хуже, чем DreamCoder)
Я на 99% уверен, что тут был перебор или еще какой-то алгоритм поиска, но в качестве эвристики там использовалась нейросетка. Как в предыдущих работах DeepMind. Это, конечно, достижение. Это классный алгоритм. И применение нейросеток вот так: для сжатия огромного массива данных и выделения в нем паттернов - это очень полезно и интересно.
Но это совсем не тот ИИ, о котором думают обыватели и как его рисуют в медиа. Тут нет никакой логики, рассуждений и мышления. Программа лишь выполняла поиск в пространстве формальных утверждений. Тут нет никакого принципиального отличия от какого-нибудь метода отжига или генетического алгоритма.
Программа лишь выполняла поиск в пространстве формальных утверждений
Ну а разве это по сути не то, чем занимаются математики? Чем это отличается от формального доказательства, но выполненного человеком?
Люди опираются на абстрактное мышление и логику. Какой-то перебор вариантов и у людей, конечно, есть. Но он уровнем выше: попробуем свести задачу вот к такому классу, а если двойственную посмотреть, а какие там свойства у этих объектов доказанные были, а нельзя ли тут теорему Неймовича применить? Перебирается лишь направление идеи, а дальше идут рассуждения.
Именно это и есть человеческий разум и интеллект. Имено это фантасты и ученые называют "сильным ИИ". И этого пока нигде нет.
Это все - причинно-следственные связи. Или просто функция ).
Добавьте в тот же DreamCoder свои теории (или даже в CVC) - и поиск решения будет выполнятся с учетом этих теорий.
И, да, у них (DeepMind/DreamCoder) даже не эвристика, чтобы использовать оптимальный поиск (увы, гении ИИ).
Если просто тренировать нейросеть как допустимую и оптимальную эвристику - должно помочь.
ИИ от Google решает задачи на уровне серебряного медалиста Международной математической олимпиады