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

微软研究院推出的InterWhen框架，通过测试时验证机制在推理过程中实时检查中间状态，确保语言模型输出符合预设策略，为高风险场景（如代码生成、数学推理、代理工作流）下的可靠推理提供新思路。该框架已开源，支持从自然语言策略自动生成验证器，并在推理时引导模型轨迹合规。

在高风险AI应用场景中，传统方法仅在模型生成最终答案后验证，存在两大缺陷：

1. 早期错误难以挽回：代理工作流中早期违规或不可逆错误，最终验证时已无法补救；
2. 实例级可靠性不足：仅验证最终输出无法保证推理过程正确性。InterWhen框架通过实时验证中间轨迹解决这一问题。

InterWhen的核心理念是验证器引导的推理，采用"LLM-Process-Modulo"执行模式：

• 离线阶段：将自然语言策略自动生成代码验证器，甚至Lean规范及机器可检查证明；
• 在线阶段：流式生成推理轨迹，通过轻量级边界（段落分隔、工具调用事件等）决定检查时机，持续监控中间状态。

InterWhen的关键技术包括：

1. 状态提取与异步验证：从轨迹提取变量（工具名称、参数等），验证器返回True/False/Unknown状态，验证与生成并行；
2. 干预与恢复：验证失败时中断生成，回滚到检查点并附加反馈，恢复生成；对不可逆操作（如写入）进行阻塞式验证。

InterWhen的核心特性：

1. 策略合规代理推理：验证中间推理、工具使用及响应，确保代理动作合规；
2. 生成中验证：无需外部步骤，保持模型推理灵活性；
3. 异步高效：验证异步执行，正确时开销可忽略；
4. 统一接口：支持符号型、神经符号型等多种验证器，适配不同领域需求。

InterWhen在Maze、Game of24、SpatialEval等基准测试中验证，使用Qwen2、Phi-4等模型，结果显示：

• 提高给定计算预算下的准确性；
• 或在给定准确性下提升效率。 典型场景演示包括电信代理合规（引导轨迹合规）、Maze路径计数（颜色标记验证步骤）、ZebraLogic约束分配（直观展示验证过程）。

InterWhen的适用范围与限制：

• 适用场景：适合数学、代码推理等可形式化任务，不适合主观任务（创意写作），当前主要支持英语；
• 使用限制：研究阶段，商业应用需进一步测试；延迟敏感场景可能不可行；存在训练数据偏差；未防范间接提示注入；
• 建议：所有决策需人工监督，不可仅依赖系统输出。

InterWhen开源为推理模型可靠性研究提供工具，开辟可信AI系统新路径。体现微软研究院负责任AI承诺，为学术界和工业界提供可复现基础。随着AI在关键领域部署，此类验证框架将成为确保可靠性的重要组成部分。欢迎社区通过GitHub Issue或邮件合作反馈。