博士论文 | Optimization and Control Techniques for Reliable Intelligent Systems：可靠智能系统的优化与控制技术

导读

大模型和机器学习系统正在被部署到越来越复杂的真实任务中，但“能生成答案”并不等于“可验证、可控制、可评估”。这篇斯坦福博士论文《Optimization and Control Techniques for Reliable Intelligent Systems》围绕可靠智能系统展开，核心问题是：如何把优化、控制、统计保证和形式化验证方法嵌入机器学习系统，尤其是大语言模型系统，让它们在长任务、无标签数据和安全约束下更可靠。

论文作者 Emiko Soroka 将整篇论文组织成四条研究线。第一条线面向机器人和控制场景，研究如何从轨迹数据中学习时间逻辑谓词，并用 conformal quantile regression 给出统计覆盖保证。第二条线面向无标签的人类-大模型交互数据，提出 LLM 引导聚类方法，让系统自动发现未知数量的用户目标类别。第三条线面向企业级大模型评估，使用小型微调语言模型适应分布漂移，并评估交互是否完成、模型在哪里不确定。第四条线面向大模型系统的形式化验证，研究大模型能否生成形式化规格，以及“代码形式规划”如何让长程任务计划被解释器执行、被验证器检查、被反馈机制纠偏。

这篇论文的价值不在于提出一个单一大模型算法，而在于给出一套“可靠性工程”的研究路径：用统计校准约束学习出的逻辑，用聚类和小模型评估无标签交互，用可执行代码承载大模型计划，再用形式化检查阻止任务偏离。它把传统控制与优化的严谨性，带入了当下更开放、更难验证的智能系统。

论文信息

论文题目：Optimization and Control Techniques for Reliable Intelligent Systems 作者：Emiko Soroka 学位：Doctor of Philosophy 单位：Stanford University，Department of Electrical Engineering 答辩/提交时间：2026 年 6 月 导师：Sanjay Lall 论文链接：https://stacks.stanford.edu/file/qx918mc2735/thesis-augmented.pdf

总体问题：智能系统为什么需要可验证性

论文开篇指出，机器学习系统和大语言模型系统都很难验证。传统优化算法、拟合算法和大模型生成系统都可能在分布外输入、长程任务、目标不明确或约束复杂时产生不可预测行为。可靠智能系统需要的不只是更高平均性能，还需要知道系统在什么条件下可信、何时不确定、哪些行为满足约束、失败后如何纠正。 论文的主线可以概括为三个层次。第一层是从数据中学习可解释的逻辑对象，并赋予统计保证。第二层是在没有人工标签的场景中评价大模型交互，从数据分布中发现结构和异常。第三层是将大模型输出转化为可执行、可检查的形式，从而把自然语言计划变成能够被程序分析和形式化验证约束的对象。 这三个层次共同指向一个判断：可靠性不能只靠模型自评，也不能只靠更大的模型规模。可靠性需要外部工具、统计校准、优化算法和可验证表示共同参与。

从数据学习时间逻辑谓词

第二章研究如何从轨迹数据中学习信号时间逻辑谓词。时间逻辑常用于机器人、自动驾驶和控制系统中，用来描述“最终到达目标”“始终避开障碍”“直到某条件满足前保持安全”等性质。传统上，这类谓词往往由专家手写，但真实场景中的规则复杂、轨迹带噪、观测不完整，手工构造既困难也缺少统计保证。 作者提出的思路是：先用轨迹预测器根据部分观测预测未来轨迹，再计算候选时间逻辑原子的鲁棒度分布；随后用 conformal quantile regression 为每个原子的鲁棒度构造置信区间；最后在这些区间上优化逻辑表达式，得到一个既可解释又带统计覆盖保证的谓词。

图1 从轨迹数据学习时间逻辑谓词的算法流程：先生成预测轨迹和鲁棒度分位数，再在置信区间上优化逻辑表达式。 这个方法的关键点在于，它不是直接学习一个黑盒分类器，而是学习一个可以被形式化验证工具使用的逻辑表达式。conformal 方法提供分布无关的统计校准，保证学习出的谓词区间在未见轨迹上具有覆盖意义。论文在二维轨迹数据和弱势道路使用者数据上测试了表达式优化方法，并比较了遗传编程、语法演化等随机优化算法。 这一章最后还介绍了 Satisfiability.jl，一个 Julia 生态中的 SMT 工具接口。它用于构造 SMT 公式、生成 SMT-LIB 语句并与求解器交互。这个工具延续了论文的核心思路：让控制、优化和验证工具更容易进入机器学习工作流。

面向文本交互的引导式聚类

第三章转向大模型评估。企业和应用开发者常常拥有大量人类-大模型交互日志，却缺少人工标签，也不知道用户目标到底有多少类。直接用大模型充当评审器可以得到标签，但稳定性较差，且不同运行之间容易产生不一致类别。作者因此提出一种 LLM 引导聚类方法，把嵌入空间中的 k-means 聚类与大模型的文本摘要能力结合起来。 方法流程是：先用文本嵌入和较大的初始聚类数将交互数据分组，再用大模型为每个聚类生成可解释标签或摘要，随后根据标签相似性和嵌入结构逐步合并聚类。这样既保留了 k-means 在向量空间中的稳定性，也利用了大模型理解长文本和生成类别名称的能力。

图2 多次聚类运行的标签稳定性矩阵：上方的引导式聚类更接近对角结构，而纯大模型标注基线更不稳定。 实验覆盖真实聊天数据、代码反馈数据、保险领域数据、WebShop 代理交互数据以及同时涉及知识库、操作系统和 SQL 工具的数据。结果显示，LLM 引导聚类在多数数据集上比纯 LLM-as-a-judge 基线更稳定，尤其能避免大模型在不同运行中生成大量不一致标签。 这章的重要启发是：大模型评估不一定要让大模型直接给最终裁决。更稳妥的方式是让传统优化算法处理结构化部分，让大模型处理语义解释部分。聚类算法给出稳定分组，大模型给出人类可读标签，两者结合能降低无监督评估中的漂移与随意性。

用小语言模型评估大模型交互

第四章继续研究无标签大模型评估，但重点转向小型微调语言模型。现实企业场景中，交互数据往往无标签，而且分布会随着客户、业务流程、工具环境和代理能力变化。使用大型模型作为评审器成本高，也未必适应特定企业数据。论文提出将小型语言模型视为数据分布的近似器，通过微调适应分布漂移，再构造评估指标。 作者提出两个具体任务。第一个是交互完成度标注：给定一段人类与大模型的多轮交互，判断任务是否已经完成。如果模型认为对话仍然缺少后续步骤，它会生成可能的补全内容；如果交互已经完成，它应预测结束标记。这个方法把“是否完成”转化为序列建模问题。

图3 用小语言模型判断交互是否完成：未完成对话会诱导模型生成后续补全，完成对话则应直接结束。 实验发现，在多个任务型数据集上，8B 级微调模型可以达到或超过 70B 大模型评审器的表现，并能适应非结构化聊天数据。论文也诚实指出，在代码反馈和保险等边界模糊的数据中，完成度本身可能没有清晰定义，评估方法会遇到限制。 第二个任务是大模型不确定性量化。许多接口只暴露 token 级 logprob，但 token 级不确定性并不等价于整段回答的不确定性。论文提出近似响应树：在生成过程中基于高概率替代 token 分支，构造可能回答的树状分布，再结合语义熵衡量序列级不确定性。这比简单采样更高效，也能更细粒度定位模型在回答路径中的分叉点。

形式化验证与代码形式规划

第五章是整篇论文最贴近当前大模型智能体讨论的部分。作者首先研究大模型能否生成时间逻辑规格，再研究能否用形式化验证约束大模型计划。自然语言计划模糊且难以检查，而代码有清晰语义，可以被解释器执行，也可以被静态分析或验证工具检查。因此论文提出代码形式规划：规划模型将复杂任务分解为子任务，并生成可执行 Python 计划；执行模型负责完成子任务；验证器检查计划是否满足安全性、活性和任务约束。 论文先在路径规划中测试大模型生成 STL 规格的能力。简单网格任务中，大模型表现较好；在 25x25 的复杂网格、迷宫和墙体布局中，生成正确规格更困难。一个重要发现是：让模型用 Python 代码形式表达规格，通常能降低语法错误并提高语义正确率。

图4 路径规划基准中的简单网格和更复杂的 25x25 网格环境，用于测试大模型生成时间逻辑规格和计划的能力。

图5 大模型生成时间逻辑规格的结果：代码形式规格在复杂网格上更有助于降低错误、提升语义正确率。 随后，论文将代码形式规划用于路径规划、多跳推理和 WebMall 网页购物任务。路径规划中，代码形式规划通常比普通基线更好，并在若干设置中优于或接近 ReAct、思维链等策略。不过作者指出，部分收益来自代码注释带来的逐步推理效果，而不完全来自形式化验证本身。

图6 代码形式规划在路径规划任务中的表现：在多个网格设置下，代码形式规划提高通过率和最优路径比例。 在多跳推理中，许多约束难以形式化验证，但代码形式规划仍能帮助模型把复杂问题分解为更明确的步骤。实验显示 GPT-4o、GPT-4.1、Claude Sonnet 4 和 Gemini 2.0 Flash Lite 等模型在代码形式提示下都有提升，但瓶颈仍在于模型能否正确拆解复杂任务。 在 WebMall 代理任务中，代码形式规划能显著减少“偏离任务”的错误，例如保证代理访问所有需要比较的商店、填写最终结果字段、按计划推进任务。但它也引入新的问题：谁负责维护外部环境状态，规划模型还是执行模型？执行模型应获得多少上下文？当计划正确但执行错误时，反馈应该传给谁？论文发现，代码形式规划提高了高级任务的检查点完成率，却不一定提升最终商品选择准确率。这说明形式化计划能约束任务流程，但不能自动解决感知、检索和执行质量问题。

实验结论与方法启示

整篇论文给出的第一个启示是，可靠性可以通过“可验证中间表示”获得增量改善。时间逻辑谓词、聚类标签、交互完成度、响应树、代码计划和形式化规格，都是介于黑盒模型输出和最终任务成功之间的中间对象。它们让系统不再只输出答案，而是暴露可以检查、优化和校准的结构。 第二个启示是，小模型和传统优化算法仍然很有价值。第 3 章和第 4 章都没有简单地让最大模型做裁判，而是利用 k-means、嵌入模型、小型微调语言模型和统计指标构建评估工具。这对企业级部署尤其重要，因为真实数据往往无标签、私有、分布漂移明显，评估系统必须便宜、可适配、可重复。 第三个启示是，形式化验证并不是万能安全按钮。它适合约束明确、状态可表示、检查器可写的任务；在开放式多跳推理和网页代理中，验证覆盖范围会受到状态管理、上下文传递和执行器能力限制。论文的贡献恰恰在于没有夸大形式化方法，而是指出它在哪些任务上有效、在哪些任务上只是部分改善。

局限与未来方向

论文讨论了多项局限。时间逻辑学习方法依赖轨迹预测器和候选语法，若候选原子不足或观测分布变化太大，学习出的谓词可能无法覆盖真实系统。LLM 引导聚类依赖嵌入模型与大模型摘要质量，且对语义边界模糊的数据集仍会产生不稳定标签。小模型评估方法需要足够接近目标分布的无标签数据，完成度定义不清时很难给出可靠指标。 形式化验证部分的局限更值得关注。代码形式规划让计划更可执行、更易验证，但在代理环境中会制造新的工程边界：计划器、执行器、环境状态和验证器之间如何分工？验证失败反馈应该是自然语言、代码错误、约束违例还是状态差异？如果任务本身没有可形式化目标，代码形式规划只能提供结构化推理，而不能提供完整正确性保证。 未来方向包括：将 conformal prediction 与更复杂的控制和机器人任务结合；为大模型交互构建更稳定的无监督评估基准；用小模型持续监测企业场景中的分布漂移；发展能处理外部状态、工具调用和长程记忆的可验证代理框架；以及将代码形式规划与程序分析、模型检查、测试生成和自动修复结合起来。

总结

这篇博士论文以“可靠智能系统”为总目标，把优化、控制、统计校准和形式化验证连接到机器学习与大模型系统中。第 2 章让从轨迹数据学习出的时间逻辑谓词具备统计保证；第 3 章用 LLM 引导聚类稳定发现无标签交互中的用户目标；第 4 章用小型微调语言模型评估交互完成度和序列级不确定性；第 5 章用代码形式规划探索大模型计划的可执行与可验证表达。 如果说很多大模型研究关注“模型能不能做”，这篇论文更关心“系统如何知道自己做得对不对”。它提醒我们，可靠性不是模型能力的自然副产品，而需要外部约束、统计保证、可解释中间表示和可验证执行路径共同构建。对于正在走向工具使用、长期任务和企业部署的大模型系统，这是一条非常值得重视的技术路线。