Вне рамок стандартного коммерческого программирования и непрекращающегося хайпа вокруг нейросетей рождается качественно иной подход к созданию программного обеспечения. В развернутом интервью для канала Machine Learning Street Talk математик и программист Охад Асор (Ohad Asor) представляет концепцию Tau Language — логического языка спецификаций, способного автоматически синтезировать гарантированно корректный код. Центральной темой беседы становится радикальный пересмотр будущего разработки, систем автоматического ведения бизнеса и концепции децентрализованных сетей, управляемых непосредственно их пользователями.
🧠 Ограничения машинного обучения и «три проклятия» ИИ 0:00
Современный бум нейросетей во многом опирается на эмпирический успех, однако Охад Асор предлагает взглянуть на эту технологию через призму строгой математической логики. По его мнению, машинное обучение — это «математическое чудо», способное обучаться на примерах и выдавать правильные ответы с высокой долей вероятности. Тем не менее основатель Tau Language подчёркивает фундаментальное ограничение такого подхода: вероятность ошибки в подобных системах никогда не будет равна нулю, а вероятность абсолютно точного результата никогда не достигнет единицы. В академической среде этот принцип описывается как PAC-обучение (Probably Approximately Correct — вероятно, приблизительно корректное обучение).
Гость интервью утверждает, что индустрия уже практически достигла пика возможностей чисто статистических методов. По мере роста сложности и размерности логических задач точность нейросетей начинает стремительно падать, в конечном итоге скатываясь к результату случайного угадывания, эквивалентному подбрасыванию монетки. В качестве примера Асор приводит булеву выполнимость (задачу SAT). Современные SAT-солверы способны эффективно справляться с формулами, содержащими тысячи переменных. В то же время статистические модели, сталкиваясь с определенным порогом сложности (например, в несколько сотен переменных), теряют предсказательную способность и выдают случайные ответы.
Для иллюстрации проблемы сверхпереобучения (overfitting) в машинном обучении Охад Асор проводит аналогию с полиномиальной интерполяцией Лагранжа. Используя полином сотой степени, можно идеально соединить сто случайных точек на графике, однако использовать полученную кривую для прогнозирования следующего временного шага бессмысленно — результат окажется абсолютно случайным. В теории машинного обучения это описывается через бесконечную размерность Вапника — Червоненкиса (VC dimension). Если модель способна подстроиться под абсолютно любые хаотичные данные, ее реальная предсказательная сила за пределами обучающей выборки стремится к нулю.
В ходе дискуссии ведущий Тим Скарф отмечает, что за последние месяцы такие компании, как OpenAI (в частности, с моделями серии o1), наглядно демонстрируют рост точности за счет инженерии и цепочек рассуждений (chain of thought). Более того, в индустрии набирает популярность трансдуктивный подход (transduction), активно применяемый, например, в рамках теста ARC Франсуа Шолле (Francois Chollet). При трансдукции спецификация тестовых данных закладывается внутрь самой функции предсказания, что позволяет учитывать контекстуальную сложность реального мира.
Несмотря на привлекательность локальной оптимизации, Охад Асор сохраняет скепсис. Он напоминает, что современные методы машинного обучения по сути являются оценщиками максимального правдоподобия. Они неизбежно регрессируют к среднему значению, выдавая наиболее обобщенный ответ.
Математик выделяет три фундаментальных проклятия машинного обучения, сформулированных в теоретической базе:
- Проклятие оптимизации (optimization curse).
- Статистическое проклятие (statistical curse).
- Проклятие аппроксимации (approximation curse).
По мнению гостя, если сузить пространство гипотез ради снижения статистической ошибки, возникнет критическая ошибка аппроксимации. Выходом из этого замкнутого круга Асор считает полный отказ от статистического угадывания в пользу дедуктивных логических методов везде, где это возможно.
💬 Дихотомия языка и физического мира 11:14
Разграничивая сферы применения логики и нейросетей, Охад Асор соглашается, что машинное обучение незаменимо в областях, которые человек не способен четко описать словами. Классический пример — распознавание лиц: любой человек мгновенно идентифицирует знакомого, но не сможет составить исчерпывающую текстовую инструкцию с описанием геометрии лица для компьютерной программы. Однако для задач, поддающихся строгому определению, использование примеров вместо прямых декларативных спецификаций кажется гостю нерациональным.
Существует глубокая философская дихотомия между реальным миром и тем, что человечество говорит об этом мире. Вторичность и ограниченность вербального аппарата Асор иллюстрирует известной метафорой: «Палец, указывающий на Луну, не является Луной». Человечество одержимо концептуальным пространством и языком, который стал для нас важнее и реальнее физической среды.
В качестве доказательства этой изоляции языка от реальности Охад Асор приводит фундаментальный тезис: наука и философия до сих пор не способны дать исчерпывающее словесное определение тому, что значит «физически существовать». Соответственно, любое наше языковое описание является лишь приближением.
Когда человек планирует пойти в магазин за томатами, слово «томат» выступает абстрактной категорией, никак не связанной с физическим объектом на прилавке до тех пор, пока покупатель не придет и не возьмет его в руки. Сам Охад иронично замечает, что словосочетание «я математик» — лишь абстрактный ярлык, в то время как объективная реальность описывает его как «парня в очках и без волос».
Человеческая labels-пластичность и способность к декларативной маркировке объектов отличает нас от животных. Нейросети не оперируют чистыми символами и абстракциями без явных архитектурных ухищрений со стороны инженеров. Вместо того чтобы имитировать символьное мышление через сложные циклы и громоздкие вычисления линейной алгебры, Охад Асор призывает внедрять логические методы напрямую.
При этом ИИ-системы должны строиться не вокруг абстрактного физического мира, а вокруг мира, каким его воспринимает человек посредством языка. Ведь конечная цель ИИ — служить специфической лингвистической природе человека.
🛠 От верификации к программному синтезу 21:09
Обсуждая развитие формальных методов в ИТ, Охад Асор заявляет, что классическая верификация программного обеспечения — это «вчерашний день». Традиционный подход устроен следующим образом: инженеры пишут код системы, затем формулируют логические утверждения (требования) к ней и пытаются доказать, что код им соответствует.
Настоящим технологическим прорывом гость называет программный синтез. В этой парадигме пользователь описывает исключительно требования и ограничения, а компьютер на их основе автоматически генерирует исполняемый код, который гарантированно им соответствует. Аналогией из практики современных разработчиков может служить методология, при которой пишутся только тесты, а сама программа синтезируется машиной до тех пор, пока все тесты не будут пройдены.
Главный вызов здесь заключается в тестировании систем на бесконечных доменах входных данных. Написать физический тест, проверяющий бесконечное число состояний смартфона, невозможно. Однако математические методы позволяют доказывать утверждения сразу для бесконечных множеств объектов. Если перевести задачу синтеза в корректный математический фреймворк, можно получить стопроцентные гарантии безопасности ПО для любых входных параметров.
Ведущий Тим Скарф озвучивает позицию «адвоката дьявола»: в реальной жизни жесткие правила часто обходят за счет гибкости языка. Например, модерация соцсетей запрещает определенный контент, но пользователи постоянно изобретают новые эвфемизмы (вроде «кальциевых пушек»), чтобы обойти фильтры. Язык постоянно мутирует, адаптируясь к контексту, и жесткая логика рискует оказаться слишком хрупкой.
Охад Асор парирует это разграничением зон ответственности. Он выделяет три плоскости:
- Физический мир.
- Человеческий мир.
- Компьютерный мир.
По признанию математика, физическая и социальная сферы хаотичны и лежат вне его контроля, но в компьютерном мире он способен гарантировать абсолютную предсказуемость.
В качестве примера рассматривается разработка банковского ПО. Ни один разумный архитектор не станет доверять генерацию ядра банковской системы большой языковой модели (LLM), поскольку риск случайной ошибки неприемлем. В традиционном программировании разработчикам приходится вручную отслеживать все участки кода, где неявно обновляется баланс счета, чтобы не допустить его ухода в минус. В системе синтеза Tau достаточно написать одну декларативную строчку:
$$\text{balance} \ge 0$$
Программа будет сгенерирована автоматически с жестким соблюдением этого правила. Если бизнес-требования изменятся и конкретному банкиру из Цюриха потребуется разрешить овердрафт при определенных условиях, это изменение просто вносится на уровень общей спецификации, трансформируя всю систему.
Основная сложность классического программного синтеза заключается в том, что наивный поиск по пространству возможных программ приводит к экспоненциальному взрыву. По словам Асора, Tau Language решает эту проблему за счет специальной математической структуры. По аналогии с основной теоремой алгебры (где некостантный комплексный полином гарантированно имеет корень, и нам не нужно перебирать бесконечное множество чисел для его проверки), фреймворк Tau позволяет осуществлять относительно простые проверки над бесконечными множествами предложений, быстро находя работающий алгоритм. При этом язык намеренно спроектирован так, чтобы проблема останова (halting problem) для его спецификаций оставалась разрешимой.
🔬 Преодоление теоремы Тарского и булевы алгебры 32:03
Ключевым теоретическим достижением Tau Language Охад Асор называет преодоление фундаментального ограничения математической логики — теоремы Тарского о невыразимости истины. До сих пор математики воспринимали эту проблему как сугубо философскую абстракцию, но Асор разглядел в ней главный барьер на пути к созданию безопасного ИИ.
Теорема Тарского гласит: если взять язык арифметики натуральных чисел с операциями сложения и умножения и попытаться добавить в него предикат истины, который принимает гёделев номер (цифровое кодирование) любого предложения этого же языка и возвращает значение «истина» или «ложь», то система неизбежно придет к противоречию. Такой язык становится противоречивым, позволяя одновременно доказать любое утверждение и его отрицание.
Охад Асор утверждает, что нашел способ обойти это ограничение в практических целях. Его метод заключается в абстрагировании предложений языка до элементов булевой алгебры. В такой модели полностью игнорируется внутренняя синтаксическая структура предложения, оно рассматривается исключительно как неделимый элемент алгебры.
Математик предлагает два эквивалентных определения булевой алгебры для понимания аудиторией:
- Множество предложений, над которыми разрешены только логические операции «И», «ИЛИ», «НЕ» и проверка на семантическое равенство (означают ли предложения одно и то же, независимо от написания).
- Семейство множеств, где допустимы только операции объединения, пересечения и дополнения, но полностью отсутствует предикат принадлежности (нельзя заглянуть внутрь множества и изучить его отдельные элементы).
Благодаря такому абстрагированию до безатомных булевых алгебр, Tau Language становится уникальным логическим языком, способным ссылаться на собственные предложения без риска уйти в логическую противоречивость.
🏗 Архитектура языка Tau и pointwise revision 53:34
С технической точки зрения Tau Language представляет собой стандартную теорию булевых алгебр, усиленную несколькими фундаментальными расширениями:
- Доступ к любым элементам: В отличие от классической теории, оперирующей только концептами нуля и единицы, Tau может напрямую ссылаться на любой конкретный элемент алгебры.
- Рефлексивность: Булева алгебра, которой оперирует язык, состоит из предложений самого же языка Tau.
- Временное измерение (темпоральность): Язык позволяет сопоставлять текущие логические утверждения со спецификациями, действовавшими, к примеру, пять шагов назад.
- Разделение входов и выходов: Четкое разграничение входных параметров и выходных реакций системы.
Последнее расширение имеет решающее значение для создания программ. В Tau Language можно математически доказать, что в любой дискретный момент времени для любого бесконечного домена входных данных существует выход, удовлетворяющий спецификации. Если спецификация проходит проверку на выполнимость (satisfiability), система гарантированно способна синтезировать рабочую программу.
Охад Асор делится актуальным статусом разработки: если долгое время у команды был готов лишь интерпретатор, способный выполнять спецификации «на лету», то буквально за месяц до интервью (весной 2026 года) ему удалось финализировать полноценный алгоритм компиляции. На выходе система генерирует оптимизированный код на языке C++, сторонником которого является сам Асор, хотя теоретически это может быть любой Тьюринг-полный язык.
Отдельное внимание в беседе уделено концепции поточечного пересмотра (pointwise revision). В классической теории ИИ задача изменения убеждений (belief revision) считается алгоритмически неразрешимой оптимальным путем. Если в старой базе знаний содержатся правила $A \implies C$ и $B \implies C$, а новое требование гласит $\neg C$, у системы возникает слишком много равнозначных вариантов деструкции старых правил (удалить первое, удалить второе, объявить ложными $A$ или $B$).
Однако в контексте Tau, где фокус смещен на то, какие конкретно выходные данные должна генерировать программа в данный момент времени, оптимальный пересмотр становится возможным. Формула поточечного пересмотра формулируется изящно:
Если существует выход, удовлетворяющий одновременно и старой, и новой спецификации, система выбирает его. Если такого компромисса нет, код автоматически перестраивается так, чтобы гарантированно удовлетворить новую спецификацию, оставив максимум от старой в неизменном виде.
Это избавляет разработчиков от необходимости переписывать огромные пласты ПО с нуля при локальных изменениях требований.
Для оптимизации и сжатия громоздких спецификаций компилятор Tau использует алгоритмы элиминации кванторов (quantifier elimination). Все кванторы существования ($\exists$) и всеобщности ($\forall$), усложняющие структуру, в процессе нормализации математически удаляются. Это может сделать итоговый код менее очевидным для человеческого восприятия, однако Асор подчеркивает, что компилятор Python тоже переписывает исходный код оптимизированным и чуждым для человека образом, просто не демонстрирует это пользователю.
🌐 Децентрализация и «эндгейм» блокчейнов 1:08:38
Глобальная миссия Tau Language выходит далеко за рамки сугубо прикладного инструментария для автоматизации кодинга. По заявлению Охада Асора, единственная цель проекта — вернуть пользователям тотальный контроль над программным обеспечением. В текущей ИТ-инфраструктуре потребители бесправны: централизованные команды разработчиков единолично решают, в какую сторону развивать софт. Технология Tau призвана ликвидировать эту асимметрию, позволив пользователям напрямую диктовать свои условия вычислительным системам.
Наиболее радикально этот подход должен изменить индустрию распределенных реестров. Охад Асор открыто называет Tau «конечной игрой (эндгеймом) для всех блокчейнов». Сейчас на рынке присутствуют тысячи изолированных блокчейн-сетей, конкурирующих за счет жестко зашитых архитектурных фич. Tau предлагает альтернативу: мета-блокчейн, способный на лету менять собственный исходный код, консенсус и правила на основе формализованного консенсуса пользователей. Ему не нужен сторонний блокчейн, скорее будущим децентрализованным сетям жизненно необходим Tau, чтобы развиваться без перманентных хардфорков и расколов сообщества.
В отличие от Ethereum, где смарт-контракты пишутся на императивных языках программирования (вроде Solidity) и существуют отдельно от базового протокола, в Tau сам код блокчейна является контрактом, написанным на языке спецификаций. Это позволяет закладывать глобальные инварианты (например, «эмиссия токенов не может превысить $N$» или «баланс валидатора не может быть обнулен без подписи трех сторон») непосредственно в архитектуру сети, гарантируя их исполнение на математическом уровне.
В такой экосистеме становится возможной реализация концепции «автоматического бизнесмена» (automatic businessman). Пользователю достаточно неявно описать свои активы, глобальные цели и типы сделок, в которых он готов участвовать, после чего система сама начнет генерировать и исполнять безопасные смарт-контракты, приносящие прибыль везде, где это математически выполнимо.
Управление развитием софта в Tau строится через так называемые «карты мнений» (opinion maps). Пользователи ведут дискуссию на естественном языке, которая с помощью LLM-трансляторов переводится в строгие логические формулы Tau. Система автоматически вычисляет взаимные противоречия в требованиях участников. Точка пересечения, набравшая консенсус (правила которого также формализованы и могут быть изменены), автоматически становится следующим обновлением системы. При этом в Tau нет классического голосования большинством — управление может быть настроено как гибкая меритократия с делегированием голосов доверенным экспертам.
Отвечая на вопрос о текущей стадии проекта, Охад признает, что в прошлом был излишне оптимистичен по поводу сроков релиза. Полноценный запуск блокчейна еще не состоялся. На данный момент существует временный токен Agoras (AGRS), развернутый в сети Ethereum. После завершения разработки основного движка Tau все временные токены будут централизованно конвертированы в нативную монету новой сети. Развертывание планируется начать с публичного тестнета (testnet), который послужит безопасной песочницей, где пользователи смогут экспериментировать с правилами и перезапускать систему с нуля в случае логических тупиков.
В финале беседы Охад Асор подчеркивает, что его проект — это глобальный манифест против «иллогицизма» и бюрократии в экономике и общественной жизни. Современная финансовая и государственная системы, по его мнению, застряли в прошлом веке: элементарные процессы вроде уплаты налогов или международных банковских переводов требуют колоссального объема ручной работы, верификаций по телефону и бумажной волокиты. Механизация логики с помощью компьютеров способна навсегда искоренить эти неэффективные надстройки, доверив рутину безупречным математическим алгоритмам.
