dxdt.ru: занимательный интернет-журнал

В работе LLM (Large Language Models) используются токены, а не слова, как слова. То есть, процесс можно сравнить с изучением письменности, но без изучения языка. Для использования компьютерами, буквы, как символы, кодируются значениями байтов – это вполне привычная система.

Так, если взять ASCII, то символу (букве) L соответствует шестнадцатеричный индекс 0x4C. Тут есть множество философских моментов: во-первых, натуральное число 0x4C – это число, а не буква, так что, в большинстве компьютерных применений, 0x4C – вовсе не имеет отношения к букве L; во-вторых, для того, чтобы число указало на букву, всегда требуется внешняя структура – ASCII, в данном случае, – и система соглашений, определяющая, как минимум, метаязык и алфавит; в-третьих, компьютер, на котором работает LLM, “читает” именно байты, а не воспринимает буквы как буквы, то есть, как элементы, переключающие неизвестную компьютеру структуру, хоть бы это была и только таблица ASCII (тем более, что современные тексты используют Unicode – другое кодирование).

Числа, записанные в байтах, могут “быть буквами”, но могут и не быть. Буквы могут “быть звуками”, а могут и не быть. Хитрость в том, что сама по себе, без дополнительных соглашений, буква L никакой звук не обозначает, а обозначает, скажем, “длину стороны треугольника”, однако L может использоваться в записи звуков. (Да, речь только про фонетическое письмо.) Тут не так важно то, насколько фонетика вообще определяет язык, как то, что превращения букв при записи слов языка определяются, в том числе, превращениями звуков. Так что именно этот момент, – поднятие фонетической структуры из разных записей, – позволяет изучать происхождение и родство современных языков. Это максимально далеко и от ASCII, и от Unicode, самих по себе.

Слово “яблоко” не является яблоком, но “слово” является словом (или тоже нет?), однако ещё дальше от смысловых конструкций ASCII- или Unicode-таблицы, преобразованные в очередные наборы чисел. Всё это не мешает попыткам переносить следы способов записи смысловых конструкций, оставшиеся в корпусе обучающих текстов, в новый поток индексов (байтов), генерируемый LLM. И эти индексы пользователю предлагается считать буквами, потому что компьютером же можно преобразовать коды в изображения символов, которые пользователь начнёт читать как текст. “Большая” же идея, естественно, в предположении о том, что автоматический компьютерный перебор может воссоздать ту самую, внешнюю структуру.

Известно, что идея LLM выросла из методов атрибуции текстов: разным авторам свойственны разные словари (конкордансы) и стили комбинирования слов, связанные с привычной записью частей речи; если на основе текстов с известным авторством построить достаточно длинные “вероятностные цепочки” слов и их частей (последнее – необходимо для учёта морфологических особенностей), то можно будет строить предположения об авторстве для других текстов, сравнивая их цепочки с цепочками из базовой выборки. Это можно делать даже вручную, но компьютерная обработка несравнимо эффективнее. Переход к LLM начинается со следующего шага, на котором уже слова из словаря выбираются так, чтобы подходить к цепочкам, построенным на большой выборке текстов. Свидетельствует ли успешное исполнение сверхмощным компьютером перевернутого алгоритма атрибуции о каком-то “универсальном интеллекте”? Вряд ли.

Воскресное чтение манускриптов. Сегодня нам попалась строка из первой книги “Илиады” (1.69), где речь идёт о прорицателе Калхасе. Вот подтверждающий скриншот из манускрипта Venetus A:

Строка, вторая на скриншоте, в современной типографике выглядит так: “Κάλχας Θεστορίδης οἰωνοπόλων ὄχ᾽ ἄριστος”, то есть, “Калхас Фесторид – “птицевед” наилучший”. Фесторид, с “Ф” – это в русской традиции, а так-то можно прочитать и “Тэсторидис”, без мощного “th-фронтинга”, – выйдет больше похоже на греческую фамилию. “Птицевед” – это довольно условно: Калхас наблюдает птиц, как и уточняется в комментарии между строками (буквально: ὀρνεοσκόπων), однако он не орнитолог, а птицегадатель. Считается, что прорицатели, наряду с другими явлениями окружающей действительности, использовали наблюдение за полётом птиц для получения предмета толкования.

Что там за птиц видели гомеровские прорицатели, были ли это орнитологические объекты или не совсем орнитологические – точно сказать сложно, особенно, на фоне “бледных собак”, “тёмно-винного моря” и прочих “пурпурных овец”: может, прорицатели смотрели прямо в варп, а уже упрощённое описание увиденного превращалось в сведения про полёт и крики птиц (не только про птиц, конечно). А может – нет. Однако прорицатели, как известно из описаний, сначала выстраивали некоторые ограничения – определяли место, способ наблюдения, ставили шатёр, размечали направления, ещё какие-то подготовительные меры принимали, – и только потом, но тоже по заранее заданному алгоритму, выполняли наблюдение, интерпретируя его результат.

Наблюдению предшествовала настройка, которая и позволяла получить искомые сведения, иначе недоступные. То есть, тщательная настройка некоторого большего пространства таким образом, чтобы в результате измерения (наблюдения) с максимальной вероятностью получить полезный ответ из, казалось бы, случайных событий. Вообще, это логика применения гипотетического квантового компьютера: там тоже сначала выстраивается некоторая сложная машина, записывающая состояния так, чтобы соответствующие “вероятности”, которые полностью не вкладываются в классический кусочек мира, “интерферировали” (см. квантовое преобразование Фурье, например), увеличивая вероятность наблюдения полезного результата. Тогда интерпретация с птицами становится вопросом используемого набора метафор.

Как понять, что факторизация числа 15 не может ничего говорить о реализации квантового алгоритма Шора? Понять это несложно: один из делителей числа 15 должен быть меньше 4 (потому что 4^2 == 16), единица не рассматривается по условиям задачи, и это не 2 (потому что только нечётные подходят). Так что любой процесс поиска, каким бы аналоговым он ни был, если вообще сходится, то неизбежно попадёт в 3, что и будет верным ответом.

Заметьте, что ещё и 5 = 3 + 2, а простых чисел, меньших 15, только шесть: поэтому, учитывая, что умножение здесь коммутативно (это очень важно для квантовых алгоритмов), число 2 отбрасывается, а схема поиска расщепляется на пары, то, в самом худшем случае, вероятность, что аналоговый аппарат, состояния которого переключаются по возможным узлам дерева, промахнётся – меньше трети. (На практике, ещё раз, для промахов там просто нет места.)

Недавняя записка про оптимизацию циклов и микроконтроллеры иллюстрирует весьма важный момент, связанный с пониманием алгоритмов, записи алгоритмов и реализаций этих алгоритмов. Не менее рельефный пример в этом же направлении касается базовых логических операций и понимания записи формул. Речь про вопрос из области логики, логических выражений: является ли P и ¬¬P – одним и тем же? Даже разработчики-программисты нередко говорят, что “да, является”.

Знак “¬” – это логическое отрицание, проще говоря – “не”, или “!”, как будет во многих привычных языках. То есть, казалось бы, тут, во второй части, написано, что “не-не-P”, а тогда, если P имеет значение TRUE, то “не-не-P” тоже TRUE; то же верно и для P == FALSE. Понятное двойное отрицание, поэтому, что P, что ¬¬P – разницы нет: одно и то же. Это, впрочем, не совсем так.

Использование дополнительной “закорючки” (“¬”) позволило реализовать два способа записи, которые точно отличаются. Как способ записи, как “формула”, “P” и “¬¬P” – сильно разные вещи. Посудите сами: во втором случае на два “знака-закорючки” больше; кроме того – для выполнения “сокращения” нужно ввести дополнительное правило, по которому двойное отрицание вообще схлопывается, а чтобы это правило сработало, потребуется его внести “в набор допустимых операций” и применить, то есть, продумать и оптимизировать, даже если не сравнивать именно две записи. Так что “¬¬P” приносит с собой много разного, отсутствующего в “P”.

Понятно, что тут очень многие соглашения вынесены за скобки, но, тем не менее, это хороший пример базовых свойств процесса оптимизации. Да, компилятор мог бы заменить ¬¬P на P. Почти что то же самое компилятор и проделывает, когда заменяет запись цикла, тело которого не вносит изменений в результаты работы фрагмента кода, на простое присваивание:

b = 14; 
for(a = 0; a < 8; a++){ 
 b = b + a;
} 

заменяется на эквивалентное

b = 42;

(или это не эквивалентная замена?)

Вообще, запись алгоритма, содержащая определение цикла, описывает повтор неких операторов/команд, но не определяет, как этот повтор должен реализовываться на оборудовании. В принципе, тело цикла можно прямо выписать в качестве повторений команд, это известный приём оптимизации, он так и называется - "развернуть циклы". Очень часто, будучи применённым к программе на языке высокого уровня (ЯВУ), приём даёт заметный прирост производительности. Почему? Потому что исчезли накладные вычислительные расходы. При обычной обработке представления цикла на ЯВУ - появляются необходимые машинные команды, соответствующие "записи" цикла, а процессор вынужден их исполнять. Команд может оказаться неожиданно много: например, потребуется сложная обвязка для реализации обработки переменной цикла.

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

Немного технических деталей про протокол Диффи-Хеллмана в практике интернет-коммуникаций, почему ключи остаются в трафике, и немного про симметричные шифры.

Протокол Диффи-Хеллмана (DH) подразумевает, что каждая из сторон вычисляет свой секрет, потом на основе этого секрета вычисляет собственный открытый параметр (назовём пару этих параметров A и B), передаваемый по открытому же каналу. После того, как сторонам удалось обменяться открытыми параметрами, они могут определить уже общий симметричный секрет, на основе которого вычисляется секретный ключ (чаще – ключи) для симметричного шифра. Так вот, каждый из параметров A и B содержит полную информацию, необходимую для вычисления общего секрета (пояснение, 31/08/24: речь тут про вычисление по записи трафика DH). Это так по определению протокола, иначе сторонам не удалось бы получить одинаковый секрет. Другое дело, что извлечь эту информацию, исходя из известных алгоритмов, вычислительно трудно (но возможно). В частности, не было бы предмета для постквантовой криптографии, если бы ключи “классических” реализаций DH не восстанавливались бы полностью из записи трафика. Так что ключ есть в трафике, а не “только на клиенте”. Это всё известно специалистам, а DH в криптографии и не позиционируется как “ключ только на клиенте”, чтобы это ни значило.

Заметьте, что на практике, если конкретная реализация криптосистемы уязвима, то открытые параметры DH (A, B) могут предоставлять информацию о том, как оптимизировать поиск нужного секрета – это обычный приём. “Обратной задачей DH” называют задачу определения исходного секрета по открытому параметру (А или B). Однако вовсе не обязательно уметь решать обратную задачу быстро и универсальным образом. Можно ограничиться прямой задачей: при знании исходного пользовательского секрета решение этой задачи – быстрое по определению, это важный математический момент; специально подобранные параметры и/или дефектный датчик случайных чисел могут свести перебор к минимуму, если атакующей стороне известен другой секрет или параметр, который задаёт бэкдор (намеренно созданную уязвимость). Соответственно, оптимизированный перебор проводится до тех пор, пока подбираемое значение не совпадёт с перехваченным открытым параметром – в этом полезная роль этого параметра, так как подбирать ключ симметричного шифра, обычно, посложнее.

Ситуация с симметричными шифрами, впрочем, тоже не лишена особенностей. Дело в том, что на практике нетрудно предсказать значение открытого текста, соответствующего перехваченному в трафике зашифрованному сообщению. Это вообще самая старая из минимально содержательных атак на практические криптосистемы, известная задолго до появления интернетов, однако в интернетах обретшая новые черты: нетрудно предсказать, что содержится в начальных байтах HTTP-запроса GET, отправленного браузером через TLS-соединение к веб-серверу под известным именем. (И уж тем более нетрудно определить, для того же TLS, значение индекса в симметричной криптосистеме, работающей в режиме счётчика.) Это означает, что, формально, в трафике есть и следы ключей симметричного шифра. Другое дело, что преобразование, соответствующее зашифрованию симметричным шифром, во-первых, практически одинаково работает в обе стороны (зашифрование/расшифрование), то есть, никто и не полагался на сложность обратного преобразования как элемент обеспечения стойкости; во-вторых, с точки зрения криптоанализа симметричного шифра, секретный ключ входит в состав выполняемого преобразования. Тем не менее, для симметричных шифров тоже известны различные подходы, позволяющие устроить “вычислительный бэкдор“.

Воскресное чтение манускриптов. И кусочков папирусов. Папирус P. Oxy. Hels. 2 (справа), а точнее – та его часть, которая доступна онлайн в виде фотографии, – представляет собой узкий вертикальный кусочек, содержащий окончания самых первых строк “Илиады” (1.1-22). Фрагменты слов на папирусе вполне можно прочитать и даже сравнить с едва ли не основным источником текста “Илиады” – с манускриптом Venetus A.

Venetus A датируют десятым веком (н.э.), хоть достоверно он “выявлен в источниках” только в 15 веке. Упомянутый же папирус – относится ко второму веку (тоже н.э.). Получается, что между данными источниками около восьми сотен лет. Немало. Начертания букв сильно отличаются. Кроме того, на папирусе совсем нет знаков пунктуации, пробелов и диакритических знаков. Вообще, при ближайшем рассмотрении, отсутствие дополнительных знаков представляется очень странным – экономия места не так велика, как необходимость перечитывать один и тот же фрагмент нараспев (для греческого), чтобы понять, что же тут написано. Но, как минимум, слова с кусочка папируса неплохо сходятся с текстом Venetus A.

На манускрипте между строками записаны комментарии к тексту, но и на папирусе межстрочный интервал более или менее постоянный, это позволяет маcштабировать изображения таким образом, что фрагмент текста папируса сходится с Venetus A построчно.

Например, на скриншоте ниже фрагменты папируса и манускрипта объединены так, что можно сравнить записи построчно. Это строки с первой (не уместилась начальная Μ на Venetus A) по седьмую. Конечно, слова могли отличаться, зато на папирусе β выглядит почти как в современных шрифтах, а вот буква β манускрипта больше похожа на рукописную русскую “и” – см. пятую строку папируса, часть слова βουλή (“замысел, воля”).

Строки в конце кусочка папируса сходятся с Venetus A ещё лучше – см. следующий скриншот.

Здесь кусочек папируса тоже положен рядом (справа). Однако, в этих строках не только Ἀχαιοὶ (“ахейцы”) присутствует на папирусе целиком (четвертая строка на скриншоте), но и если выровнять масштаб по межстрочному интервалу и сдвинуть папирус так, чтобы πάντα[ς] из второй строки фрагмента (на скриншоте) наложилась на πάντας (“всех”) Venetus A, то (ωνα) папируса совместится с (ωνα) в слове Ἀπόλλωνα (“Аполлона”) из текста Venetus A (предпоследняя строка на скриншоте), что хоть и понятно почему, но всё равно особенно занятно.

В современной типографике для древнегреческих текстов вопросительному знаку (“?”) графически соответствует точка с запятой (“;” – как и в новогреческом, где, формально, знак только так выглядит). В старых записях “знаков вопроса” не было. Пунктуация вообще появилась не сразу, а в старых текстах слова бывают записаны даже без пробелов.

Воскресное чтение манускриптов. Сегодня посмотрим на скриншот из манускрипта, известного как Clarke 39 (Codex Oxoniensis Clarkianus 39) – это записи сочинений Платона, на древнегреческом, конечно. Манускрипт датируют 895 годом, и там встречаются неожиданные варианты “знаков вопроса”. Фрагмент ниже (22r) относится к диалогу Платона “Критон”; уже это может показаться странным, но, в данном случае, не важно: речь пойдёт о более странных вещах – о пунктуации в средневековых манускриптах, поэтому в смысл диалога Платона не станем вдаваться.

Тут уже в первой строке фрагмента нетрудно найти знак, неотличимый от точки с запятой, что является большой редкостью для манускрипта девятого века н.э. Дальше – хорошо видны более экзотические варианты: двоеточие над “запятой”. На следующем скриншоте некоторые из них дополнительно отмечены зелёными стрелками.

В современной типографике текст между стрелками выглядит так: “τί φῄς; ταῦτα οὐχί καλῶς λέγεται;” (“Что думаешь? Это хорошо ли говорится?” – тут “точка с запятой” является вопросительным знаком).

Естественно, считается, что “запятая” тут – это вовсе не запятая, а указание на повышение тона, соответствующее вопросительной интонации, то есть, что-то вроде изогнутой стрелки. Это начертание могло послужить основой для современного знака “?”. Даже в этом манускрипте отдельный вопросительный знак используется крайне редко, далеко не во всех случаях вопросительных предложений. В древнегреческом языке вопрос можно построить при помощи специальных слов и с использованием диакритических знаков, но в неясных, – по мнению редактора, – случаях потребовалось отдельное уточнение (и оно иногда отличается от современного варианта текста). Две точки в этой записи служат для разделения высказываний участников диалога, для разделения предложений, а одна “верхняя” или “средняя” (не ясно) точка – может обозначать и окончание предложения, и паузу, так что вот эта точка тут больше и похожа на запятую, в современном понимании. Поэтому знак, указывающий на повышение тона, может быть приписан снизу как к одной точке, так и к двум.

Да, возможное отсутствие знаков препинания в исходном тексте сразу наводит на аналогию с современной перепиской, – допустим, – в мессенджерах на русском: “привет Сократ что делаешь”, “Здоров, Критон! Да вот, сижу тут, заточили меня, но есть некоторые свежие мысли” (Сократ почему-то использует знаки препинания, даже восклицательный знак, странно). Всё же, вряд ли сотрудник скриптория расшифровывал, размечая только что разработанными пунктуационными знаками, дамп базы древнего централизованного мессенждера: более распространённая точка зрения гласит, что сотрудник скриптория переписывал с папирусов и других манускриптов.

Посмотрим на увеличенный фрагмент.

Тут встречаются и многоуровневые “точки с запятой”, и простые “двоеточия”, так что всё сходится.

Вернёмся, впрочем, к первому фрагменту скриншота.

Если приглядеться, то там над первой “точкой с запятой” виден некий знак, похожий на проценты. Что он означает?

Это редакторский знак. Дело в том, что тут пропущен кусок текста, так что вопросительный знак (“;”) вообще оказался перенесён – он должен быть через восемь слов, но тоже после “δ᾽ οὔ” (как и на скриншоте), а недостающий фрагмент записан тут же, на полях (“οὐδὲ πάντων ἀλλὰ τῶν μέν, τῶν δ᾽ οὔ;”).

Заканчивается этот комментарий вопросительным знаком, который, как мы разобрались, неотличим от точки с запятой (настолько неотличим, что приводит к занимательным случаям в Unicode; где, впрочем, предлагается “нормализовывать” всё в один символ, в “;”).

Кстати, что касается постквантовых криптосистем от NIST и “квантовых компьютеров, взламывающих современные криптосистемы”, которые, якобы, “могут появиться через десять лет” (а могут и не появиться): есть ещё ничуть не менее распространённый штамп, утверждающий, в этом контексте, что “квантовые компьютеры кардинально быстрее решают задачу факторизации”. Факторизация – это разложение данного числа на простые множители. Однако речь в данном штампе почти всегда идёт про алгоритм Шора. Технически, это разные утверждения: о скорости факторизации и – про алгоритм Шора. Что не так важно. Куда как более показательно, что никакой “квантовый компьютер” пока что вообще не решал задачу факторизации, что уж там говорить про то, чтобы решать эту задачу “кардинально быстрее”.

Без преувеличений и “раздувания хайпа” надо было бы сказать, что алгоритм Шора описывает теоретическое “квантовое преобразование”, которое позволяет снизить сложность факторизации, проводимой классическим компьютером, до полиномиальной. И тот же математический аппарат, который порождает данное “квантовое преобразование”, пока что успешно используется при интерпретации некоторых физических экспериментов. Не более того. О каком-то “кардинально быстрее” – и речи-то пока что не идёт. А вот “постквантовая стойкость” – это, в рамках термина, именно предполагаемая стойкость именно к “алгоритму Шора”.

Понятно, что стандартизованная постквантовая криптосистема может оказаться уязвимой для классического криптоанализа (и, скорее всего, так и выйдет). При этом, несмотря на прижившиеся штампы в СМИ, пока никто не продемонстрировал, как именно можно было бы реализовать алгоритм Шора с полиномиальной сложностью, что называется, в железе. Потому что те немногие эксперименты с числом 15 или чуть большим числом, на которые ссылаются много лет, в принципе не позволяют проверить ключевую часть реализации алгоритма – квантовое преобразование Фурье.

Тем не менее, пробовать построить квантовый компьютер хотя бы на 2^1024 состояний – это полезно.

Воскресное чтение манускриптов. В прошлом году, в заметке про кусочек папируса с фрагментом “Илиады”, я писал, что какие-то очень краткие фрагменты текстов, читаемые на папирусах, могли бы относиться к той же “Илиаде”, но их не получится так идентифицировать, поскольку недостаточно информации, а фрагменты выходят за пределы “эластичности” текста “Илиады”. Это довольно очевидное наблюдение. Тем не менее, посмотрим, можно ли на сканах манускриптов быстро найти что-то примерно подходящее, для иллюстрации. То есть, фрагменты текстов из нескольких слов, которые было бы не ясно куда отнести. Оказывается – найти можно. Для примера годится не слишком частая, но характерная фраза из записей сочинений Гомера. Скажем, кусочек из стиха, в котором упоминается Kubernetes – потому, что этот фрагмент тоже не так давно встречался на dxdt.ru, в записке про “Кибернетический след и цветовой сдвиг“. А именно: ἐνὶ οἴνοπι πόντῳ – “в тёмно-винном море”.

Ниже пара фрагментов манускриптов: Venetus A (“Илиада”, Гомер) и BnF.Grec.2771 (“Труды и дни”, Гесиод). Соответствующая фраза – выделена и там, и там.

(Venetus A, 23:316)

(BnF.Grec.2771, st. 622)

Первый манускрипт (Venetus A) датируется началом девятого века, второй – десятым (всё н.э, понятно). То есть, между соответствующими манускриптами больше ста лет, согласно датировкам. При этом структура, оформление, а кроме того, что называется, “типографика” и начертания букв, очень и очень близки, что хорошо видно на скриншотах. Удачно, что интересующие нас слова в обоих случаях приходятся на конец строки. Попадись кому-то достаточно небольшой кусочек с записью только этих слов (как выделено на картинках, вместе с частями диакритических знаков и буквы из верхней строки) – различить источники по составу и по буквам текста вряд ли было бы возможно. Однако, если удалось бы прицепить какие-то ещё буквы (строки выше и ниже), то результат уже мог бы быть более избирательным.

Гесиод – из гомеровского периода, так что, наверное, ничего удивительного. Тем более, что приведённый фрагмент текста “про море” находится очень близко к описанию в “Трудах и днях” путешествия на “состязание поэтов”, которое нередко считают упоминанием состязания между самим Гесиодом и самим Гомером.

В продолжение записки про ИИ Google и “серебряную медаль” Международной математической олимпиады. Там исходная задача, которую потом “решает” ИИ, прежде переводится людьми на входной язык системы машинных доказательств – то есть, на некоторый формальный язык, описывающий в определённых логических формулах целевое состояние, соответствующее задаче. Это не программа, как иногда пишут, а запись, грубо говоря, теоремы, соответствующей задаче, в формулах, которые возможно (при некоторых ограничениях) доказать в данной системе. Да, доказательство выполняется при помощи компьютерных вычислений, тем не менее, формальная запись задачи-теоремы не является программой, реализующей некий алгоритм – иначе не было бы смысла в поиске записей доказательств. И вот в “популярном изложении” необходимость такого перевода обосновывают тем, что нужно “переписать на языке, понятном системе”. Это, конечно, искажение. Но с ним связаны два важных момента.

Момент первый, – достаточно очевидный, – в том, что этот “суперпродвинутый” искусственный интеллект даже не способен прочитать условие задачи и, предположим, перевести его на формальный язык самостоятельно, хоть это и могло бы быть типичным вариантом запроса к ChatGPT. Так как для корректного перевода нужно хорошо понимать не только задачу, но и принципы построения формальных языков, выдача подобного ИИ-перевода для входа “системы ИИ” просто не подходит. Это понятно.

Есть и второй момент, который “замыливают” посильнее: перевод на формальный язык необходим для того, чтобы предлагаемые системой решения могли быть проверены на соответствие этому описанию машинным способом. То есть, так как предполагается, что будут подбираться тексты “доказательств” на формальном языке, необходим автоматический, машинный “проверятор” для этих доказательств – иначе, если решения потребуется согласовывать с человеком, то и работать это всё будет слишком медленно, поскольку образуется непреодолимый затык с проверкой решений. Так что необходима запись на формальном языке и проверяющая компьютерная система, а такая система в принципе не может проверять записи на естественном языке. Так что, понятно, это не решение олимпиадной задачи в том смысле, который тут принято присваивать слову “решение”.

Что же касается применения систем машинного (автоматического) доказательства в области теоретической (чистой) математики, то тут мнения, как говорится, сильно расходятся. Прежде всего потому, что теоретическая математика это не только не наука, но и вовсе не является такой уж “точной и строгой” областью, как, почему-то, нередко предполагают. Однако системы машинного доказательства очень полезны в некоторых прикладных математических направлениях. Например, для формальной проверки корректности (соответствия задаче) программного кода. Автоматические системы на этом направлении уже используются. Наверное, и автоматический генератор доказательств с перебором тут мог бы тоже пригодиться, как инструмент “фаззинга”. Но нужно учитывать, что во всех случаях речь, всё же, идет о компьютерных вычислениях, а не о математических операциях, поэтому соответствующие методы имеют существенные ограничения, как фундаментальные, так и вполне “локальные”, обусловленные ошибками на разных уровнях реализации.

Нередко можно прочитать, что “сверхразумный ИИ” сгенерирует такие “решения и идеи”, которые человек понять не сможет, а ИИ – не сможет объяснить человеку (ну, настолько вот сложные и непонятные результаты). Это очень популярная характеристика, которую часто обозначают как одно из ключевых свойств “сверхразумного” ИИ (хотя таким свойством должна бы быть как раз способность объяснить сложное, но сейчас не об этом).

С другой стороны, в популярной литературе по теме ничуть не реже утверждается, что вот на пути к уровню “сверхразумности” – ИИ должен быстро переходить из статуса просто “сильного ИИ”, в статус “сверхразумного”, используя для этого поэтапные самоулучшения: то есть, вот такой ИИ доработал собственную модель, обновился, перешёл на более мощную версию, и тут же опять улучшил показатели, снова обновился, и так далее. Так утверждается.

Между тем, подобный “рекурсивный ИИ” мог бы работать в обратную сторону, с целью объяснения тех самых “сложных идей” из первого абзаца: вот “сверхразумный” ИИ объяснил свои идеи своей предыдущей итерации – интеллекту не менее искусственному, но который попроще, пусть и близок по “уровню понимания”, тот – предыдущей итерации, и, – опять же, – так далее, вплоть до уровня, близкого уже тем самым человекам.