Tau Language

Asor认为，机器学习始终是概率性的，最终会撞上难度阈值，因此不适合用于任何时候都不能违反规则的软件。 他称ML是“数学奇迹”，但强调其PAC上限：错误率永远不会降到0，确定性也永远不会达到1。对于足够大的SAT问题——以他举的例子来说是“数百个变量”——他认为即使是o3、o30或o300也会变成“抛硬币”，而专用SAT求解器可以处理数千个变量。

Tau提出的不是普通验证，而是软件合成：用户提出要求，只要规格可满足，系统就生成一个保证满足要求的软件。 用户不必编写银行代码、审计每一次余额更新，只需写下“余额大于等于0”。Asor的简洁表述是：“你只写测试”，计算机则生成一个对所有可能输入都能通过测试的程序。

其技术押注是，实用逻辑推理已经超越了支撑1970年代AI寒冬的悲观判断。 NP完全问题曾被认为即使在中等规模下也不可处理，但基于DPLL/CDCL的SAT求解器加上“一堆相当简单的启发式方法”，证明它们的效果出乎意料地好。Asor看到了一条经验上的“SAT求解器准摩尔定律”，因此现在正是重新投资逻辑AI的时点。

Tau声称的差异化在于，它可以通过布尔代数抽象引用自身的句子，同时避开Tarski定理所针对的无约束真谓词。 Asor把句子抽象成布尔代数元素，保留and、or、not和语义相等性等操作，同时丢弃内部结构。加入时间以及明确的输入和输出后，Tau可以检查是否对每个输入都存在满足规格的输出，并在条件成立时合成程序。

逐点修订旨在让合成软件无需全部重建也能继续编辑。 Tau优先选择同时满足旧规格和新规格的输出；如果不存在，就选择满足新规格的输出。这样用户可以局部控制，同时保留其余部分，不过Asor也承认，归一化可能产生看起来陌生的规格，性能、可读性和可解释性仍在持续改进。

区块链是Tau的旗舰应用，因为同一种语言可以定义合约、交易、治理，以及治理规则本身的修改。 Asor称Tau是“所有区块链的终局”：用户可以发布知识悬赏、定义可接受的交易，或告诉一个“自动商人”——“尽可能为我赚钱”。更深层的押注是由用户控制的软件，其治理规则以及“修改规则的规则”本身都可以改变。

尽管愿景广阔，执行风险仍然不小。 Asor说，他在访谈前约1个月敲定了完整的合成算法，但也表示目前实现的系统仍是解释器，合成尚未实现。在承认自己“过去过于乐观”后，他没有给出上线日期。AGRS目前是一个临时Ethereum代币，计划未来兑换为原生代币；项目计划先推出可重启的测试网，再上线主网。

🔗 原始收听与视频来源： Tau 语言：软件合成的未来 [赞助] - Ohad Asor