Tau Language: Программируемое будущее или математическая утопия? 0:00
Машинное обучение совершило революцию, однако текущий подход — использование нейросетей для «угадывания» ответов на основе вероятностей — имеет фундаментальные ограничения, утверждает математик и разработчик Охад Асор. В интервью каналу Machine Learning Street Talk он представляет Tau Language: систему, основанную на строгой логике, которая позволяет пользователям напрямую определять поведение программ и получать математические гарантии их работы. По мнению Асора, нынешние методы ИИ достигли своего «плато», и будущее за системами, где логика не просто дополняет статистику, а становится фундаментом.
🌌 Три проклятия машинного обучения 0:15
Асор выделяет три фундаментальные проблемы, которые ограничивают эффективность современных нейросетей:
- Оптимизационное проклятие: сложность поиска глобального минимума функции потерь.
- Статистическое проклятие: необходимость огромных выборок данных и проблема переобучения.
- Аппроксимационное проклятие: невозможность гарантировать нулевую ошибку.
По словам Асора, машинное обучение — это «вероятностно-приблизительное обучение» (PAC learning), которое никогда не даст абсолютных гарантий правильности. Когда задача становится сложной (например, в задачах удовлетворения логических ограничений — SAT), нейросети при достижении определенного порога переменных начинают выдавать ответы не лучше, чем «подбрасывание монетки». Асор утверждает, что существующие языковые модели не «рассуждают», а лишь статистически имитируют процесс, лишенный контакта с реальностью.
🛠 Tau Language: логика как язык управления 21:23
В отличие от классических методов, Tau Language предлагает переход от верификации (проверки готового кода) к синтезу программ (автоматической генерации кода на основе требований).
- Принцип синтеза: Пользователь пишет спецификацию — требования к программе, а система автоматически создает исполняемый код, гарантированно соответствующий этим требованиям.
- Точка истины: В качестве основы для логических выводов используются булевы алгебры. Асор заявляет, что его система обходит знаменитую теорему Тарского о невыразимости истины, абстрагируя предложения до элементов булевой алгебры.
- Точечная ревизия (Pointwise revision): Уникальная возможность обновлять спецификацию программы «на лету», меняя только нужный фрагмент и сохраняя целостность всей остальной логики.
⛓ Блокчейн будущего 1:11:39
Асор позиционирует Tau как «финальную точку» (endgame) для всех блокчейнов. В его видении, существующие сети страдают от «хрупкости» кода и контроля со стороны узких групп разработчиков.
- Контроль пользователями: Вместо того чтобы полагаться на разработчиков, сообщество пользователей само определяет правила сети, которые превращаются в программный код через Tau.
- Автоматический бизнесмен: Возможность делегировать системе сложные финансовые задачи. Пользователь задает лишь цели (например, «получать прибыль»), а система находит оптимальные сделки в рамках установленных ограничений.
- Governance как софт: Governance-механизмы блокчейна сами являются программой на Tau, поэтому правила управления системой можно менять так же легко, как и любую другую часть софта.
⚖️ Риски и перспективы 1:28:33
Несмотря на амбициозность проекта, Асор признает, что перед пользователями встанет крутая кривая обучения. Хотя синтаксис языка минималистичен, понимание предметной области остается сложной задачей. Контраргумент, известный в сообществе: если система станет слишком сложной или «застывшей» в своих правилах, она может стать менее гибкой, чем традиционные методы.
По прогнозам разработчика, в будущем для преодоления барьера входа могут использоваться LLM, которые будут транслировать естественный язык человека в строгие спецификации Tau. На текущий момент проект находится на стадии разработки: основная логика «движка» готова, но внедрение и синтез программ остаются задачами для дальнейшей оптимизации.