代理模型检查

验证 LLM 生成的系统代码很困难：错误普遍存在，缺少正式规范，安全契约在调用站点隐式编码，而不是在函数边界强制执行。我们提出了代理模型检查，这是一种将 LLM 代理与有界模型检查后端结合起来的范例，其原理是代理提出，求解器验证：代理处理需要语义判断的任务（规范推理、检查选择、反例分类、细化建议），而 BMC 则执行每个与健全性相关的决策。该范式基于三个承诺。规范是从受限 DSL 中的调用者上下文中自上而下推断出来的，确定性地转换为后端的假设/断言原语，并具有可选的功能正确性子句，将验证从无恐慌提升到行为 忠实性。验证是组合性的：每个函数都根据其规范进行独立检查，并用后置条件约束的存根替换被调用者，因此每个查询的成本随单个函数的状态空间而变化，并且细化会自动传播给调用者。反例不是错误报告：它们通过验证管道（可达性、被调用者可行性、动态重播、真实性审核）来区分活动的树内崩溃和潜在的公共 API 故障，而建模工件则驱动细化循环而不是被抑制。我们在 BMC-Agent 中实例化该方法，并在 LLM 生成的 C 和 Rust 内核和编译器代码以及成熟的 OSS-Fuzz 强化库上对其进行评估，确认真正的缺陷，在严重模糊的表面上产生有界的干净验证，并在选定的算法函数上建立功能等效性。