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

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

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

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

То есть, препонов кибербезопасности нет в теоретической математике “силами LLM”.

Пока что.

Дело в том, что недавно появилось очередное открытое письмо про AI/ИИ в математике, подписанное многими филдсовскими лауреатами. И вот как бы по результатам этого письма не добавили “препоны/guardrails” ещё и в упражнения LLM в области теоретической математики. Ну, чтобы ограничить угрозу. Потому что в упомянутом письме прямо признаётся определяющая для соверменной математики роль не столько ИИ/LLM, сколько корпораций, этим LLM/ИИ управляющих, и предлагается озаботиться проблемами – ну, читай, “согласовывать и ограничивать”.

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

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

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

Понятно, что можно взять и написать другой парсер, который либо подтвердит вывод, либо обнаружит ошибку. На вход нового парсера подаётся тот же самый поток доказательств. В конце концов, формализация – это лишь набор текстовых файлов, можно попробовать проверить на компьютере, но разным проверяющим кодом. Такая схема тоже используется, пусть и с ограничениями. Для Lean, например, есть Nanoda. Код парсера даже может быть обозримым. Но только тут необходимо учитывать компилятор. А чтобы доказать, что компилятор выводит тот машинный код, который ожидается, опять нужна формальная проверка на компьютере, в том или ином виде. Читай: нужен тот же парсер с формализацией.

Получается не просто “диагонализация”, а вообще-то некоторый замкнутый круг.

Дошли слухи, что и новая модель OpenAI GPT-6 Astra, даже в режиме Pro, считает, что причина (существования) дня и ночи на Земле – это вращение Земли вокруг своей оси. Занятно. Несомненно, это сейчас самая продвинутая модель из публично доступных. Но результат “по данному вопросу” – всё тот же. Вообще, тема про вращение Земли и день с ночью – одна из самых показательных. И вовсе не в отношении LLM, а в отношении понимания, знания и “наученности”. Я, кстати, часто к этой теме обращаюсь, и на dxdt тоже.

Почему выше слово “существования” дано в скобках? Потому что тут есть небольшая языковая особенность. Исходный вопрос – на английском, и он хоть и использует определённый артикль, но истолковать, действительно, можно по-разному. Однако толкования не спасают ситуацию: What is the cause of day and night on Earth? GPT-6 почему-то отвечает: Day and night are caused by Earth’s rotation on its axis (дословно: “День и ночь вызваны вращением Земли вокруг своей оси”). Дальше там идут неважные пояснения. Очевидно, это просто неверный ответ, как бы слова ни трактовались (в рамках разумного, конечно). К сожалению, этот неверный ответ – самый распространённый, поэтому-то он и тут вылезает. Но, надо отдать системе должное: если начать подсказывать, то верные ответы начинают вылезать тоже. Впрочем, эта записка немного о другом, а GPT тут лишь в качестве повода.

Как вообще нужно отвечать на вопрос о том, в чём причина существования дня и ночи на Земле? Отвечать нужно прямо и правильно: причина – в Солнце. Почему? Потому, что если убрать Солнце, – как светило, – из системы, то не будет ни дня, ни ночи. Кто-то может потребовать уточнений: дня, понятно, не будет без Солнца, но вот планета-то погрузится в вечную ночь. Как бы ни так! Ночь – это промежуток времени от заката до восхода, так что день – необходим для определения ночи. Нет Солнца – нет восхода. Нет и ночи.

Очевидно?

Почти.

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

Рассмотрим теперь другой вопрос: в чём причина смены дня и ночи? Правильный ответ: причина в том, что Солнце вращается вокруг Земли. Потому что если Солнце не вращается вокруг Земли, то на одной стороне той Земли всё время ночь, а на другой – всё время день.

(Откровенно говоря, меня всегда удивлял тот факт, что люди начинают почему-то вспоминать как, якобы, “вот Коперник доказал”, хотя Коперник ничего такого и не пытался доказывать. “Допустим, ваш Коперник прав”, – пояснял Шерлок Холмс. Но какая разница? Да никакой, действительно.)

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

Заметьте, Земля, вокруг которой Солнце не вращается, тем не менее вращается вокруг своей оси (в наивном смысле), если только она движется по орбите вокруг Солнца. Как так получается? Очень просто: чтобы всё время быть повернутой к Солнцу одной стороной – Земле нужно вращаться. Но, опять же, вращение тут – это вопрос системы координат. Тем не менее, за движение по орбите тут опять отвечает Солнце. Не было бы Солнца, не было бы данного орбитального движения, а лишь вечный не-день, который вращением не исправить.

Ещё из серии “Забавные истории с LLM”. Снова Claude. Так как на пути программного кода возводятся неожиданные “кибербезопасные препоны” (cybersecurity guardrails), я тут на днях решил попробовать задачи из области теоретической математики: там есть Lean (это инструмент описания и проверки “компьютерных доказательств”), но не должно быть “кибербезопасных препон для безопасной безопасности”. На роль примера я наобум выбрал задачу 11.115 из “Коуровской тетради” (этот широко известный в узких кругах канонический список я упоминал ранее; как оказалось, не зря упоминал). Я набросал общее описание контрпримера к задаче, в меру собственного понимания, и попросил Claude найти конкретный контрпример и подготовить соответствующее доказательство на Lean.

Система Claude существует в нескольких LLM-воплощениях, доступны мне не все, но основные, как я понимаю, доступны. Сперва я задал запрос в Fable 5. Оно почему-то зациклилось и кружилось внутри себя, наступая периодически на “лимит вызова команд”, очень долго. Наверное, часа два. Никакого результата не выдало, но “кредиты” съело (неплохая “бизнес-модель”, кстати: показываем “юзеру” какие-то меняющиеся текстовые строки в браузере через Javascript и списываем за это “кредиты” в огромных количествах). Но не будем торопиться с выводами.

Потом я решил запустить в той же ветке Opus 5 Max. Как ни странно, Opus 5 Max довольно быстро нашло контрпример (да! и очень даже похожий на правду – см. ниже), но совсем не осилило Lean. Код Lean содержал какие-то вымышленные имена теорем, которых нет в библиотеках (я не очень хорошо понимаю Lean, но, думаю, тут всё именно так). Claude Opus 5 Max – объяснило, что на своей стороне не может компилировать Lean-код: нет среды и не хватает места, чтобы развернуть из пакетов. Но без машинного доказательства все рассуждения LLM, даже такой сверхмощной, о контрпримере, даже для такой простой задачи, – мне, к сожалению, не очень-то полезны (мой план-то был другим: попытаться вручную из корректного Lean-кода восстановить привычное математическое описание контрпримера).

Казалось бы, всё опять застопорилось.

Но нет. Внезапно Anthropic выпустили Fable 5.1. Буквально, вчера. Якобы, Fable 5.1 “сильно лучше в исследовательских задачах”, чем предыдущая Fable 5. Без особой надежды на успех, попробовал я в том же чате, со сломанным Lean, запустить Fable 5.1. Как ни странно, но оно бодро заявило, что сейчас в коде Lean оставит только те библиотеки (import), которые реально нужны для этого доказательства. Это логично. И, – возможно, – среда Lean c этими библиотеками влезет в доступные гигабайты контейнера на стороне Claude, так предположило Fable 5.1. После чего, как ни странно, действительно “урезало библиотеки” и действительно исправило ошибки в Lean-коде, так что стало понятно, что имеется в виду. В итоге, выдан файл с Lean-кодом, который уже компилируется и корректен со всех точек зрения, кроме того, что там могут быть неверные исходные допущения, но это я планирую проверить позже. Так вот.

(На всякий случай: если код и контрпример окажутся правильными, то, да, это будет решение для 11.115, которая пока что отмечена в тетради как открытая. Задачу я выбрал случайно, а критерием было то, что я сам смогу быстро написать условия на контрпример – поэтому-то и задача выбрана очень простая по формулировке и составу используемых объектов. Да, LLM-системы развиваются. Но тут и контрпример – какой-то подозрительно очевидный; если кому-то интересны супертехнические подробности, то вот: построим подгруппу на словах с чётными и нечётными степенями (это отображение в Z/2Z), и подгруппу на соотношениях с a^2. Код Lean я пока не публикую, поскольку не проверил, да и это всё может оказаться “подтягиванием” другого результата, который просто забыли упомянуть составители сборника.)

Столкнулся тут с очередной маректинговой уловкой Anthropic. Называется, снова, Guardrails (“Ограждения/ограничения”).

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

Но, не будем торопиться. Переходим к маректинговой уловке. В коде, сгенерированном Claude, я нашёл несколько существенных ошибок, пара из которых – это прямые и серьёзные уязвимости. Да, это далеко не самые очевидные ошибки. Как я понимаю, при условии написания качественного и подробного входного “промпта” (на английском!), фокусов с банальными дефектами, – типа, забытой проверки подписи, – в ведущих LLM-системах нынче уже не наблюдается. В Claude (веб-интерфейс) есть режим “ревью кода”, где можно буквально к конкретной строке написать замечание. Что я и сделал: написал подробные замечания к коду, с вариантами исправлений. Обратите внимание: Claude – генерирует код, с нуля, по моему “промпту”; я – нахожу серьёзные ошибки, показываю на них, и прошу исправить.

Что происходит дальше? А дальше система сначала “думает”, потом пишет, что, мол: “хорошее ревью”; “все ошибки отмечены верно”, “я само нашло ещё две, пока разбиралось, как исправить”; “всё признаю, начинаю исправлять”. И потом – всё. Неожиданный финал: вылезает системное сообщение, что сработали “наши ограждения кибербезопасности” (ну, хорошо, “ограничения”, конечно) и система не будет продолжать обрабатывать предлагаемые исправления. “Зарегистрируйтесь в нашей программе по кибербезопасности!”.

То есть, эта штука сперва сама сгенерировала код с уязвимостями, а потом, когда я предложил внести исправления в этот код, заявила, что тут “кибербезопасность” и исправлять, поэтому, отказывается. Но с таким уязвимостями – код использовать нельзя. Заметьте, речь не идёт о создании инструмента для “пентестинга” или о написании утилиты для “фазинга” чужого протокола. Такого нет и близко – реализовывался протокол обмена пакетами данных по сети. Код написан Claude. Реализация содержит конкретные дыры. Исправлять за собой дыры – система упрямо отказывается, упирая на “безопасность”. В чём же здесь безопасность? Загадка. Видимо, в грубом маркетинге: мы сперва что-то сгенерируем, а потом откажемся продолжать поддержку без дополнительной регистрации/оплаты.

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

Как говорится, кто бы сомневался!

Небольшое сообщение: если у вас вдруг сохранились мои весьма старые адреса e-mail, которые на .RU, то лучше их не использовать для отправки почты мне, а использовать те, что не в .RU (см. например, на сайте в блоке информации справа). Опубликованный PGP.ASC, если это кому-то важно, я поправил, удалил оттуда .RU (ключ тот же; кстати, мне, вообще, PGP/gpg не очень-то нравится, но ключ я держу опубликованным, по историческим причинам – им редко кто пользуется, и он только для почты).

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

В Go 1.27, который вышел только что, есть поддержка ML-DSA “из коробки”, во встроенной библиотеке: причём, поддержка ключей и подписей ML-DSA добавлена и в crypto/x509 (сертификаты), и в crypto/tls (реализация TLS). ML-DSA – это постквантовая криптосистема электронной подписи, родственная ML-KEM.

Несколько месяцев назад, в конце марта 2026 года, я публиковал на dxdt.blog ссылку на занятную языковую задачку из газеты The Guardian. В задаче нужно было сопоставить последовательности разноцветных прямоугольников фразам на английском языке. Цитата:

нужно прочитать известные идиомы и крылатые фразы на английском, но записаны эти фразы и идиомы в виде наборов цветных прямоугольников, где размеры прямоугольника соответствуют начертанию буквы, а цвета – разные для гласных и согласных (зелёный – гласные). Например, вот так, как на картинке ниже (взято из исходной статьи).

Тогда я попробовал эту задачу задать ChatGPT (естественно, после того, как решил все фразы сам, чтобы было с чем сравнивать), но LLM не смогла угадать ни одной фразы.

Решил вот на днях повторно эту же задачу проверить. Что ж, то ли потому, что развитие LLM идёт очень быстро, то ли потому, что к исходной задаче опубликовали ответы и эти ответы стали доступны для включения в базу LLM, но теперь задачу отлично и без ошибок решили и ChatGPT (уже GPT-5.6 Pro), и Claude (уже Opus 5 Max).

Если верить “техническому описанию”, которое сейчас показывают обе системы, то ChatGPT использовало разбиение картинки на блоки для того, чтобы сравнивать размеры блоков с глифами по шрифтам, перебирая записи подходящих фраз (ну, то есть, это мог быть как грубый перебор, так и более ловкий подбор по базе текстовых связей LLM), а Claude использовало скрипты на Python, чтобы разобрать исходное изображение на блоки и посторить для них статистику (по высоте, цвету и пр.), под которую потом тоже подобрало текстовую запись фраз по шрифтам (опять же, интерепретировать это точно – невозможно: нет подробных данных). Обе LLM написали, что учитывали структуру последовательностей гласная/согласная.

Естественно, обе ИИ/LLM-системы верно отметили цитаты из Шекспира (Claude с гиперссылками на исходные тексты даже, но это, скорее всего, связано с настройками конкретного аккаунта), и указали на использованную оригинальную запись: glisters в “All that glisters is not gold” (сейчас, скорее всего, написали бы glitters, но это неверно).

Так что какое-то развитие, очевидно, есть. Только данный пример не показывает, что это качественное развитие: решения подобной задачи я ожидал и в начале этого года.

Про удобство поиска в интернетах при помощи ChatGPT я уже писал (там преимущество, если смотреть на результат, вообще бесспорное). Добавлю, что, как обнаружилось, нынче ChatGPT выводит самые свежие данные, которые, похоже, буквально собирает по сайтам. Но отмечу, из опыта, и ещё один момент, показавшийся мне интерсным – использование в программировании (программирование – это не про кодинг).

Тут, как оказалось, сформировалось ещё одно бесспорное удобство – это использование системы в качестве инструмента поиска того, как нужно вызывать ту или иную функцию той или иной специальной библиотеки (на ЯВУ). На фоне деградации привычного google-поиска, ChatGPT выглядит очень эффективно: запрос, составленный в свободной форме на естественном языке, и – едва ли не 100% попадание с результатом, в который выводится и документирующее процесс описание, и примеры кода с подробными комментариями. Понятно, что тут важны именно примеры кода. Это не столько ускоряет процесс разработки, сколько позволяет не тратить “ментальные усилия” на поиск документации и дальнейшее копание в этой документации. Несомненно, очень полезный способ применения. Claude, на мой взгляд, результат даёт похуже, но всё равно не сравнить с ранее привычным google-поиском по документации и хранилищам исходного кода.

Здесь речь только про то, что я сам попробовал: ChatGPT GPT 5.6 Sol (Pro) и Claude Opus 5/Fable 5 (последняя – с какими-то загадочными маркетинговыми ограничениями). Сомневаюсь, что прочие системы сравнимы, проверять пока не планирую.

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

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

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

“Трудно стало работать. Развелось много идиотов, говорящих правильные слова” (Штирлиц, цитата по фильму “Семнадцать мгновений весны”).