《AI》：Which Decisions Live in the Provable Layer? Formally Verified Safety Constraints for Agentic Clinical AI, with a Whole-Person Longitudinal Benchmark
编辑推荐：
临床人工智能（AI）系统开始在整个护理过程中行动，而非一次回答一个问题。其安全性通过采样输入空间的方法检查：一个测试套件尝试一些输入，一个语言模型评审员阅读一些案例，一个医生小组审计一些案例。采样检查可以通过一条安全规则，但仍可能遗漏破坏规则的罕见输入，例如一
临床人工智能（AI）系统开始在整个护理过程中行动，而非一次回答一个问题。其安全性通过采样输入空间的方法检查：一个测试套件尝试一些输入，一个语言模型评审员阅读一些案例，一个医生小组审计一些案例。采样检查可以通过一条安全规则，但仍可能遗漏破坏规则的罕见输入，例如一个记录在案的义务在几次就诊后被丢弃。本研究衡量了这一差距，并发布了CIV-Bench，一个公开基准，包含832个临床规则集，涵盖八个全人领域的安全属性，采用单次就诊和纵向形式，外加一个计算压力层级，每个规则集均具有独立确立的地面真相。研究人员比较了形式化验证（使用可满足性模理论（SMT）求解器一次性检查所有可能输入）与实践中的方法：随机单元测试、语言模型评判员以及一个盲法医生小组。形式化验证检测了所有612个违规，未产生假警报，未返回不健全判决；对于每个项目，它要么返回一个规则在所有输入上成立的证明，要么返回一个具体破坏规则的输入。一个前沿语言模型评判员匹配了此检测率，但它返回的是采样案例上的通过率而非保证，且每个项目消耗的计算量高出三个数量级。通用开源权重评判员在计算压力层级上返回了不健全判决；医学微调评判员的不健全情况更为广泛，在纵向属性上崩溃，尽管在单次就诊医学检测上表现强劲，因此医学微调并未缩小差距。单元测试和医生小组遗漏了那些维持整个护理过程的深层、跨就诊违规。形式化验证的区别不在于更高的检测率，而在于其返回的证据类型：一个覆盖整个输入空间的证明、一个可重放的反例、或一个明确声明无法判定的结果。该保证适用于放置在此层中的决策，并且依赖于安全规则被正确指定。
**研究背景**
当前临床人工智能（AI）系统正从单次问答转向覆盖整个护理过程。其安全性检查主要依赖采样方法，如随机测试套件、语言模型评审或医生审计，这些方法只能验证部分输入，可能遗漏罕见但关键的安全违规，例如跨就诊的义务丢失。采样方法无法提供覆盖整个输入空间的保证，尤其在纵向护理中，安全义务需在多次就诊间持续。因此，亟需一种能提供确定性保证的形式化验证方法，并建立基准来系统比较不同方法。
**研究人员开展的研究**
研究人员发布了CIV-Bench——一个包含832个临床规则集的公开基准，涵盖八个全人领域（分诊、药物安全、检查、鉴别诊断、心理健康、治疗偏好、物质使用、未满足社会需求）及一个计算压力层级，每个规则集具有独立确立的地面真相。他们比较了形式化验证（使用可满足性模理论（SMT）求解器Z3）与当前实践方法：随机单元测试、语言模型评判员（前沿模型、通用开源模型Qwen3-8B、医学微调模型MedGemma-27B）以及盲法医生小组。验证器将规则集编译为SMT约束，对决策规则检查不变量是否不可满足，对转换系统使用有界模型检验和k-归纳。结果表明，SMT验证检测了所有612个违规，无假警报，无不健全判决，平均每项3毫秒；前沿模型同样检测所有违规但需5.9秒/项；开源模型在计算压力层级产生17个不健全判决；单元测试漏检43个违规；医学微调模型在纵向属性上崩溃，仅检测17.7%的纵向违规并产生208个不健全判决。医生小组在120项子集中检测81.3%违规，但在深度和纵向项目上表现弱。该研究还验证了三个已发表临床指南（美国儿科学会发热婴儿指南、美国妇产科医师学会妊娠高血压指南、美国心脏协会/美国卒中协会缺血性卒中指南），证明形式化验证能发现转录错误。
**结论**
概率保证方法无法提供覆盖整个输入空间的证明，单元测试和医生小组在深层、跨就诊属性上失败，前沿模型虽检测准确但无保证且成本高。SMT形式化验证返回不同证据类别：整个输入空间的证明、可重放反例或明确弃权，且无不健全判决。该保证适用于有限符号层中的决策，但依赖于正确规范。基准、验证器和分析已发布，供独立复现。
**意义**
为临床AI系统提供可审计的保证，指导哪些决策应置于可证明层，推动分层保证框架的建立。
**技术方法**
主要关键技术包括：1）SMT验证：使用Z3求解器将规则集编译为SMT约束，通过检查不变量不可满足性返回证明或反例；2）有界模型检验与k-归纳：用于转换系统的纵向属性验证，时间盒限制为5秒，若无法判定则返回弃权；3）基准生成：确定性构造器基于模板实例化规则集，独立预言机通过穷举枚举或广度优先搜索确定地面真相，不使用求解器；4）比较方法：随机单元测试（1000/10000/100000样本）、语言模型评判（前沿、Qwen3-8B、MedGemma-27B，零样本，温度0，约束JSON输出）、盲法医生小组（120项分层子集，临床推理，无地面真相）。样本来源为合成数据，无患者数据，三个指南来自AAP、ACOG、AHA/ASA。
**研究结果**
**3.1 Detection, Soundness, and Cost**：在832项基准上，SMT验证检测所有612个违规（100%），无假警报，无不健全判决，平均3ms/项；前沿模型同样检测所有违规但需5.9s/项；开源模型Qwen3-8B检测98.4%违规但17个不健全判决（均在压力层级）；单元测试检测93.0%违规但43个假安全判决；医学微调模型MedGemma-27B检测69.9%违规，208个不健全判决，28.2%假警报，在纵向属性上仅17.7%检测率，表明医学微调未提供纵向推理能力。
**3.2 The Blind Spot of Sampling, by Depth**：通过深度分析，单元测试检测率随交互/就诊/计算深度下降（深度12时35.7%），逻辑回归斜率-0.59（95% CI -0.71至-0.46），而验证和前沿模型不随深度变化。配对McNemar检验确认验证显著优于单元测试（P=2.3×10
-13）。单元测试的假安全数量随样本量增加而减少，但所需预算未知。
**3.3 Human-Expert Panel**：盲法医生小组在120项子集中检测81.3%违规，1个假警报（在40个成立项中）。一致率中等（Fleiss kappa 0.52，Gwet’s AC1 0.64），在纵向和压力层级上检测较弱（纵向21/26，压力4/12）。验证和前沿模型在同一子集中检测全部80个违规。
**3.4 Counterexample Case Studies**：两个反例说明纵向机制：社会需求在早期就诊记录后，错误维护路径在无解决事件下清除义务，单元测试返回假安全；药物规则中高优先级规则重新启用被安全守卫禁用的药物，验证返回反例并证明修正后规则无此类轨迹。
**3.5 Application to Published Clinical Guidelines**：对三个指南进行验证：1）AAP发热婴儿指南：忠实编码被证明安全，省略绝对中性粒细胞计数标准后返回反例（22天婴儿ANC>4000被错误出院）；2）ACOG妊娠高血压指南：忠实编码被证明安全，将“或”误写为“且”后返回反例（孤立重度收缩压被遗漏治疗）；3）AHA/ASA缺血性卒中指南：忠实编码被证明安全，遗漏舒张压阈值后返回反例（禁忌舒张压患者接受溶栓）。验证定位了转录错误。
**总结讨论部分**：概率保证方法（单元测试、语言模型评判、医生小组）在深层、跨就诊属性上失败，因为它们是采样统计系统，无法提供整个输入空间的证明。SMT验证在有限符号层上返回不同证据类别（证明、反例、弃权），且无不健全判决。前沿模型虽检测准确，但无保证且成本高（三个数量级）。医学微调模型在纵向属性上崩溃，表明领域对齐不提供跨就诊推理能力。提出分层保证框架：内容安全护栏（概率监测）、单元测试（具体证据）、运行时监测、SMT验证层（全空间证明）、定理证明核心（最严格小规模）。验证器弃权时路由至下一层并标记人工审查。局限性包括：未运行内容安全护栏、基准为有限合成、规范编写需人工、保证有条件于正确规范。
**翻译研究结论部分**：概率保证方法是统计系统，无法提供整个输入空间的证明。当前主导的质量保证实践——单元测试——在违规见证罕见时报告假安全，盲法医生小组显示相同限制；在本基准上，两者均在表征纵向全人护理的深层和跨就诊属性上失败。一个前沿推理模型虽然在检测上准确，但返回的是样本统计量而无保证且成本显著更高，且该区别是能力不变的而非绑定于特定模型版本。SMT形式化验证一个有限符号临床规则层返回不同证据类别。它证明整个输入空间上的不变量，展示可重放反例，或弃权，且在本基准上，在报告求解器超时为弃权而非安全的纪律下，它未返回任何与地面真相矛盾的判决。一个机器可检查的证明或明确弃权是直接可审计的，这一属性与智能体临床系统的治理和部署准备相关。基准、验证器和分析已发布，以便任何团队可以对其自身规则集运行测量。临床AI的设计问题是：哪些决策存在于可证明层。
