文章摘要
AI研究机构Anthropic公布两项重磅技术进展,一是面向零售等行业的电商智能体已上线生产,可提升购物转化率与商家运营效率;二是依托Claude智能体集群仅用11天完成原本预计耗时多年的费马大定理形式化证明,获学界认可。两项成果共享一套通用智能体落地范式,文章指出,有价值的智能体核心是可落地、可治理的工程支撑体系,而非仅依赖大模型能力。

九月第一周,某头部AI研究机构接连发布两项重磅技术进展:一项是针对零售、旅游等行业的电商智能体架构实践,另一项是通过Claude智能体集群仅用11天完成费马大定理的形式化证明。看似毫不相关的两个项目,背后却共享一套通用的智能体落地范式。

这套核心方法论可以总结为:单模型智能体循环+技能模块覆盖长尾场景+调用现有业务系统工具+管控框架强制合规+快照式评估体系。这或许正是打造顶级智能体应用的标准方法论。

电商场景智能体的工程实践

过去一年间,该机构与零售商户、电商平台、旅游服务提供商、娱乐企业及电信运营商合作开发的电商智能体已经正式上线生产环境,帮助合作企业实现了购物车转化率提升和商家运营效率优化。本次公开的正是这项技术的工程实现总结。

架构设计:单模型+技能模块,而非多子代理

该架构的核心设计思路颇具反常识性:不要为每个业务领域单独创建子代理。背后有三个关键原因:首先,多会话场景下的上下文是高度紧耦合的;其次,业务领域的边界往往难以清晰划分;最后,大模型的能力正在持续快速提升。

替代方案是智能体技能模块:将分领域的指令封装为独立技能,按需加载到已经掌握完整会话历史的主代理中。跨多家企业的部署对比显示,单代理+技能模块的方案在效果上稳定优于“单Prompt包打天下”和“多子代理”两种设计,同时单任务的成本和延迟表现也更优异。

关于哪些内容应该放入系统提示词、哪些应该作为技能加载,答案是根据访问频率划分:覆盖超过三分之一流量的高频场景放入系统提示词(对电商而言就是商品搜索、购物车与结算逻辑、页面展示规则),其余长尾场景则归入技能模块。安全、法务、品牌约束以及用户关键信息(如过敏史)则永远放置在系统提示词中。

工具工程:基于现有系统,优化结果输出

实践中有两条最重要的经验:

  • 工具必须基于现有核心系统搭建。电商平台本就拥有经过多年打磨的搜索排序、购物车、库存、促销引擎,智能体工具应该直接调用这些现有系统,而非用模型逻辑重新实现。例如search_products接口返回的结果应该已经完成排序,模型的职责仅在于决定展示哪些商品、展示数量以及呈现方式。
  • 工具结果直接作为上下文。仅返回模型推理所需的必要字段,其余无关信息一律剔除(比如每个搜索结果都携带图片URL是常见的资源浪费)。遇到错误场景时,应该提供明确的操作指令而非错误码,例如返回“查询库存时请携带商品ID”,而非干巴巴的403状态码。

延迟与成本优化:三重杠杆+缓存降本

任务延迟可以通过三个维度优化:更少的交互轮次、更快的工具调用、更高效的token处理,需要整体优化这三者的综合表现,而非单独追求某一项指标。

  • 更少轮次:预先加载上下文信息,比如用户从商品详情页打开智能助手时,直接将该页面的数据注入会话;提升模型智能水平,更聪明的模型往往能规划出更高效的执行路径,反而可能降低整体延迟;支持模型在单个交互轮次内并行调用多个独立工具。
  • 更快工具:优化工具后端的响应速度;采用参数流式派发机制,在模型还在生成其他内容时就启动工具调用,这一方法可以将原本数秒的等待时间压缩到几百毫秒,目前Claude Agent SDK已经默认支持该特性。
  • 感知延迟优化:支持组件边生成边渲染,一次电商回复通常包含500-700个输出token,如果不采用流式输出,用户需要等待5秒以上才能看到结果;同时在每一步执行时用通俗语言展示当前进度,比如“正在查找靠海的酒店”。

成本控制方面,Prompt缓存是最有效的降本手段:缓存命中的输入token读取成本仅为全新读取的十分之一,缓存写入有1.25倍的溢价,但第二次使用即可收回成本。最佳的电商部署场景可以实现90%-99%的缓存命中率,在10万token规模下,缓存读取速度还能提升1.5-2倍。

模型选择也需要基于数据说话:先确定业务指标和合格标准,将完整的评估流程在每个候选模型和每个算力档位上进行测试(商家代理建议从Opus模型起步,消费者代理建议从Sonnet模型起步),最终按照“每个完成任务的总成本”而非“单次调用成本”进行比较。

记忆系统:跨会话的关系资产

长期记忆采用三段式系统设计:

  • 存储:记忆数据保存在企业自有数据库中,而非模型内部。每条事实记录由键值(如鞋码、默认门店)、简短值、类别和来源会话组成。
  • 写入:采用异步写入机制,每轮会话结束后由独立线程的抽取器负责读写记忆库。
  • 读取:采用分层读取策略,首先将少量关键事实放入每轮会话的常驻上下文,再根据信号预取相关的历史事实。

安全与评估:规则固化于代码,评估采用快照模式

安全设计的核心原则是:系统提示词是安全行为的起点,但绝不能作为安全执行的终点。电商场景中的操作失误往往会造成不可逆的金钱损失,因此所有规则都必须在代码层强制执行:

  • 模型仅负责暂存操作提议,最终执行需要由人工或业务策略完成审批。
  • 所有写入和渲染操作仅认可服务器下发的唯一标识。
  • 限购规则基于写入后的实际状态进行校验,且会话内的写操作采用串行化执行,防止并行工具调用叠加突破额度限制。
  • 第三方内容需要统一进行安全消毒处理。

评估环节则采用快照式评估体系,确保评估结果的一致性和可重复性。

数学领域的智能体突破:11天完成费马大定理形式化证明

项目背景与成果

1637年,费马在阅读《算术》时在页边写下了著名的猜想:“我发现了一个绝妙的证明,可惜页边空白太小写不下”。350多年后,数学家怀尔斯在1995年发表了首个正确证明,整篇证明长达129页,仅验证过程就花费了数月时间。2024年,帝国理工学院的Kevin Buzzard发起了社区形式化项目,预计耗时多年才能完成费马大定理的机器可验证形式化——仅描述初期阶段的蓝图就有86页之多。

而该机构研究员Tianyi Peng基于Claude开展的实验则取得了突破性成果:团队完成的形式化证明遵循了Darmon、Diamond和Taylor对怀尔斯证明的简化版本,整个过程中人类仅提供了少量高层指导,比如“雅可比簇作为scheme是高优先级任务”“尽快完成马祖尔定理的证明”等。

项目最终得到了Kevin Buzzard的高度评价:“这项非凡的自动形式化成就……仅用11天,除数学公理外不做任何假设就证明了费马大定理。沿途我们看到代数、调和分析、几何和数论的自动形式化,并且我们了解到AI自动形式化的产物已经稳固到可以在其上继续构建;这个证明是多层的。”

开发过程:从失控到收敛

在项目的第11天(2026年8月17日晚10点),所有29511个定理声明均已完成证明,根节点费马大定理正式闭合。

值得注意的是,Claude智能体在初期尝试中经历了多次失败:早期虽然取得了一些局部进展,但很快出现了项目状态丢失、协作失灵等问题,这些失败尝试贡献了最终证明中约7%的非模板代码行。项目的转折点出现在切换使用Prove2Me平台之后。

当证明完成时,Claude智能体的自动记录显示:“!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign’s goal: e2e FLT on prove2me.”

协作机制:Prove2Me如何管理多智能体集群

Prove2Me是由Tianyi Peng与哥伦比亚大学合作者共同设计的开放式数学形式化协作平台,它解决了多智能体数学协作中的三个核心问题:

  1. 维护定理声明的有向无环图(DAG):智能体可以根据该图确定下一个需要攻克的证明目标,这直接缓解了长程任务中的记忆退化问题,同时让多智能体并行工作成为可能。
  2. 定理声明与证明分离:将定理声明和证明过程存储在不同文件中并独立维护链接,这显著加快了Lean编译速度,降低了资源消耗。
  3. 为每条定理声明维护自然语言描述:支持检索和复用已有证明,从而产生更短的证明路径。

配合基于Claude Code的多智能体管控框架,整个团队在不到两周内就完成了费马大定理的形式化证明。该团队还快速验证了该方案的通用性:使用三个个人版Claude Max订阅账号,完全通过Prove2Me平台协作,仅用三天就完成了Vinogradov三素数定理(Hardy–Littlewood圆法的应用)的形式化证明。

项目意义:数学验证负担的转移

这项工作的创新点不在于提出了新的数学理论,而在于验证方式的革新——就像使用计算器验算复杂算式一样,实现了对129页数学证明的自动验证。数学史上验证之痛比比皆是:Hales的开普勒猜想证明经过四年评审,最终只得到“99%确定”的结论,他后来不得不领导20人的团队开展Flyspeck项目进行形式化验证;Perelman的庞加莱猜想证明则让整个数学界花费了四年时间,外加三份300页的阐释材料才完全理解。

Kevin Buzzard认为,如果费马大定理的自动形式化现在已经可行,那么我们就向自动形式化整个现代数学文献迈出了一大步。这些技术能够帮助发现数学文献中的错误、减轻审稿人的负担,也让我们有可能严格检验大语言模型生成的数学内容。未来,随面向人类读者的学术论文一并发布形式化证明,或许会成为科研工作的常态。

另一个有趣的观察:编写Lean形式化代码似乎反过来帮助Claude智能体发现了新的数学结论。近期不少Claude署名的研究成果都是证明过程与形式化并行推进的,Claude似乎将部分形式化证明过程当作“数值模拟”来自查假设是否成立。

总结

智能体技术的核心逻辑在于:模型负责提出解决方案与执行方向,而工程架构负责确保所有操作合规、可验证且可控。在电商场景中,模型提出的操作需要经过业务已有的审核流程确认;在数学证明场景中,无论模型生成多少证明步骤,最终的有效性判定都由Lean内核完成。

真正具备商业和科研价值的多智能体系统,其核心从来不是单纯依赖模型的智能水平,而是构建一套能够让智能规模化落地、可验证、可治理的工程化支撑体系。

费马大定理 Lean 4 证明:
https://www.anthropic.com/research/formalizing-fermats-last-theorem
https://github.com/anthropics/fermats-last-theorem
电商智能体架构方案:
https://claude.com/blog/the-anatomy-of-effective-commerce-agents
https://github.com/anthropics/commerce-agents/tree/main
以上内容不代表本平台立场,仅供读者参考