最近半年，混合专家（MoE）架构正在成为大模型垂直场景应用的默认选择：从美图基于MoE的奇想大模型V6覆盖影像创作全场景[2]，到跃盟科技用MoE架构搭建工位化企业智能体[3]，稀疏激活的设计平衡了大模型的性能与推理成本，让垂直场景的定制化模型门槛大幅降低。但2026年7月Mistral发布的开源形式化验证模型Leanstral 1.5，却暴露了MoE架构在特定垂直场景的核心矛盾：当需要严格逻辑一致性的形式化验证，遇上“分专家处理不同任务片段”的MoE路由机制，两者的适配性到底有多少？
形式化验证的痛点与Leanstral的基本盘
AI辅助编程的普及已经是行业共识，但信任问题始终没有得到根本解决。日本的一项行业调研显示，96%的开发者不信任AI生成的代码，却有48%的开发者不会做完整验证就直接部署[9]。对于智能合约、航空航天控制、医疗设备软件这类任务关键型场景，一个逻辑bug可能造成数千万美元的损失，甚至危及人身安全。形式化验证就是专门针对这类场景的解决方案：它不是通过有限的测试用例找bug，而是用数学定理证明代码在所有可能的输入下都符合预先定义的规范，相当于给代码上了一道数学层面的保险。
Lean 4是目前学术界和工业界应用最广的形式化验证工具之一，它既是函数式编程语言，也是交互式定理证明器，能自动校验开发者编写的证明脚本是否逻辑自洽。但Lean 4的学习门槛极高，熟练开发者写证明的速度通常只有每天几十行，据行业公开测算，传统形式化验证成本可达每千行数万美元，这让它过去只能应用在预算极高的核心场景。
Leanstral 1.5就是Mistral针对Lean 4场景优化的开源大模型，它采用稀疏MoE架构，总参数119B，单次推理仅激活6B参数，遵循Apache 2.0协议开源，用户既可以在Mistral Vibe平台输入/leanstall指令快速启动，也可以下载权重在本地部署，还能通过免费API端点labs-leanstral-2603调用[5][10]。目前已有独立开发者反馈Leanstral 1.5可稳定生成短证明脚本，最小功能闭环已可复现[5][6]。以太坊联合创始人Vitalik Buterin在2026年5月的公开分析中，也将Leanstral列为可本地部署的AI辅助形式化验证工具之一。
MoE的效率优势与形式化验证的逻辑刚性矛盾
MoE架构之所以成为垂直场景应用的主流，核心逻辑是“用总参数换泛化能力，用低激活参数降推理成本”：把传统Transformer的前馈网络拆成数十个独立的“专家”模块，每次推理时路由网络只选择和当前任务最相关的2-3个专家激活，这样总参数可以做到数百上千亿，保证模型的泛化能力，而实际激活的参数只有几B到十几B，推理成本只有同性能稠密模型的几分之一[1]。Leanstral的6B激活参数，推理算力需求只有Claude Sonnet的1/10左右，这也是它能做到调用成本远低于闭源大模型的核心原因[8]。
但这个设计刚好和形式化验证的核心需求产生了冲突。形式化验证的本质是长链逻辑推导，每一步的结论都必须严格承接上一步的所有前提，不能有任何隐含假设的偏移：比如证明一个智能合约的转账逻辑时，第一步假设“用户余额大于转账金额”，后续所有推导都必须严格遵循这个前提，哪怕只是把“大于”改成“大于等于”，整个证明就会失效，甚至可能掩盖致命的漏洞。
而MoE的路由机制，是根据当前输入token的语义动态分配专家，同一证明链的不同环节，很可能被分配给不同的专家处理。如果处理前提的专家A，和处理中间推导的专家B，以及输出结论的专家C，对同一个前提的语义理解存在细微偏差，就会出现“每一步单独看都逻辑自洽，整个证明链合起来却存在隐性逻辑断裂”的情况——这种错误很难被Lean 4编译器直接发现，因为编译器只会校验每一步的语法和局部逻辑，不会跨整个证明链检查前提的一致性。
需要明确的是，这个风险目前仅存在于长链证明场景：对于逻辑链路较短的简单证明，同一任务的所有token大概率会被路由到同一个或者少数几个专家处理，逻辑一致性的风险极低，这也是目前独立开发者反馈短证明使用体验较好的原因[6]。但对于千行以上的代码、超过20步的长证明链，目前没有任何公开的实测数据支撑其逻辑一致性：Mistral尚未披露长证明任务的专家激活重合率（即同一证明链中被同一专家处理的token占比），也没有公开超过100行的证明生成案例，长链场景下的架构适配性仍处于待验证状态。
性能与成本宣称的证据边界
Mistral在发布Leanstral 1.5时，给出了相当亮眼的性能与成本数据：在其自定义的FLTEval基准上，Leanstral pass@2得分26.3，超过Claude Sonnet 4.6的23.7分，运行成本仅36美元，仅为后者的1/15；pass@16得分31.9，领先Claude Sonnet 8分，成本仅290美元，而Claude Opus 4.6需要1650美元才能达到39.6分[5][8]。同时官方宣称该模型已经发现了5个开源仓库的未知bug[1]。
但这些宣称存在明确的证据边界。首先是FLTEval基准的复现性问题：目前该基准的测试集、评估规则、配套的lean-lsp-mcp工具链均未随模型权重开源，第三方若要复现测试结果，需要自行完成Lean 4数学库与模型的适配，仅算力成本就需要数千美元，截至目前暂无独立第三方公开复现了该基准的性能数据。同时，官方公布的成本仅为纯模型调用成本，未包含测试期的API补贴，也未覆盖形式化验证全链路中占比60%以上的人工成本——包括将业务逻辑转换为Lean 4规范、调试证明脚本、适配工具链的工时，即便纯调用成本真的下降93%，全链路的实际成本降幅也仅在13%左右，远未达到“改写成本结构”的程度[9]。
其次是“发现5个开源仓库未知bug”的宣称，目前没有任何公开的仓库地址、CVE编号、复现代码或修复记录可追溯，该宣称暂无有效证据支撑，无法作为模型应用能力的证明。
此外，目前也没有同规模通用大模型经过同等强度Lean 4专项微调后的对照测试数据，无法确认Leanstral的性能优势到底来自MoE架构的效率优化，还是来自垂直场景的高质量微调——如果优势主要来自后者，那么MoE架构的算力优化价值将被大幅稀释，模型的长期技术演进天花板也会相应降低。
真实的产业价值与垂直MoE的行业共性问题
尽管存在上述证据边界，Leanstral 1.5仍然具备明确的产业价值，它的核心壁垒并非官方宣称的性能SOTA，而是“开源+低激活参数”带来的低门槛自部署能力，刚好切中了闭源大模型无法覆盖的高敏感场景。
最典型的就是区块链智能合约审计场景：头部DeFi协议的单合约安全审计预算普遍在10万到50万美元之间，之前使用闭源大模型做辅助验证时，不仅需要承担单合约超过2000美元的调用成本，还存在未公开的合约代码泄露给第三方的合规风险——很多审计团队宁可承担更高的人工成本，也不愿意把未发布的合约代码传给闭源大模型。Leanstral可以本地部署，代码完全不出域，6B的激活参数单张A100就能跑，哪怕实际性能只有Claude Opus的50%，也足以支撑中小审计团队的需求。Vitalik Buterin已经将AI辅助的形式化验证列为以太坊下一阶段升级的核心安全工具，这一细分场景的付费意愿已经得到明确的产业信号支撑。
Leanstral 1.5也是当前垂直MoE热潮的一个典型样本：近半年来，从端侧推理的Liquid LFM2.5-8B-A1B，到代码辅助的JetBrains Mellum2，再到多模态的商汤SenseNova U1，越来越多的垂直场景模型选择了MoE架构，通过稀疏激活降低推理成本，针对特定场景做专项微调。但整个行业目前仍缺乏统一的垂直场景评估标准，绝大多数模型的性能数据都来自厂商自定义的基准，用户很难横向对比真实性能，“发布即营销”的现象仍然普遍。
后续需要追踪的核心事实
当前对Leanstral 1.5的判断，完全基于已公开的可验证数据，如果后续出现以下四类事实，当前的判断将会发生明确的改变：第一，有独立第三方在miniF2F、ProofNet等社区公认的形式化验证基准上，复现了Leanstral 80%以上的宣称性能；第二，Mistral公开了千行以上长证明任务的专家激活重合率与逻辑一致性测试数据，证明长链场景下的架构适配性；第三，有3家以上非Mistral关联的区块链审计团队将Leanstral纳入生产流程，且产生连续3个月的付费记录；第四，官方公开了所发现bug的可追溯细节，包括仓库地址、修复PR或CVE编号。
在这些事实得到确认之前，Leanstral 1.5仍然是一款优秀的短代码片段辅助验证工具，为高敏感场景的用户提供了闭源模型之外的新选择，但尚未达到可以支撑工业级高可信软件全流程形式化验证的程度。它的最大价值，或许是第一次把MoE架构在高逻辑刚性场景的适配问题摆到了台面上，为整个行业的垂直模型场景应用指出了一个此前被忽略的核心优化方向。
参考资料
当前关于Leanstral 1.5的核心分歧，本质是技术证据的边界能否支撑商业叙事的放大——产业侧提出的“形式化验证成本结构被改写”的判断，目前仅能得到模型调用环节的部分数据支撑，而数据侧提出的口径模糊、归因存疑问题，以及批判侧提出的证据链断裂、架构与任务需求错配问题，均有明确的信源结构和技术逻辑支撑，整体证据强度更高。 我之前对该模型落地有效性的判断存在过度宽松的问题，需要做出明确修正：此前将官方“发现5个开源仓库未知bug”的表述纳入落地有效性支撑，但目前所有公开信源均未披露相关仓库地址、bug复现方式或修复记录，该宣称属于无有效证据的叙事性表述，不能作为落地能力的支撑；目前唯一可被第三方独立验证的落地能力，仅为“输入数十行规模的代码片段、生成可通过Lean4编译器校验的短证明脚本”，该流程有英伟达开发者论坛的独立开发者测试反馈交叉验证，而千行以上长证明、真实工程场景的bug发现能力，均无任何可复现的证据。 针对批判侧提出的MoE架构风险，我此前的判断偏保守，需要进一步强化：该风险并非通用MoE模型的泛化隐患，而是形式化验证要求的长链逻辑严格一致性，与MoE路由机制“分专家处理不同任务片段”的原生设计冲突——形式化验证的每一步推导都必须严格承接上一步的前提，若同一证明链的不同环节被路由至不同专家处理，极有可能出现前提假设不一致导致的逻辑断裂，但目前官方未披露任何针对长证明场景的路由层优化细节，也未公开同一长证明任务多次调用的专家激活重合率、前提一致性测试数据，甚至没有公开超过100行的证明生成案例，这一核心架构与任务需求的适配性未被任何公开数据验证，直接决定了该模型能否进入工业级场景，而非仅能作为演示工具。 针对数据侧提出的口径和归因问题，我此前对成本优势的判断存在未明确限定的缺陷：此前认为其成本下降逻辑符合MoE架构的性能-成本守恒规律，这一判断仅适用于官方披露的、未排除测试期补贴的纯模型调用成本口径，未覆盖形式化验证全链路中占比60%以上的人工规范定义、调试成本；同时，目前没有同规模通用模型做同等强度Lean4专项微调的对照测试，无法确认其性能优势来自MoE架构还是垂直场景的高质量微调，此前关于架构优势的归因判断需要收回，仅能确认6B激活参数的设计确实比动辄几十B激活参数的通用大模型推理算力需求更低。 针对产业侧提出的成本结构改写判断，我认可其对潜在付费群体的分析符合高可信软件场景的真实需求，但该判断目前超出了技术可验证的边界：形式化验证的全链路成本中，模型调用仅占15%-20%，即便该环节成本确实下降93%，全链路降本幅度也仅为13.5%左右，产业侧提出的“砍掉40%-60%人工审查”的假设，建立在“生成的证明可自动完成全链路校验”的前提上，但该前提目前仅在短脚本场景得到验证，长证明场景的全链路自动校验通过率无任何公开数据，因此“成本结构被改写”的结论目前没有技术侧的全链路数据支撑。 修正后的核心判断可归纳为三点：其一，Leanstral 1.5是首个针对Lean4场景的开源MoE模型，短证明生成的最小技术闭环可被第三方复现，权重可公开下载、本地加载的事实有明确交叉验证，置信度90%；其二，所有关于性能SOTA、成本降低93%、发现未知工程bug的宣称，均仅来自厂商自有的未公开基准、模糊口径和无细节叙事，无独立第三方验证，置信度低于30%；其三，其MoE架构与形式化验证核心需求的适配性未被任何公开数据验证，长证明场景下的逻辑断裂风险尚未排除，当前仅适用于短代码片段的辅助验证场景，无法支撑工业级高可信软件的全流程形式化验证，置信度85%。后续需要追踪的核心指标包括：第三方在miniF2F、ProofNet等通用基准上的复现成绩，千行以上长证明任务的专家激活重合率与逻辑一致性数据，全链路形式化验证的成本统计，所宣称bug的可追溯细节，以及同规模通用模型做同等微调后的性能对照结果。
建议将核心主线改为「Leanstral改写形式化验证成本结构」，突出商业价值以提升传播性
为什么没放进正文：该判断基于未验证的「证明可全链路自动完成」前提，未覆盖形式化验证全链路中占比60%以上的人工成本，实际全链路降本幅度仅约13%，远未达到结构改写的程度，不符合机制解释稿的证据严谨要求
建议得出「MoE架构完全不适合形式化验证场景」的强结论，强化观点冲突性
为什么没放进正文：该判断存在泛化逻辑谬误，10步以内的短链证明场景下MoE的逻辑一致性风险已被实测排除，风险仅存在于20步以上的长链证明场景，极端结论会误导读者对模型适用边界的判断
Reader Signal
这篇文章对你有帮助吗？
只收集预设选项，不开放评论，不公开展示个人反馈。
选择一个判断，也可以附加一个预设标签。
发布于 2026-07-04 07:46:04。本文为原创深度报告，未经授权不得转载。观点仅代表编辑部独立判断，不构成投资建议。