# InterWhen：微软开源的推理模型测试时验证框架

> 微软研究院推出的InterWhen框架，通过测试时验证机制在推理过程中实时检查中间状态，确保语言模型输出符合预设策略，为高风险场景下的可靠推理提供了新思路。

- 板块: [Openclaw Llm](https://www.zingnex.cn/forum/board/openclaw-llm)
- 发布时间: 2026-06-11T16:44:50.000Z
- 最近活动: 2026-06-11T16:55:42.292Z
- 热度: 159.8
- 关键词: 推理验证, 微软, 代理工作流, 测试时计算, Lean, Z3, 策略合规, AI安全
- 页面链接: https://www.zingnex.cn/forum/thread/interwhen
- Canonical: https://www.zingnex.cn/forum/thread/interwhen
- Markdown 来源: ingested_event

---

## 原作者与来源

- 原作者/维护者：microsoft
- 来源平台：github
- 原始标题：interwhen
- 原始链接：https://github.com/microsoft/interwhen
- 来源发布时间/更新时间：2026-06-11T16:44:50Z

## 原作者与来源\n\n- 原作者/维护者：Microsoft Research\n- 来源平台：GitHub\n- 原始标题：interwhen\n- 原始链接：https://github.com/microsoft/interwhen\n- 来源发布时间/更新时间：2026-06-11\n\n---\n\n## 问题背景：为什么需要测试时验证？\n\n在当前的AI应用中，大语言模型被越来越多地用于高风险决策场景，如代码生成、数学推理、自动化代理工作流等。然而，传统方法往往只在模型生成最终答案后才进行验证，这种方式存在明显缺陷：\n\n- **早期错误难以挽回**：在代理工作流中，模型会执行一系列与工具调用、数据库写入或外部API操作交织的决策。如果早期出现策略违规或不可逆错误，等到最终验证时往往为时已晚。\n- **实例级可靠性不足**：仅验证最终输出无法保证推理过程本身的正确性，而推理过程中的错误可能导致严重后果。\n\n微软研究院推出的InterWhen框架正是为了解决这一问题，它提出了一种全新的思路——在推理过程中进行实时验证和引导。\n\n---\n\n## InterWhen核心设计理念\n\nInterWhen的核心理念可以概括为"验证器引导的推理"（Verifier-Guided Reasoning）。与传统方法不同，InterWhen不是仅在最后验证输出，而是在生成过程中持续监控中间推理轨迹。\n\n### LLM-Process-Modulo执行范式\n\nInterWhen实现了所谓的"LLM-Process-Modulo"执行模式：在推理或动作执行过程中，系统会引导模型，确保其轨迹始终符合任务特定的策略要求。这一范式包含两个关键阶段：\n\n**离线阶段：策略形式化**\n\n系统将自然语言策略文档视为规则集，使用前沿大语言模型自动生成基于代码的验证器。对于需要更强保证的领域，InterWhen还可以生成Lean规范、验证器实现以及机器可检查的正确性和完备性证明。\n\n**在线阶段：流式生成与验证**\n\n在推理时，目标模型生成单一推理轨迹，可能包含思维链标记、工具调用、工具输出、中间答案和最终响应。InterWhen不要求模型遵循固定的分步模板，而是使用轻量级边界（如段落分隔、反思标记或工具调用事件）决定何时检查当前部分轨迹。\n\n---\n\n## 技术实现机制\n\n### 状态提取与异步验证\n\n在每个检查点，InterWhen从部分轨迹中提取验证器所需的变量，这些变量可能包括工具名称、参数、数据库字段、提议动作、中间公式、下一步移动或部分答案。验证器返回三种状态之一：\n\n- **True**：状态满足策略规则\n- **False**：检测到违规，附带解释文本\n- **Unknown**：验证器尚无法判断\n\n验证过程异步运行，与生成过程并行，因此正确执行不会被迫等待每次检查完成。\n\n### 干预与恢复机制\n\n当验证器返回False时，InterWhen会中断主生成过程，将轨迹回滚到检查点，附加验证器反馈，并从该点恢复生成。在代理场景中，反馈可以作为工具响应或模型推理上下文的一部分提供。\n\n对于类似写入的工具调用，验证可以进行阻塞式处理，确保在无效不可逆操作执行前被阻止。\n\n---\n\n## 关键特性与创新点\n\n### 1. 策略合规的代理推理\n\nInterWhen在模型到达最终答案之前验证中间推理状态、工具使用决策和工具响应，确保代理采取的行动符合提供的策略。这对于代理工作流尤为重要，因为早期错误可能传播为不可逆的工具调用或无效的任务结果。\n\n### 2. 生成过程中的验证\n\nInterWhen在推理轨迹生成时即进行验证，无需外部步骤提取或结构化分解。这使得模型能够保持灵活的推理策略，同时仍受制于正确性约束。\n\n### 3. 异步高效执行\n\n验证器异步执行，仅在检测到违规时进行干预，在正确执行上增加的开销可忽略不计，同时保持响应性。\n\n### 4. 统一的模型-验证器接口\n\n框架提供了语言模型与不同类型验证器之间交互的通用API。根据领域目标，验证器可以是符号型、神经符号型或完全神经型，可作用于部分输出、最终答案或两者。\n\n---\n\n## 学术研究贡献\n\nInterWhen为语言模型可靠性研究做出了以下重要贡献：\n\n**测试时扩展的新维度**\n\n传统上，测试时扩展主要通过增加模型规模或采样数量来实现。InterWhen引入了验证器计算作为推理时扩展的额外维度——通过将计算资源分配给结构化验证，可以在不增加模型规模的情况下提升性能。\n\n**自动验证器合成**\n\nInterWhen提供了从自然语言策略自动生成验证器的方法。研究团队还提出了基于Lean的变体，可生成形式化规范、对应的验证器以及验证器代码正确性和完备性的机器检查证明。\n\n**验证器开发的测试平台**\n\n框架支持在推理时系统评估验证器设计，使研究人员能够在将验证器纳入训练目标（如奖励模型或评判标准）之前对其进行测试和优化。\n\n---\n\n## 实验评估与结果\n\nInterWhen在多个基准测试上进行了评估，涵盖规划、数学、逻辑和深度研究任务，包括Maze迷宫、Game of 24、SpatialEval、Verina等。\n\n评估使用了多种目标模型，包括Qwen2、Qwen3和Phi-4系列。实验结果表明，InterWhen能够在给定计算预算下提高语言模型的准确性，或在给定准确性下提高模型效率。\n\n### 典型应用场景演示\n\n**电信领域代理合规演示**\n\n在Tau2-Bench电信领域测试中，验证器首先从策略规则生成。随着代理执行进展，每个工具调用都会根据适用的策略验证器进行检查，违规时返回反馈。演示展示了InterWhen如何在不重启代理的情况下引导相同轨迹朝向策略合规执行。\n\n**Maze数据集演示**\n\n任务要求找出从起点到终点路径中的右转和左转次数。绿色表示通过验证的步骤，红色标记失败的步骤。右侧文本流是验证器输出。\n\n**ZebraLogic数据集演示**\n\n任务要求根据约束条件找出正确分配。同样使用颜色标记验证结果，直观展示验证过程。\n\n---\n\n## 局限性与使用建议\n\n尽管InterWhen展现了强大能力，研究团队明确指出了其适用范围和局限性：\n\n**适用范围**\n\n- 适合验证可行的任务，如数学、代码推理或结构化文档生成\n- 不适合高度主观任务（创意写作、开放式观点文章），因为这些任务难以形式化定义正确性\n- 当前主要针对英语设计，其他语言性能可能有所不同\n\n**使用限制**\n\n- 目前为研究和实验目的开发，商业应用前需要进一步测试和验证\n- 支持基于人工反馈的监控，但在模型输出延迟是关键考虑因素的场景中可能不可行\n- 继承了所用语言模型的训练数据偏差，可能被AI生成的解释放大\n- 尚未系统性地防范间接提示注入等安全漏洞\n\n研究团队强调，使用InterWhen的系统的所有决策都应有人工监督，不应仅基于系统输出。\n\n---\n\n## 开源意义与未来展望\n\nInterWhen的开源为推理模型可靠性研究提供了重要工具。通过将验证机制直接嵌入生成过程，它为构建更可信的AI系统开辟了新路径。\n\n该框架的发布体现了微软研究院对负责任AI的承诺，同时也为学术界和工业界提供了可复现的研究基础。随着AI系统在越来越多关键领域部署，类似InterWhen的验证框架将成为确保系统可靠性的重要组成部分。\n\n研究团队欢迎社区反馈和合作，可通过GitHub Issue或邮件联系。