如果你让一个 AI 智能体去写张量运算代码十有八九会得到维度对不上的矩阵乘法如果你再要求它证明这段代码是对的它大概率会给出一个听起来合理、但根本站不住脚的解释。Chelis 这个项目把两件事揉进了同一种语言让 agent 既能编写张量程序也能在编译期完成正确性证明。它是一个面向智能体设计的可证明张量领域特定语言核心思路是把矩阵形状、数值范围这类约束变成类型系统的一部分再由内置的证明引擎去自动验证。这篇文章我会从设计动机讲到类型系统再带你把一个用 Chelis 写的张量程序从安装到跑通完整走一遍最后整理我在实际使用中踩过的坑。适合正在做 AI 编程工具的人、被 shape mismatch 折磨过的算法工程师以及所有对形式化验证感兴趣但被 Coq 吓退的读者。1. 为什么需要一门“可证明的张量语言”1.1 张量代码的痛点维度错误是运行时的幽灵张量这玩意儿说白了就是多维数组。0 维是标量1 维是向量2 维是矩阵3 维往上就是各种 batch、通道、序列叠加出来的高维数据。深度学习里几乎每个算子都在跟张量打交道而张量代码最常见的 bug 不是逻辑写错是形状对不上。我早期做机器学习平台时被这类问题坑过太多次。一次是线上推理的向量维度写死成 512结果某个模型换成 768 维 embedding 之后代码编译过了、模型也加载了跑到某一层才报 shape mismatch。一个需要在 GPU 上跑几小时的训练任务因为一个矩阵转置忘写前向传播算出来全是 NaN反向传播直接崩掉。这类错误在 Python 生态里几乎都是运行时才暴露NumPy 和 PyTorch 虽然会在执行时进行形状检查但那已经是错误发生之后的事了。如果把编程语言比作快递系统传统类型系统检查的是“包裹里是不是苹果”而张量形状检查要做的是“地址的门牌号是不是和收件人对应”。门牌号错了快递照样能送出去到了才发现送错楼——这就是运行时才报错的本质。你需要一个能在包裹贴上地址、还没发货之前就把门牌号核对清楚的机制。Chelis 想做的就是这个。1.2 让 agent 写代码更要让 agent 证明代码现在大模型生成的代码正确性是个大问题。让智能体写一个简单的矩阵乘法它知道输出形状是(m, n)但具体到某个分支、某个广播场景就会产生幻觉忘记转置、批处理维度顺序搞反、或者把(k, n)当成(n, k)传进去。代码能跑结果全错这类问题比“跑不起来”更隐蔽。测试当然能兜底一部分但测试只能覆盖你想到的输入。你在本地测了(3, 4) x (4, 5)线上来了个(3, 6) x (6, 5)代码崩了你又没测到。而且对大模型生成的代码来说常规的单元测试根本治不了“自信地错”的毛病——它能产出看起来完全合理的断言和测试用例因为生成的测试本身就带入了同样的幻觉。Chelis 给出的答案很直接让 agent 写代码的同时把“这段代码为什么是对的”也作为一等待办事项。agent 生成的不只是运算逻辑还有形状约束和不变量。这些约束不是给人类看的注释而是要被内置证明引擎真实验证的数学命题。证明通过了才允许编译证明不通过就把错误目标回传给 agent 让它修正。这样一来agent 的输出从“看起来对”变成了“可被机器验证地对”。1.3 与现有方案的对比类型系统、证明助手与张量库市面上其实不缺少能检查维度的工具但大部分都不适合做“agent 可编写可证明”这件事。Python 生态里的主流方案是运行时检查比如 PyTorch 的 assert。这类方案升级成本低但检查滞后且 agent 生成的代码经常绕过这些检查。Haskell 之类的强类型语言能做维度静态检查但表达张量形状和广播规则需要很重的类型级编程学习成本高而且大多数做机器学习的人根本不会用。依赖类型语言和证明助手比如 Agda、Coq、Idis 这一票确实能做到完整的形状级验证学术上很强但它们的证明脚本对 agent 而言极其不友好。Coq 的证明策略、反馈式证明、各种 tac 的组合连熟练的工程师都要反复查文档让大模型去写这些策略生成几百行之后错误信息密集到根本无法迭代。还有一类是专业张量 DSL比如 JAX 或 Dex。JAX 有静态形状检查Dex 在编译期做了很多形状推断但它们的目标不是“证明”而是“高性能计算”。它们的错误信息面向人类设计agent 读了之后很难形成修正循环。Chelis 的位置正好在中间语法像 Python 一样直白维度信息编码在类型里规则被约束成自动证明器能处理的范围而错误输出是结构化的、可被程序解析的便于 agent 快速理解并迭代修复。2. 语言设计核心拆解2.1 类型系统把维度变成类型的一部分Chelis 最核心的设计决策是把张量形状从运行时属性提升到类型层面。在 Chelis 里一个(3, 4)的浮点矩阵类型不是简单的Tensor而是Tensor[3, 4], f32。这个类型里写死了两个信息形状是[3, 4]元素类型是f32。如果只是写死具体数字那这套系统能干的活很有限。实际张量代码里有大量形状是由变量决定的一个 batch 大小可能是b序列长度可能是n这些在函数定义时还不知道具体值。所以 Chelis 支持类型级变量也就是维度多态。你可以写def batched_matmul(a : Tensor[b, m, k], f32, b : Tensor[b, k, n], f32) - Tensor[b, m, n], f32这个函数签名说了三件事输入是两个三维张量它们的 batch 维度相同内部矩阵形状满足矩阵乘法条件输出形状由输入形状完全决定。只要编译通过任何具体维度传进来都一定匹配。凭什么能保证因为编译器在检查函数体时会把你写的运算符对应到一组维度约束上。以矩阵乘法为例它的规则是左侧张量的最后一个维度必须等于右侧张量的倒数第二个维度。这个规则在 Chelis 里是一等公民约束。你写a b编译器就自动生成约束a.shape[-1] b.shape[-2]然后交给约束求解器去判断在当前类型环境下是否能满足。不光是形状元素值的范围也能变成类型约束。Chelis 支持细化类型refinement type可以在类型上附加谓词。比如def relu(x : Tensor[n], f32) - { r : Tensor[n], f32 | all(r, 0.0) }这个函数签名承诺的不只是形状不变还包括输出里的每个元素都大于等于 0。你可以在定义函数体时提供证明目标比如对每个位置i证明r[i] max(x[i], 0.0) 0.0。由于max的语义是取大这类目标自动证明器通常直接就能处理。2.2 证明模式自动证明与 agent 辅助证明结合类型系统给出了命题接下来要解决的是怎么证明。Chelis 的证明引擎不是让你手动写 Coq 策略而是分层降级优先用自动证明证明不了再把目标回传给 agent 做半自动辅助。自动证明层背后接的是 SMT 求解器。SMTSatisfiability Modulo Theories是个听起来唬人、思路其实很朴素的玩意儿给定一组约束判断是否存在一组取值让所有约束都成立。它擅长处理线性算术、等式、数组、位向量这类逻辑。张量形状约束绝大多数是线性表达式之间的等式和不等式比如m k 1、n 0、m * n k * k。这类目标对 Z3 之类的求解器来说几乎是热身运动。但现实项目里总有一些证明目标无法靠一句话的上下文自动闭合。比如你要证明矩阵乘法结合律或者要证明某个复杂 reshape 操作前后元素总数不变这时候只靠当前函数体的局部约束是不够的你需要额外的不变量。Chelis 允许你在函数体里显式写assert或invariant把缺失的前提补上。如果这些还不满足agent 可以介入读取求解器给出的未闭合目标和当前上下文补写引理或调整不变量。这套“自动为主、agent 为辅”的模式是我认为 Chelis 区别于传统证明助手的关键。用 Coq 证明一个张量性质可能要 50 行策略脚本Chelis 里绝大多数情况就是一行prove { ... }然后交给求解器。只有卡住的时候才需要更精细的人工干预这个“卡住”的时刻恰恰是 agent 能在旁边帮上忙的时刻。2.3 对 agent 友好的语言表面设计让 agent 能写、能改、能修语言表面设计很重要。Chelis 在语法上有几个很刻意的选择。第一语法表面积尽可能小。它几乎没有继承、重载、装饰器这类花哨特性核心语法就是类型标注、函数定义、张量展开、约束和证明块。token 消耗少大模型就不容易在语法细节上产生幻觉。第二运算符语义稳定。就是矩阵乘法*是逐元素乘法sum是沿轴归约不搞隐式广播花活。第三错误信息结构化。普通编译器输出的是一大段人类语言Chelis 除了给人看的提示还附带一份机器可读的错误摘要agent 可以通过简单的接口直接解析出错误类型、所在位置、未满足的约束表达式然后针对性修复不需要从自然语言里再猜测意图。我平时给 agent 写提示词时最怕的就是它把几百行上下文都吃掉。Chelis 把错误信息压缩成紧凑的结构化片段这在用智能体迭代代码时价值极大agent 看到的不是一篇小作文而是一张可以直接“照着改”的问题清单。3. 实操从零跑通一个可证明的张量程序3.1 环境搭建与最小示例我按当前常用的方式来说明安装流程。Chelis 的编译器本体是一个可执行文件安装后还需要一个 SMT 求解器作为后端。# 安装 Chelis 编译器 curl -sSL https://example.org/chelis/install.sh | bash # 安装 Z3 求解器后端 apt install z3装完验证一下chelise --version能看到版本号输出就说明编译器本体正常。接着建一个最小文件验证证明链路# hello.chelise def main() - Int { let a : Tensor[2, 3], f32 ones([2, 3]) let b : Tensor[3, 4], f32 ones([3, 4]) let c a b assert c.shape[0] 2 assert c.shape[1] 4 0 }保存后运行chelise build hello.chelise如果没有任何输出、退出码为 0说明两个维度的断言都被证明器自动验证了。注意a b本身会产生一个维度约束左矩阵的列数3必须等于右矩阵的行数3。这里满足了所以整个链路是通的。3.2 维度标注、细化类型与约束写法Chelis 里写张量函数有一条固定的套路能写成类型的别写在运行时里。函数签名里尽量把形状关系表达清楚函数体内才不需要堆一堆 if-else。看一个完整带证明的函数def softmax_zero_sum(x : Tensor[n], f32) - { r : Tensor[n], f32 | all(r, 0.0) } { let max_x max(x) let exp_x exp(x - max_x) let sum_x sum(exp_x) let r exp_x / sum_x prove { forall(i in 0..n - r[i] 0.0) } r }这个函数里有三个值得注意的点。第一返回类型带着一个细化条件all(r, 0.0)也就是承诺输出里所有元素非负。第二函数体内的prove块向证明器提交了一个目标对每个下标ir[i] 0.0成立。第三证明器要完成这个证明需要利用exp返回非负、sum返回非负、非负数除以非负数仍非负这些规则。如果你用的求解器配置合理这些在它的知识范围内可以直接闭合。如果求值器无法自动证明一个常见的处理方式是把中间结论显式写出来let exp_nonneg : Prop exp_x 0.0把这些中间条件补充进去之后证明器往往就能续上。3.3 一个会故意失败的例子以及报错解读光看成功路径不够我们来制造一个维度错误看看 Chelis 怎么报错。# wrong.chelise def main() - Int { let a : Tensor[3, 4], f32 ones([3, 4]) let b : Tensor[5, 6], f32 ones([5, 6]) let c a b 0 }编译它chelise build wrong.chelise你会看到类似这样的输出error[E003]: shape mismatch in at wrong.chelise:4:9 constraint: a.shape[1] b.shape[0] left side: 4 right side: 5 hint: consider transposing b or changing its declared type这个报错的含义一目了然第 4 行a b触发了矩阵乘法的形状约束左矩阵的列是 4右矩阵的行是 5两者不相等。编译器没有等你运行时爆炸它在编译期就把它挡下了。实际开发中我见过很多错误并不仅仅是一处维度不匹配而是多个约束互相打架。Chelis 的错误信息会把参与冲突的约束全部列出你要做的是挨个检查是声明类型写错了还是调用时传参顺序错了还是广播逻辑设计有误。多数情况是声明类型写错了因为推理出的类型往往是对的。3.4 让 agent 参与编写和证明的完整流程现在把 Chelis 和 agent 串起来跑一遍。我的做法是写一个简单的任务描述让 agent 生成代码然后让编译器检查失败就把结构化错误回传。任务示例实现一个支持 batch 的矩阵乘法输出形状为(b, m, n)。我给 agent 的提示词大致长这样用 Chelis 实现 batched_matmul。类型签名要求 batched_matmul(a : Tensor[b, m, k], f32, b : Tensor[b, k, n], f32) - Tensor[b, m, n], f32 函数体内直接用 完成计算并加一个证明块验证每个 batch 的输出形状。agent 第一次生成的代码可能长这样def batched_matmul(a : Tensor[b, m, k], f32, b : Tensor[b, k, n], f32) - Tensor[b, m, n], f32 { let r a b prove { r.shape[0] b r.shape[1] m r.shape[2] n } r }我把它喂给编译器结果报错prove块里的目标不能被直接证明因为当前上下文里缺少a b输出形状规则的具体展开。于是我把错误摘要回传给 agenterror[E003]: cannot prove target r.shape[0] b the target requires unfolding the definition of on batched inputsagent 读完之后把证明块改成利用类型注释的方式let r : Tensor[b, m, n], f32 a b prove { r.shape[0] b r.shape[1] m r.shape[2] n }这一版编译通过。整个过程只迭代了两轮。核心经验是给 agent 的结构化错误越精简迭代效率越高。一条条长篇英语解释反而会让模型分心错误摘要里只要包含错误类型、约束表达式、期望值、实际值agent 就能精准修正。4. 踩坑记录与排查技巧4.1 证明目标无法闭合时的处理路径自动证明失败是我遇到最多的情况。失败不等于代码真的错了往往是上下文中缺少某一个关键事实。我的排查顺序是这样的先看这个目标是不是在自动求解器的能力范围内超出范围的试着补一个中间断言补了还不行考虑是不是约束本身有歧义需要显式写出形状关系。具体来说如果证明块里出现一个涉及乘法和非线性的目标比如m * k k * m (m - m)求解器通常能处理但如果是m * d n k * k n这种真正的非线性问题SMT 求解器不保证能解出来。这时候要做的是“人肉化”把这个约束拆成几个更容易的引理。比如先把m * d k * k作为前提再证明两边加n后相等。我自己平时会给 agent 加一条规则如果证明器返回unknown或者timeout优先尝试增加类型约束而不是修改证明策略。因为类型约束会把问题域缩小求解器往往就活了。4.2 维度多态与具体类型的匹配问题维度多态是 Chelis 最强大的特性之一也是最容易踩坑的地方。类型变量之间的匹配关系如果不注意就会出现“已经具体化的维度”和“尚未确定的维度”互相冲突。我之前写过这样一个函数def concat_along_last(a : Tensor[m, n], f32, b : Tensor[m, n], f32, axis : Int) - Tensor[m, 2 * n], f32这里axis是个运行时整数但返回类型却把n升级成2 * n。问题来了如果调用方把axis设为 0返回值本质上不是[m, 2n]而是[2m, n]类型系统和实际计算结果就对不上了。Chelis 会拒绝这种方式因为axis不是类型级已知的常量。正确做法是把轴信息也类型化或者限制这个函数只支持固定轴。这个例子提醒我能放进类型的别放进运行时放进去的值必须参与证明而不是参与推断。4.3 与运行时边界什么时候信任证明什么时候不信任证明器再强也只能保证它视野范围内的约束。如果你的 Chelis 代码调用了外部库比如某个用 C 实现的张量算子那这个算子的行为就超出了证明器能检查的范围。Chelis 的做法是外部函数一律标记为不透明调用点的类型要你显式声明证明器信任这个声明而不做深入验证。这里有一个真实的信任边界问题。如果你把外部函数的返回类型乱填证明器会基于错误的前提继续证明最后产出一个“在虚假前提下成立的结论”。这不是 Chelis 的 bug而是任何带 FFI 的形式化系统都存在的边界。我的建议是凡是跨过外部边界的函数在实现处加运行时断言兜底。也就是说类型证明负责整个系统内部的正确性运行时不变量断言负责边界两层配合才安全。4.4 给 agent 的提示词与错误回传的配合技巧把 Chelis 接入 agent 工作流时有几个非常实际的经验我跟身边的朋友试了很多遍总结出来的。不要试图把完整语言手册塞进上下文。Chelis 的规范文档有几十页全放进去 token 开销大agent 反而抓不住重点。我通常只注入三样东西一个类型语法示例、一个约束写法示例、一个错误信息解析说明。这三个加起来不到 500 个 token效果远超完整手册。错误回传时要做减法。编译器的原生错误可能包含不少上下文对 agent 而言真正有用的只有错误类型、涉及约束、期望值和实际值。我写了一个简单的脚本把这些字段从错误输出里提取出来再拼接成一条紧凑的 JSON 塞回给 agent。实际测试下来这个流程比直接回传原始错误信息减少了差不多一半的迭代轮数。给 agent 设上限。不要让它在同一个证明目标上无限重试。我的规则是同一个错误类型出现三次就停止修改代码先检查类型签名是不是就错了。很多时候问题不在证明块而在函数签名本身。最后再分享一点我自己的体会Chelis 最打动我的地方不是它省掉了多少行代码而是它把“我猜对了”变成“我证明了”。在机器学习领域工作这些年我见过太多代码在测试集上跑得风生水起一到生产环境就被维度错误干翻事后定位还要靠肉眼比对输出日志。维度这类错误本质上是数学问题应该用数学方法在代码运行之前就解决掉。Chelis 提供的路径是可行的但也不完美SMT 求解器遇到非线性目标还是会卡住与现有深度学习框架的互操作层还比较薄用它做大型训练模型还不太现实。但如果说智能体编程是未来那智能体生产的代码必须在交付之前被验证——Chelis 至少让我看到了这个未来的一种合理的落地方式。如果你也深受张量 bug 困扰或者正在做 agent 编程工具链不妨拿它试一试。