不变量The Invariant — when agents leave the chat box

先解释一个词，免得后面绕不开它。证明助手（proof assistant）是一种很特别的编程语言：你不仅写代码，还要写一份“为什么这段代码满足规格”的数学证明，而机器会逐行去验这份证明。Lean 4 就是这类系统里最近最受关注的一个。它的逻辑很硬：如果证明能通过，意思不是“我试了很多次没坏”，而是“在规格覆盖的所有输入里，这个结论都成立”。

这和测试的差别，不是勤奋程度的差别，而是世界观的差别。测试像拿手电照仓库：你照到的地方没老鼠，但黑暗里还有没有，不知道。证明像把仓库的平面图、墙体、门锁、所有通道都形式化，然后让一个不会通融的检查器说：这条路根本不存在。

形式化验证以前很贵。写 Lean 证明难到什么程度？许多数学家和工程师都能读懂一个定理或一个算法，却未必能把它变成机器愿意接受的证明。Mistral 在 3 月发布的 Leanstral，把自己定位成第一个面向 Lean 4 的开源代码 agent，目标就是“proof engineering”：不只生成代码，还要围绕严格规格做形式化证明。Mistral 的说明里把瓶颈说得很直：在高风险数学和关键软件里，人工验证已经成了工程速度的阻抗。

DeepMind 的 AlphaProof 论文也走在这条线上：它把 Lean 当成一个可验证环境，让 agent 在其中寻找形式化证明；2026 年 5 月的 AlphaProof Nexus 工作进一步把这件事推向研究级开放问题，报告称 full-featured agent 在 353 个形式化 Erdős 问题里解决了 9 个，并且公开了 Lean 证明。

但真正刺到我的，不是这些战绩，而是它暴露出的角色问题。一个会执行的编码 agent，外面套着能读写文件、运行命令、反复试错的 harness，确实更会把事情往前推；可“往前推”本身带着危险：它太想收尾，太想把红灯变绿。你给它一个不完整的命题，它有时会把洞藏进一个漂亮的结构里，仿佛工作已经完成。

“会干活的”和“会判断对不对的”，是两种能力。把它们放在同一个急于交差的 agent 身上，等于让被告兼任法官。

想象一个看起来很简单的需求：做一个“周报 agent”，每周五自动总结销售、客户、库存、会议纪要，再给管理层生成一页报告。老板觉得这就是把模型接上邮箱、CRM、数据仓库和文档库。真正做过的人知道，第一周就会撞墙。

客户在销售系统里叫 ACME China，合同系统里叫 ACME CN Ltd.，财务系统里叫“艾克米中国”。会议纪要里销售说“那个大客户”，客户成功说“华东续约项目”，老板说“上次你们提的那个风险”。这些不是模型不聪明，而是公司世界本来就是一堆别名、权限、历史包袱和人类偷懒的简称。

具体一点。周五下午四点，销售 VP 在聊天框里丢下一句：“把 ACME 的续约风险写进周报，顺便加上客户会上提到的价格阻力。”agent 很勤快：它从 CRM 里拿到 ACME China 的 pipeline，从合同库里找到 ACME CN Ltd. 的续约日期，从 Teams 会议纪要里摘出“华东试点暂停”，又从财务系统里查到集团层面的账期延长。十分钟后，它给管理层写了一句漂亮但危险的话：“ACME 集团续约风险升高，华东试点暂停，价格谈判受阻。”

这里缺的不是写作能力，而是一张公司地图：谁是母公司，谁是子公司；哪个项目名对应哪个 account；哪份会议纪要属于哪个 opportunity；哪类财务字段只能在什么权限下进入管理层周报；一个简称到底指客户、项目、地区，还是某个销售口头禅。人类靠经验和八卦补洞，agent 不会。

Microsoft 的 Work IQ 值得看，不是因为它又多了几个 API，而是因为它把“公司上下文”当成 agent 的基础设施来做。官方说法是：Work IQ 提供 workplace intelligence layer，让 agent 访问并推理组织数据、上下文和工具，同时内置权限感知治理；它把 chat、context、tools、workspaces 放到同一层，给长任务一个持续空间。

它最有工程味的设计，是把 Work IQ MCP 的操作面收缩成 10 个左右的通用工具，用 getSchema 在运行时让 agent 理解数据结构；权限上也不是堆几百个静态 OAuth scope，而是用 Rego-based policy engine 对每次请求按资源路径、方法、用户身份、数据内容做判断，并记录每次工具调用。

一个好 agent 不是“什么都能访问”。一个好 agent 是“知道此刻该访问什么，并且知道哪扇门永远不该开”。

再讲一个更危险的合成 case。一个数据 analyst agent 接到请求：“帮我分析高价值客户的投诉率，看看哪些区域风险最高。”它生成 SQL，跑出结果。语法正确，数字也对。大家以为事情完成了。

但这条 SQL 为了凑齐分析，把客户交易表、投诉表、医疗附加险字段、客服备注和某个内部风险标签 join 到了一起。单独看，每张表它都有权限；组合在一起，就变成一个不该被普通业务人员看到的敏感画像。

把场景落到一个保险运营团队。区域经理想知道：“高净值客户里，哪些城市最近投诉率异常？”agent 生成的查询并不离谱：先从客户表筛出 lifetime value 最高的客户，再 join 工单表看投诉，再 join 保单附加险表区分产品类型，最后 join 一个内部风险标签表，想把“容易升级成舆情”的客户排出来。

这段 SQL 的麻烦不在语法。第一，health_rider 暴露了敏感健康相关属性；第二，post_claim_label 是理赔后才生成的标签，拿来解释理赔前投诉风险会偷看未来；第三，报表按城市和产品线切得太细，有些格子只有两三个人，即使没有姓名，也足够让一线团队猜出是谁。于是一个“区域投诉率”报表，悄悄变成了健康画像、时间线泄漏和小样本再识别的混合物。

传统权限系统常问的是：“你能不能看这张表？”agent 时代更棘手的问题是：“你能看 A，也能看 B；但你能不能把 A 和 B 按这种方式合并？合并后的结果能不能发给这个人？”

这就是论文 Data Flow Control: Data Safety Policies for AI Agents 的核心。作者说，agent 越来越会生成 SQL、编排数据管道、自动做分析；可查询“正确”不等于查询“安全”。他们提出的 DFC 把策略下沉到 DBMS 查询层，对记录级数据流做约束；Passant 作为可移植查询重写层，在 DuckDB、Umbra、PostgreSQL、DataFusion 和 SQL Server 上测试，论文报告约 0% 额外开销。

不要让 prompt 负责所有安全。能沉到数据库层的规则，就不要留在一句“请勿泄露隐私”里祈祷。

很多 agent 项目都会经历一个幼稚期：模型犯一次错，就往 prompt 里加一句规则。第一次：“以后遇到空值要小心。”第二次：“聚合前检查粒度。”第三次：“用户问财年要确认 fiscal calendar。”一个月后，prompt 像发霉的冰箱贴，到处都是“注意”“小心”“必须确保”，每一句都有来历，但模型不知道什么时候该用哪一句。

我更喜欢把经验做成 skill。这里的 skill 不神秘，就是一张可调用的工序卡：什么时候适用，要调用什么工具，检查哪些前置条件，常见失败是什么，如何验证结果。

DataCOPE 做的是无监督 skill discovery：让数据分析 agent 从自己的探索轨迹里发现可复用技能。报告式分析用 Adaptive Checklist Verifier，推理式分析用 Answer Agreement Verifier；论文报告，在四种模型设置平均下，报告式任务提升 9.71%，推理式任务提升 32.30%。

SciVisAgentSkills 则把这个想法放进科学可视化：ParaView、napari、VMD、TTK 这些工具不是会叫名字就能用。论文把环境假设、工具使用模式、领域启发写成技能包，在 108 个专家设计的多步骤任务上测试，并强调 skills 的效果还要和 harness 一起看。换句话说，技能不是魔法咒语，它要被正确加载、缓存、执行和恢复。

prompt 是一张纸；skill registry 是一间档案室。一个会变旧，一个能归档、晋升、废弃和复用。

Hugging Face 给 Reachy Mini 加 MCP remote tools，表面看是个轻巧的小新闻：桌面机器人现在可以通过 Hugging Face Spaces 调用天气、搜索这类远程工具，不必改本地 app。真正值得看的是它的权限结构。

Reachy Mini 的身体工具——转头、跳舞、表情、摄像头、头部跟踪——留在本地；远程工具作为可选能力安装到 profile 里，由 tools.txt 决定是否启用。文章里有一句很工程：tools.txt 是 gatekeeper。也就是说，机器人不是看到一个工具就能用，而是先经过一层明确的能力清单。

这件事一旦从聊天框转到机器人身上，就变得很现实。聊天机器人乱调用天气工具，最多答错；实体机器人乱调用动作工具，可能撞倒杯子、吓到孩子、夹到手指。Hugging Face 那篇文章还写得很诚实：prompt 可以鼓励并行调用天气和搜索，但不能保证并行；如果确定性编排重要，就该把逻辑从 prompt 移到代码里。

同一条线还有 Holo3.1 和 LeRobot Humanoid。Holo3.1 把 computer-use agent 推向本地和移动端：AndroidWorld 上 35B-A3B 从 67% 提升到 79.3%，并发布 FP8、Q4 GGUF、NVFP4 量化权重，面向本地推理。LeRobot Humanoid 则释放了一个低成本、3D 打印的人形机器人学习平台，当前双足平台零件成本约 2,500 美元，并给出硬件、装配文档、运行时、识别工具和训练环境。

AI 出屏幕以后，能力必须能被安装、禁用、审计、修理和替换。否则它不是平台，是魔术。

金融是最容易被 AI 幻觉迷惑的领域之一，因为金融语言本来就长得很像“有道理”。模型说一句“该因子捕捉了盈利修复的滞后反应，并在低波动环境中体现出横截面区分能力”，听起来像投研；也可能只是高级版算命。

这周的几条金融 AI 线索，正好能拼出第二阶段的要求。YouZhi-LLM 关注的是高并发金融推理：论文说 KV cache 内存开销限制了金融 LLM 的部署并发和成本；YouZhi-7B 在金融 benchmark 平均分上提升 12.3%，同时最大并发提升 2.69 倍；YouZhi-14B 提升 7.0% 准确率和 2.43 倍并发。

AlphaEval 关注的是 alpha 信号评价。它不满足于只看回测和相关性，而是把 generated alphas 放到五个维度里看：预测能力、稳定性、市场扰动鲁棒性、金融逻辑和多样性。FinBloom 则从实时信息切入：金融 LLM 要处理新闻、价格、filings 这类随时变化的数据，它提出的 Financial Context Dataset 超过 50,000 个金融查询，并用 1400 万金融新闻和 1200 万 SEC filings 的部分样本做训练材料。

合成一个投研 case：自动 alpha 挖掘系统发现一个新信号，过去 18 个月回测曲线漂亮得像广告。真正的审计不会先鼓掌，而会问：这个订单流字段在交易前真的能拿到吗？新闻情绪时间戳有没有延迟？小盘股成交量够不够？换手成本算了吗？为什么这个信号有经济含义？它是不是只在某个奇怪市场阶段有效？

金融里最危险的不是模型不会说金融话，而是它说得太像金融话，以至于你忘了让它把时间线和机制讲清楚。