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

NIST выпустил первые стандарты по криптосистемам с постквантовой стойкостью. Как и ожидалось:

• FIPS 203: обмен ключами (KEM) – Kyber, который в стандарте называется ML-KEM, где ML – это Module-Lattice (модули с решётками, а не “машинное обучение”);
• FIPS 204, FIPS 205: подписи – CRYSTALS-Dilithium (ML-DSA, основной, 204) и Sphincs+ (SLH-DSA, дополнительный/резервный, 205).

(via)

P.S. Универсальных квантовых компьютеров пока нет и не видно, даже если присмотреться, но NIST в новости намекает, что, “как предсказывают некоторые эксперты”, квантовые компьютеры, способные взламывать современные криптографические алгоритмы, всё же могут появиться в течение десяти лет.

Официальная новость ТЦИ про добавление определения X25519Kyber768 на audit.statdom.ru (САБИУ). Цитата:

На серверной стороне поддержка реализована, например, на узлах Google и веб-фронтендах Cloudflare, одного из крупнейших мировых провайдеров веб-доступа. То есть существенная часть веб-трафика в Интернете уже защищена с помощью данной криптосистемы.

Вообще, этот момент почему-то сейчас упускают из виду: может, оно и прошло незаметно, но сейчас, если вы используете Google или Youtube через более или менее современный браузер из распространённых, TLS-трафик уже защищён при помощи ключей, полученных с использованием Kyber768 – то есть, постквантовой криптосистемы. А если сюда добавить, что очень многие мало-мальски популярные сайты используют Cloudflare, – в том числе, в Рунете этот сервис очень распространён, – то окажется, что немалая часть обычного TLS-трафика в Вебе, – точно больше трети, – уже перешла, так сказать, на “постквантовые ключи”. А момент довольно интересный, но почему-то про него не особо-то пишут даже технические СМИ.

(Кстати, по наличию поддержки на стороне сервера можно, – примерно, – судить, у кого насколько “свой” TLS-бэкенд. Тоже занимательно.)

Код, написанный на C, можно транслировать на другие языки высокого уровня при помощи строгого и детерминированного транслятора. Казалось бы. Тем не менее, DARPA тоже подключается к хайпу и предлагает реализовать такой транслятор при помощи LLM. Конечно, перевод должен осуществляться на Rust, потому что нужно же “исключить уязвимости при работе с памятью”, но, конечно, нельзя исключать и влияние моды – об этом, кстати, прямо сказано в исходном сообщении.

(Новость на русском.)

Очередное “ИИ решает математические задачи”, в этот раз – от Google и про олимпиадные задачи, но, хотя бы, есть уточнения про ограничения. В исходном сообщении сказано, что “AI achieves silver-medal standard solving International Mathematical Olympiad problems” (“ИИ достиг уровня серебряной медали, решая задачи Международной математической олимпиады”).

Если прочитать сообщение внимательно, то оказывается, что, на первом шаге, задачи были вручную переформулированы в виде предложений на формальном языке, который “подходит для системы”. Буквально: “First, the problems were manually translated into formal mathematical language for our systems to understand” – “Прежде всего, задачи были вручную переведены на формальный математический язык, чтобы наши системы их поняли”. То есть, данный ИИ, – который, как теперь напишут в СМИ (не Google), “демонстрирует уровень серебряного медалиста Международной математической олимпиады”, – даже не может прочитать задачи в том виде, как они представлены для людей (я, собственно, давно привожу этот момент в качестве примера).

Под “формальным математическим языком”, судя по всему, имеется в виду язык системы компьютерных доказательств Lean. То есть, речь, конечно, не про то, что задачу просто “записали строго”: исходные формулировки и так достаточно строгие. Заметьте, что корректный перевод исходного текста задачи на тот или иной формальный язык требует достаточно высокой квалификации и, обычно, примерного понимания сути самой задачи. Рассматриваемой системе ИИ этот шаг, очевидно, недоступен.

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

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

Подборка некоторых заметок на dxdt.ru по теме ИИ (Искусственного Интеллекта):

ИИ на модных LLM/VLM и задачи-картинки – современные системы ИИ не могут справиться с простейшими задачками, сформулированными при помощи картинок.

Машинный ИИ в книгах прошлого века – 75 лет назад вышла книга Giant Brains or Machines That Think.

Тексты про ИИ и Situational Awareness с программным кодом – в весьма популярной статье про состояние ИИ обещают суперинтеллект, пишущий “триллионы строк программного кода”, уже в ближайшие годы.

LLM и задача про название книги (на примере GigaChat) – для элементарной задачки, доступной младшему школьнику, GigaChat генерирует абсурдный “текст-ответ”.

Мешанина токенов в LLM – небольшое пояснение с примерами про “веса и токены”, которые используются LLM для генерирования текстов.

Машинное обучение на электронах – шуточная заметка про “обучение нейростеки” на результатах квантовых опытов.

ИИ и формулы окружностей – отличительной чертой действительно интеллектуального результата обработки данных является возможность заменить “поток чисел” корректной и короткой формулой.

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

“Вес” значений омонимов в текстах для LLM – проявление омографов в результатах выдачи LLM.

Морфологический переворот как инструмент в “тесте Тьюринга” – LLM не связывают с самим текстом никакой смысл или структуру, поэтому омонимы в запросе позволяют показательно “переключать ветки” генерируемого текста.

Пример про запутывание контекста в LLM (GigaChat) – конкретные примеры работы LLM с омонимами (“собачка в замке”).

Обобщение ИИ и “кнопки на пульте” – уровень рефлексии и ритуальное восприятие “пультовых систем”, как самодостаточных структур.

Галлюцинации ИИ в словах года – влияние хайпа на словари и влияние словарных статей на отношение к публикациям про LLM-чаты.

Неверная интерпретация систем ИИ как “инструмента для анализа” – некоторые пользователи ошибочно полагают, что системы ИИ/LLM “собирают и проверяют информацию”.

Широкие проблемы применения ИИ – “нейросети” могут применять как придётся, полагаясь на “компьютер не может ошибаться”.

Перспективный ИИ в “разработке кода” – ИИ-говорилка вместо программиста и тестовые примеры в реализациях шифров.

Вычислимые опасности ИИ – экономикой многих предприятий уже управляет MS Excel, LLM-генераторы текстов – ещё удобнее, осталось дождаться “нечеловеческого интеллекта”.

Детектирование текстов, сгенерированных ИИ – можно ли точно детектировать выдачу одной программы при помощи другой программы.

Развитие автоматических “говорилок” (чат-ботов) – про мультфильм “Трое из Простоквашино” (1978 года).

Нейросети из пикселей – “растягивание” пикселей и подмена утерянных данных на сгенерированные.

Закладки в системах с машинным обучением – недокументированные возможности, скрытые в коэффициентах “нейросетей”, предназначенных для классификации объектов.

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

Скрытный искусственный интеллект – возможно, “сверхразумный машинный интеллект” предпочитает осторожную тактику.

Опасный ИИ и общедоступные вычислительные ресурсы – о запретах на “алгоритмы ИИ”.

Для OpenSSL переделали сайт, почему-то потеряв старые ссылки (например, блог, что не очень-то удобно). Зато добавлены Bouncy Castle и Cryptlib.

Однако главную часть новой основной страницы под openssl.org занимает текст “Миссия”, рассказывающий о доступности инструментария “для всех”, но если с данной страницы, прямо под текстом “Миссия”, кликнуть на большую кнопку-ссылку Cryptlib, то тут же окажется, что там доступ для российских IP-адресов заблокирован: “403 Forbidden” – говорит тамошний веб-сервер.

Исследователи предполагают (англ.), что некоторые из зверей могут воспринимать инфракрасное излучение при помощи специальных шерстинок-антенн: так, мелкие грызуны, которые рассматриваются в исходной работе, несут подобные шерстинки на шкурке со стороны спины.

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

Заголовок новости начинается словами “В KDE устранены крахи” (дальше там про улучшение поддержки Wayland). Конечно, пусть KDE и весьма неплохая оболочка, но нравится не всем.

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

На сервисе ТЦИ audit.statdom.ru добавлена проверка поддержки криптосистемы X25519Kyber768 на TLS-узлах (HTTPS).

Официальные сопроводительные документы, касающиеся запрета продуктов “Лаборатории Касперского” в Штатах, уже доступны (на странице по ссылке – блок внизу, справа). Однако все моменты, которые могли бы оказаться минимально интересными с технической точки зрения (Appendix A) – аккуратно вырезаны (с пометкой “Business Confidential Information”). Поэтому ничего содержательно нового там всё равно не просматривается, но тенденция – показательная.

(Дополнение: о чём-то, типа предполагаемой “сборки из исходников”, можно догадаться по контексту, но, всё же, это было и так понятно.)