Tau 语言：软件合成的未来 [赞助] - Ohad Asor

摘要

• 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代币，计划未来兑换为原生代币；项目计划先推出可重启的测试网，再上线主网。

精读

1. 统计准确率永远不会成为正确性保证

• Asor并非一上来否定机器学习，而是先表达赞赏：机器学习可以从从未见过的样本中泛化，这被他称为“数学奇迹”。但PAC学习承诺的只有“可能大致正确”；错误率既不可能为0，正确概率也不可能达到1。

• 他更强的判断是，准确率只会提升到某个问题复杂度阈值。超过这一阈值后，模型可能变得像随机猜测，尤其是在要求所有约束同时成立的结构化逻辑问题上。

• 他举的具体例子是布尔可满足性：例如“如果A出席且B不出席，那么C出席”这类聚会规则。SAT求解器可以处理数千个变量，而Asor预计，变量达到数百个后，即使是o3、o30或o300也只能提供“抛硬币”级别的结果。

• 多项式插值提供了一个类比：用一个1,000次多项式拟合1,000个任意点，下一个点仍然无法预测。无限制的概念类拥有无限VC维度；完美拟合意味着过拟合，而不是泛化能力的证据。

2. Tim的变换挑战揭示了真正的取舍

• Tim以o系列模型的进步，以及近期围绕François Chollet的ARC挑战所做的变换研究提出反驳：把测试实例的信息放进预测函数，拥抱情境化的复杂性，而不是只依赖一个被训练来泛化至未见样本的归纳模型。

• Asor的回答是，改变构造预测函数的路径，并不会消除计算上的限制。如果概念类包含能够拟合一切的任意多项式，那么在任意数据上插值仍然没有预测能力。

• 更小的概念类可能无法拟合训练数据；如果它确实拟合成功，Asor说，这只能带来更高的信心，而不是对样本外表现的保证。

• Tim点出了3重困境——优化、统计和逼近的诅咒——随后追问逻辑牺牲了什么。Asor的简短答案是：“信息必须在那里。”当要求能够被陈述时，逻辑才有效；而当手头只有样本时，机器学习仍然有价值。

3. 逻辑适用于可定义规则，机器学习填补无法陈述规则的空白

• 人脸识别是Asor举出的典型机器学习案例：人们可以立即认出一张脸，却无法用语言充分描述识别规则。当定义不可得时，样本加上一个不那么准确的统计系统，仍可能“聊胜于无”。

• 对于能够表达的规则，他认为通过线性代数进行间接编码没有必要。机器学习仍可以嵌入更大的逻辑系统：先用逻辑描述算法，再把其中负责猜测的部分与约束软件其余部分的确定性要求结合起来。

• 这一区分背后还有一层哲学分野：“指向月亮的手指不是月亮。”语言可以指向物理现实，却永远无法触及现实本身；但人类高度生活在概念中，并通过语言与计算机沟通，因此符号表达是服务人类目标的系统最自然的接口。

4. 合成用关于行为的陈述取代实现

• Asor认为验证已经是“老新闻”。验证从一个系统出发，检查关于该系统的命题；合成则只提供命题或要求，并自动生成满足这些要求的系统。

• 编程上的类比是只写测试、不写应用。与其手工实现代码再检查，不如“只写测试”，之后由计算机合成一个能让测试通过的程序。

• 一部手机如果必须永远不能传输密码，就需要普遍性保证：概念上，要对所有可能的输入和配置进行量化。Asor明确表示，按字面描述的方式无法实现这一测试，但合适的数学框架可以在无限域上证明性质并提供保证。

• Tim反驳说，密码可能以无穷多种未预见的方式编码。Asor同意这种情况可能发生，表示密码只是一个例子，并重申重点是借助特定数学框架，对所有相关系统配置和输入陈述性质。

5. 关键软件凸显需求为何重要

• 对于银行软件，Asor问道，谁会把整家银行交给o3模型？他说，即使是最热情的LLM拥护者也不会。传统程序员则会检查每一次显式和隐式的余额变动，但仍然可能遗漏。

• 在Tau中，预期的替代方案是写下“余额大于等于0”。此前的银行规则包含一个授权例外，但“苏黎世银行家”的思想实验把讨论从编写软件推进到了修改软件规格。

• 合成出来的实现可以不同，但任何符合规格的实现都必须遵守形式化条件。Asor表示，Tau的合成框架就是为了处理这类规格更新，而不是假定第一次形式化永远足够。

6. 边界由可定义性划定，而不是由完整世界模型划定

• Tim提到1980年代专家系统的瓶颈：规则不断累积特例，最终变成难以管理且脆弱的本体。Asor拒绝接受Tau应当全面描述现实这一前提：“我无意描述整个真实世界”；它只需要捕捉计算机为实现人类目标必须完成的事情。

• 他区分了3种限制。形式语言只有可数多个有限句子，因此大多数数学结构都不可定义。可计算性理论排除了停机问题等问题；可计算数是可数的，而几乎所有实数都不可计算。物理现实更严格，因为连“物理上存在”都无法精确定义。

• Asor明确区分了计算机世界与人类和物理世界：他说自己知道如何处理前者，但后两者超出了他的能力范围。

• 只有在所需行为已知的情况下，编程语言才能表达计算机可以完成的一切。如果“种族主义表述”无法定义，就无法为检测它写出形式化保证；用户可以改为提供样本，并接受一个不那么准确的概率系统。

7. SAT求解器改变了逻辑AI的实用性判断

• Asor把1970年代逻辑AI的寒冬追溯到Lighthill辩论，以及人们相信NP完全推理即使在小规模下也无法使用。他说，这一信念没有理论证明，而大型SAT实例此后提供了经验上的证据，说明当时的悲观判断并不准确。

• 突破并不华丽：DPLL与CDCL结合，再加上“一堆相当简单的启发式方法”，却意外地奏效。Asor说，没有人完全知道它们为何表现如此出色，但求解器能力仍在持续提升，像一条“SAT求解器的准摩尔定律”。

• Tim将这一逆转与深度学习在GPU、数据和算法变化之后的复兴相比较。Asor明确得出投资结论：逻辑AI被放弃，是因为人们认为它计算上过于困难，而不是因为它缺乏潜力；如今的实践证据已经足以支持重新建设和研究。

8. 布尔抽象赋予Tau受限的自指能力

• Asor说，一个能够引用同一语言中句子的语言，是安全AI不可或缺的能力。传统逻辑AI和逻辑框架在没有相应额外组件的情况下也缺乏这一能力。他声称自己是唯一发现这一特定解决方案的人。

• 按Asor的描述，Tarski难题出现在算术获得真谓词时：该谓词接收句子的Gödel编号，并宣告其为真或假。只要在语言内部假定这样一个谓词，就可能产生矛盾，使每个陈述及其否定都可被证明。

• Tau避免把句子的完整结构带入自指。它只把句子视为支持and、or、not和语义相等性的布尔代数元素——类似于只允许并集、交集、补集和相等、却不能检查成员关系的集合。

• Asor的关键限制是，Tau只有通过这一布尔接口，才能成为自己的元语言。“我们忘掉句子的结构”，只保留一种他认为足以实现实用自指、又不会重新制造无约束真谓词的抽象。

9. 时间、输入和输出让代数变成软件

• Tau扩展了标准布尔代数理论：它允许引用任意代数元素，而不只是0和1，并把底层代数设为Tau自身句子的集合。

• 随后它加入时间，允许把当前陈述与5步之前的陈述进行比较，并区分输入和输出。正是这些扩展，把逻辑语言变成了软件规格语言。

• Tim最初将Tau描述为对每个输入都保证存在匹配输出；Asor纠正了他。Tau首先检查可满足性：在每个时点，对所有输入，都必须存在满足规格的输出。只有这一性质成立时，它才能在Tau句子的无限域上合成符合规格的程序。

10. 无限实现空间可处理，但效率仍未解决

• 合成不会枚举每一个程序，因为程序空间是无限的。Asor将其比作证明一个非常数复多项式存在一个零点，或选择一个大于10的数：数学可以证明存在性并构造一个例子，而无需扫描无限域。

• Tau最初是一个能够执行规格的解释器。Asor说，完整合成算法在访谈前约1个月完成，但也表示目前实现的系统仍是解释器，合成尚未实现。目标输出语言是C++，不过原则上任何图灵完备的目标语言都可以。

• 一个规格通常对应无穷多个程序。如果后端的任意选择不可接受，用户就必须增加约束。后续行为可能暴露出需求缺失，也可能说明世界已经发生变化。

• 效率是一个“很大的难题”。计划是识别简单案例、提前求解逻辑，并输出直观的输入—输出函数；SAT或SMT求解器或许能提供帮助，但Asor并不确定。最坏情况下，程序复杂度会随规格大小增长，而优化、可读性和可解释性仍在持续推进。

11. 逐点修订尽可能保留旧行为

• 一般性的信念修订无法解决：给定A→C、B→C，以及新信息¬C，可以删除任意一个蕴含，也可以推导¬A或¬B，没有一种选择在所有情况下都最优。

• 软件输出提供了一个更窄的目标。Tau会在存在这种输出时，选择同时满足旧规格和新规格的输出；否则就只选择满足新规格的输出。用户只需陈述发生了什么变化，其余部分保持不变。

• Asor说，逐点修订一旦看明白，就会显得“非常容易”。无原子布尔代数中的量词消去可以移除存在量词，归一化则可以合并冗余，有时能把一份庞大的规格压缩成一行。

• Tim担心优化会抹去开发者心中的来路。Asor承认，归一化后的规格可能更难理解：解释器和编译器会在内部重写代码，但Tau的重写结果只有在某些时候更好；而数学上并不存在一个关于可理解性的定义，可以提供神奇的补救。

12. 用户控制最终走向可变治理与可编程货币

• Tau的设计目标是“1个且只有1个目标”：由用户控制的软件。Asor的绝对化表述是：“我是用户；我的计算机由我做主。”对于真正由用户控制的软件，他说，使用T技术“别无选择”。

• 集体控制还延伸到“修改规则的规则”。这不必意味着每个人拥有相同影响力——用户可以把自己的声音委托给信任的专家，从而形成精英治理；治理机制本身也可以被修改，或被设计成抵抗未来的修改。

• “Tau是一场关于Tau的讨论”：观点图记录讨论中的观点，包括哪些观点相互矛盾；讨论形成的共识成为软件更新，甚至共识的定义也可以配置。Asor承认，演化路径可能陷入僵局或变得僵化；逻辑保证和经济激励可以降低风险，但无法消除风险。

• 主持人认为区块链需要Tau；Asor同意，区块链需要Tau，以便随着时间推移由用户重新定义。Tau是旗舰特例：它的语言可以定义区块链、区块链合约，以及修改这些规则的规则。现有智能合约语言是编程语言，而Tau的目标是在同一层级上规定区块链和合约的行为。

• 预设应用包括知识悬赏，以及一个被赋予资产、目标结果和可接受交易的“自动商人”。用户可以说“为我赚钱”，而Asor保留了关键限定——“尽可能如此”；系统的目标是生成适用的行为。

• 产品准备度落后于理论。AGRS目前是一个临时Ethereum代币，计划未来进行兑换；Asor没有给出上线日期，并预计用户会阻止分叉；项目计划先推出一个陷入治理僵局后可以重启的假币测试网，再把规则迁移到主网。

• 他更广泛的经济论点是自动化：税收、会计、转账和金融工作流都可以编程，而不是被困在2025年的文书和人工流程中。被问到人工检查是否能阻止欺诈时，他没有声称自己知道答案；他更窄的主张是，无论哪里出现“非逻辑主义”，都应当与之斗争。