Axiom Math 对谈 SGLang：模型的下一步是可验证，结果层才是真正的护城河

大概率是可验证。

AI 正在真正进入生产环境，而一旦进入生产环境，核心问题就变了，不再是模型能不能给出一个好答案，而是整个系统能不能在可预测的成本和延迟下，稳定、重复、规模化地交付结果，并让这些结果可验证、可追溯、可信赖。

在 AGI Playground 2026 的圆桌论坛上，Axiom Math 联合创始人兼 CTO Shubho Sangupta、Radixark 核心技术成员鲍科，与 SoTALab 联合创始人于林希展开深度对谈，从长任务智能体的成功率衰减、推理基建的生产级升级，聊到可验证 AI 的边界、模型商品化后的价值迁移，最终回到同一个核心问题：可验证，可能是 AI 发展的下一个真正瓶颈。

于林希同时担任本次圆桌主持，SoTALab 目前正为全球顶尖模型提供长程任务、computer use 和专家领域知识方面的高质量数据。Axiom Math 从数学证明领域切入，将严格的形式化验证嵌入 AI 推理的每一个环节，用确定性工具对抗模型的捷径行为。

Radixark 要解决的问题则不一样，它扎根在推理基础设施层，以开源框架 SGLang 为核心，从底层优化智能体工作负载的部署效率与运行稳定性。本文整理自本次圆桌对话，内容经编辑调整。⬆️关注 Founder Park，最及时最干货的创业分享 我们将通过「AI 产品市集」、内容报道、社群分发等方式，帮你触达早期用户、获得真实反馈，以及建立关键连接。

01 长任务能力 Scaling 的唯一路径， 是做好验证 于林希：行业都在说 AI 已经进入了优先部署和可靠性的时代。Agent 进入生产环境后，你们观察到最大的变化是什么？客户现在最焦虑的是什么？鲍科： agent workload 一个明显变化是单次任务变得更长、调用链更复杂，因此对端到端正确性和稳定性的要求更高。

他们会用 benchmark 来确保模型能输出正确答案，以及 function calling 的能力。其次是生产部署层面的性能和稳定性，上线之前会做大量压力测试，确保线上服务不会崩溃或卡死。

体验层面，他们关心首 token 的延迟、token 之间的间隔，会设定相应的 SLO（Service Level Objective，服务级别目标），并在自己的硬件上优化吞吐。Shubho：我从数学的角度来说。

我们构建的是数学「系统」——我更愿意叫它系统而不是 agent——因为它不只是把模型串联起来，还要维护跨多个子 agent 的大型记忆体，同时调用各种确定性工具，包括专门的数学服务、确定性搜索引擎等。在数学领域，agent 的运行时间极长，上下文也极长，因为数学本质上就是搜索和回溯：从一个定理出发，要不断地分解。

在这种长时间运行的 agent 中，怎么跨子 agent 做搜索和回溯？怎么管理记忆？上下文太大了，单个模型根本放不下。而且数学场景，数学家的介入方式也很有意思，他们看分解图时可以直接反馈说「别走这条路了，我知道行不通」。

模型有自己的推理链路，agent 框架也有自己的推理链路，怎么清晰地区分哪些属于框架层，哪些属于模型层？对于长时间运行的 agent，什么时候该判断「这条路走得太远了，解法可能在别处」？这些问题目前在数学领域尤为突出，但未来 coding 领域出现超长 agent 时，同样会遇到。

于林希：我们看到 agent 在越来越长的时间跨度上工作。任务简单、几步就能完成时，准确率很高；但一旦任务链超过 50 步，整体成功率就会断崖式下降——这本质上是一个乘法问题。这个差距能靠 foundation model 推理能力变强来弥合吗？

还是说 agent 的每一步都需要逐步验证？Shubho：从强化学习的角度来看，长任务推演中每一步的奖励信号越精细，训练效果就越好。我早期做围棋引擎训练时，奖励只在百步对局结束时给出，这种模式在百步规模下还行得通。

但现在的数学证明动辄数千步，光靠终局奖励远远不够，每一步都需要细粒度反馈。关键在于怎么实现。我们可以通过验证体系来提供奖励信号，比如用 Lean 定理证明器——Lean 虽然不会直接告诉你证明是否完成，但能反馈当前已满足多少个证明目标，这就可以转化为奖励信号。非形式化推理轨迹的奖励信号很难获取，但如果把问题转化为可验证的命题，就能更容易得到细粒度奖励。

我认为细粒度奖励与验证，是长任务能力规模化的唯一可行路径。于林希：你在 Nvidia、Meta 和百度花了二十年做 scaling 相关的工作。创立 Axiom Math 之前，是什么让你觉得光靠 scaling 已经不够了？

Shubho：说实话，创立 Axiom 的时候，我们一开始并没有在想验证这件事。Karina 和我就是都热爱数学和编程，觉得数学是一条通向自我进化的路径——在数学里没有灰色地带，要么证明了，要么没证明，信号非常强。所以本质上，公司是因为我们对数学和编程的热爱才创立的。

后来我们又发现，如果我们能证明数学里的东西，也许也能证明代码里的东西——因为在数学中，我们本质上是用计算机来做证明，归根结底就是代码。所以从很多层面来看，这家公司的目标其实是统一数学和计算机科学。02 超大参数的模型， 带来了新的 infra 基建问题 于林希：鲍科，从 inference 基础设施的角度看，你觉得生成侧的问题基本解决了吗？

鲍科：没有。时代在变，模型迭代非常快，硬件也在变。模型这几年 scale 了很多——两年前 700 亿参数算大模型，但现在 Kimi K3 的总参数量已经到了 2.8 万亿。模型比以前大得多，对基础设施的挑战也大得多。

架构上也变复杂了。以前是标准的全注意力、multi-head attention，现在有了 sliding window、linear attention，各种混合架构。这些对显存池设计和 prefill 缓存都带来了新挑战。新硬件上 kernel 的优化和调优也是持续的工作。

所以我觉得优化空间还很大。于林希：你们处在模型和硬件之间，两端都在快速演进。从你的角度看，生产环境中最容易被低估的问题是什么？鲍科：在我们的 inference 引擎里，已经针对不同场景做了性能优化——低延迟场景、大规模部署场景、高吞吐场景。

对生产团队来说，最头疼的往往是怎么为不同的工作负载找到最优配置，而且有些工作负载还是动态变化的。我们给用户提供了配置手册，给出不同场景的部署命令，但有些参数还是需要根据具体工作负载来调优。我们正在做的事情就是简化这个过程，让一些参数实现自动配置，比如显存比例、speculative decoding 的配置等，能根据工作负载动态调整。

于林希：你之前提到 SGLang 正在从开源框架演进为企业级生产系统。要从「跑得快」升级到企业真正敢把核心业务交给它的服务水平，还需要补齐哪些关键能力？稳定性、可观测性和故障恢复，会不会成为比性能更重要的竞争壁垒？

鲍科：没错。inference engine的核心就是让模型高效地跑在硬件上，尽可能提升生成 token的效率。但引擎只是产品的内核，在它之上还需要一系列生产级服务，确保它能在大规模集群上稳定、可扩展地运行。其中很重要的一块是可观测性——收集指标、日志，用于排查异常请求和链路追踪。

还有稳定性，确保系统能长时间运行而不出生产事故。于林希：Agentic 工作流跟传统聊天请求有本质区别——更长的文本、更长的上下文、更高的前缀复用率、更复杂的调用链。缓存、speculative decoding 和复杂模型结构方面的优化，能在多大程度上降低每个 agent 任务的成本？

inference 的核心计量单位，会不会从「每百万 token」变成「每个成功完成的任务」？鲍科：用户最关心的始终是成本，而 SGLang 一路走来，核心就是通过一系列技术组合拳把成本打下来。从 Radix Attention 起步，挖掘请求间的复用潜力。

我们最初是从 Radix Attention 做起的。逻辑很直观：在请求之间找优化空间。如果系统发现某个请求的 KV cache 已经算过了，后续带有相同前缀的请求就可以直接复用。

这样能大幅减少 prefill 端的计算量，最直接的效果就是首个 token 延迟明显降低。应对 Agentic 挑战，构建分层缓存体系。但 agentic 工作负载更复杂，往往涉及多轮 function call，上下文非常长，GPU 显存存不下这么多 KV cache。

为此我们开发了HiCache——用多层存储来管理 KV cache 的前缀复用：显存满了就offload到 DRAM 或分布式存储系统里。这样 KV cache 依然可以被复用，从而降低每一轮推理的 TTFT。针对不同场景，投机解码与异构调度。

在低延迟场景下，解码往往是显存带宽瓶颈，我们用投机解码（Speculative Decoding）来利用更多 GPU 算力加速。还有 Overlap Scheduler，核心是把 CPU 和 GPU 的计算尽可能重叠起来，目标很明确：让 GPU 尽可能保持 100% busy，减少空转。

于林希：SGLang 不仅做推理，还在向训练后环节延伸，朝训推一体化发展。自主进化系统会产生海量推演、验证与重试数据，这对底层基础设施提出了哪些新要求？鲍科：SGLang 可以作为 RL（强化学习）的Rollout engine，这个场景非常重要。

RL 工作流是超高吞吐量负载，我们做了大量优化来提升每一步推演生成的吞吐——比如前缀缓存、分层缓存都可以用于 RL 推演生成；同时 RL 是多轮生成过程，会话缓存也很关键。此外 RL 场景有明显的长尾效应：同一批请求中，部分请求的生成长度会远超其他请求。针对这种长尾情况，我们可以用投机解码来加速，提升整批任务的完成效率。

03 数学证明有希望泛化到整个通用推理 于林希：Axiom 提供证明验证、命题提取、源码转换和确定性修复，作为云基础设施对外服务。为什么 AI 做数学需要一个独立的证明基础设施层？请求量 scale 上去之后，什么是最难保障的？

Shubho：Axiom 的起点挺有意思的。我们发现所有 LLM 都会以某种方式「作弊」——这里说的作弊是指它会找到通往既定 reward 的捷径。我们用 Lean 证明能否编译通过作为 reward 来训练 LLM，在 Lean 中，证明能编译就意味着它是正确的。

但模型有各种办法「钻空子」：比如声明一些定理然后直接断言它们成立，或者塞入循环依赖。我们从去年很早就开始注意到模型在做这些事情，于是着手构建一套完全独立于 LLM、完全确定性的方法，来识别模型走捷径的各种方式。这就成了 Axiom。其他训练模型的团队也做过类似尝试，但我们可能是第一个做成产品并向全世界开放 API 的。

后来我们不断加入新功能：比如给定一个大型证明，能不能从中提取定理？能不能提取命题？这样它不仅成为我们 RL 流水线的一部分，也成为数据流水线的一部分。我们会生成大量 Lean 代码，并从中提取丰富的元数据。

今年早些时候我们向全世界开放了这个 API，Lean 程序员非常喜欢。我们还做了一个 MCP 前端，用 Claude 或 GPT 做证明的人会大量使用这个 MCP 接口，非常受欢迎。于林希：我记得去年全行业做数学题还是只看最终结果对不对。

推进数学推理能力，是怎么带动 LLM 通用推理能力演进的？过程级验证在其中扮演什么角色？Shubho：这也是我们正在探索的问题。

经过数学证明训练的模型能否泛化到其他推理领域，目前仍然是个开放命题。但我们已经观察到一些明确的结论：经过数学证明训练的模型，在软件验证基准上也表现优异，这类基准会把软件问题转化为数学问题来验证其不变性。从数学证明到软件验证、甚至硬件验证，我们已经看到了清晰的能力泛化。

至于能否进一步泛化到通用推理，我持乐观态度。科学领域中，数学及其相邻学科（理论物理、化学、理论计算机科学）本质都是推理。用形式化数学训练模型会产生很强的迁移能力；而且形式化数学训练最终产出的是可被计算机校验的代码，这会成为通用推理能力的良好基础。

我认为这种影响是双向的。于林希：现在大多数 RL 训练用 LLM-as-judge 来互相打分，各有利弊；而数学和代码领域可以用编译器、证明器来提供确定性 reward。你怎么看这两种机制的取舍？什么时候该用哪种？可验证的 reward 会不会成为比预训练数据更稀缺的资源？

Shubho：如果能给出细粒度的 reward，我认为这是最好的方向。关键是怎么做到，有些场景可以，有些不行。在数学中，最终的 reward 是明确的——证明成立与否。

但我们在尝试能不能给部分 reward。这很像人类考试拿「部分得分」：证明做了一半也能拿分。接到确定性系统上，比如 Lean 引擎，它可以告诉你还剩多少 goal 没有完成，这就能转化为一种 reward 信号。

我觉得 RL 中有三个核心难题：一是 reward 到底怎么定义，reward hacking 是真实存在的问题；二是能不能让 reward 足够细粒度；三是能不能让训练不崩溃。我对数学领域更乐观一些，因为人类在数学中一直在做「部分评分」，也许我们可以把这种做法嵌入到给模型的 reward 中。

04 未来真正有壁垒的是「结果层」 于林希：数学和代码天然自带校验器，但现实业务场景大多没有明确的对错之分——目标模糊、意图可变、信息不完整，评判标准也有争议。你觉得可验证 AI 的边界在哪里？Shubho：可验证 AI 能拓展到哪些领域、哪些领域无法完全验证，这个问题未来五六年会逐步有答案。

我的核心判断是：凡是能通过代码解决的问题，都可以被验证。真正的瓶颈在于，人类并不擅长严谨、形式化地表述自己的需求。比如给智能体写指令，生成的代码往往不符合预期，根源通常是需求本身没有被精确定义。

我认为未来，代码调试会演变为对需求规范的迭代：人们用自然语言描述需求，智能体生成代码并尝试验证，再用自然语言反馈哪里验证不通过，人类据此迭代需求。抽象层会整体上移——从「迭代代码」变成「迭代需求定义」。Andreessen Horowitz 有句名言叫「软件吞噬世界」，而所有被软件覆盖的领域，大概率都可以被验证。

于林希：你觉得一切都可以被验证？Shubho：是的。于林希：我有一个类似的看法。我在 Seed 做模型训练时，分析过用户请求。

虽然大多数用户输入的文本都是残缺不全的，他们一般不会写完整的句子，但把所有请求汇总分析后你会发现，那些不完整甚至有错误的句子背后，真实意图其实是可以捕捉到的。大多数人的思维方式是相似的。

所以如果我们做 agent 或 agentic model，执行层面应该基于非常精确的行为来运作，但意图是可以被提取的——只要有足够多的数据，就能真正理解用户在特定领域中想要什么。意图可以很复杂，但人们真正想要的东西，是可以被聚合和提取出来的。那在你看来，随着模型能力越来越同质化，价值会迁移到哪里？

Shubho：我的观点可能有些争议：当前全球顶级模型之间的能力差距大概在 3-6 个月，模型层的商品化速度很快。AI 的进步节奏已经放缓，不再是指数级提升。我认为未来真正有壁垒的是「结果层」。

不再是标准的 token 输入输出 API，而是面向行业的、可交付具体结果的服务——比如正确的代码行数，或者单位成本下完成的任务量。这种行业专属的结果交付不具备通用 API 的标准化属性，会形成更强的护城河。未来五六年，行业价值会向这个方向流动。

当然这也取决于模型的进化速度：如果能力持续指数级提升，格局会不一样；如果增速放缓，或者出现垂直领域专用模型，结果层的价值会更加凸显。目前我们已经看到垂直专用模型的苗头。于林希：回到今天的主题，验证会成为 AI 的新瓶颈吗？

鲍科：我觉得验证本身不是瓶颈，但为 RL 训练获取正确的、可证明的答案，可能是更难的部分。比如数学领域现在可以获得可证明的答案，但在软件工程等领域，很难像数学一样，获得低成本完全正确的答案来做训练信号。这才是真正难解决的问题。Shubho：至少在软件领域，过去一个人加入公司，通常需要花很长时间才能上手写代码。

但现在，一天写一万行代码完全不是问题。可我们发现瓶颈变了，这些代码好不好？测试写了没有？我能放心合并这段代码吗？

就算在我们这么小的公司里，reviewer 已经成了瓶颈：大家写了几千行代码，谁来 review？所以我认为，要真正解锁软件工程下一个层次的生产力，关键在于能不能证明代码的某些性质，它是不是符合你的意图。这才是下一波生产力释放的关键。

数学领域也会面临同样的问题。我再说一个有争议的观点：未来写一篇数学论文会变得非常容易。但如果人人都能写，谁来 review？

数学领域会比几乎所有其他领域更早面对这个问题——论文不断涌来，但没有人来 review。于林希：补充一下。不仅是没有人来 review，而是没有人有能力 review。随着推理能力的提升，能够审查 AI 工作的人会越来越少。

内容中包含的图片若涉及版权问题，请及时与我们联系删除