TGMS用计划契约与证据契约让数据库智能体的无效计划可拒、声明可查
核心概要
该工作提出面向LLM智能体的两项可执行契约：计划契约在执行前校验计划结构、结果字段引用与标识接地，证据契约记录结果的双时态信念状态、完整性与来源，并据此核验声明；在TGMS双时态图系统上，结果字段检查把无效引用转为可修复的拒绝，完整性传播在15个受控用例中全部检出截断计数错误，声明门控使199条输出答案中不再含无支撑声明，代价是少输出21条答案。
Figure 1: The plan contract checks admissibility before execution. Execution produces annotated results, and the evidence contract checks the resulting claims. The contracts do not guarantee intent interpretation or operator choice.
arXiv · 第 3 页深度剖析
提出并形式化两项契约：计划契约规定智能体可执行与可引用的内容，证据契约记录结果支持声明时的信念状态、完整性与来源，并给出三条保证——计划可采纳性、执行可复现性、声明忠实性。 以往工作多关注如何获得有用计划并高效执行，输入模式只约束进入操作的值，值接地只校验数值与实体一致；该工作把约束放在执行前与执行后两个边界上，并明确保证范围不包含任务正确性。 契约以TGMS实现并评估：13个时序算子各在500个随机用例上与独立暴力预言机比对；执行确定性通过结果规范化序列化与SHA-256摘要复现来体现。
结果字段检查把模型引用不存在结果字段的失败从运行时错误转为执行前的结构化可修复拒绝。 首次实机探测中所有生成计划都通过参数校验却无一成功执行，因为计划引用了产出算子未返回的字段（如s2.count而非s2.rows_total）；加入结果模式与跨步引用检查后，三任务探针集执行成功率由0/3升至3/3，7B消融中执行成功率由0.23升至0.55。 三任务探针集、7B与14B消融对比，以及语法约束解码未解决该不匹配的对照实验；作者指出该失败是语义性的而非纯语法性的。
完整性传播使基于不完整页面的计数无法支撑关于完整结果的声明，声明门控据此在输出前移除无支撑声明。 值接地无法发现该错误，因为所报实体与派生计数同可见页面一致；TGMS记录rows_total与截断标志、将不完整性沿依赖步骤传播并纳入声明核验。 受控生成器中15/15检出、关闭后0/15检出；自然开发集仅3个判定改变；CollegeMsg冻结战役中门控前220条答案有21条含无支撑门控声明，门控后199条全部通过，代价是少21条答案与总体准确率下降一个百分点。
在冻结工作负载上，固定算子接口并非普遍准确率优势：CollegeMsg上TGMS达0.408类型化答案准确率，高于所评估基线的0.064–0.284，但在Bitcoin-OTC上与同一双时态存储上的直接SQL持平。 同信息SQL基线使用相同双时态DuckDB表、相同模型与修复预算，仅改变查询语言、计划表示与静态检查，因此比较的是两种接口设计而非单一机制；修正探针上TGMS与双时态SQL均能回答历史信念问题，而最新状态基线不能。 四个冻结工作负载测试集分别为94、94、102、94个任务，主配置为Qwen2.5-14B-Instruct-AWQ温度0，CollegeMsg聚合三个种子；作者说明email-EU与合成工作负载的增益置信区间含零，属正向但不结论性。
启示与展望
该设计面向需要在记录可被更正后仍能复现历史判断的场景，例如审计与合规查询，以及计划由多步算子组合、部分结果会改变答案含义的工作负载。对使用者而言，计划契约使无效计划在执行前被拒绝并附带结构化修复信息，证据契约使被门控的声明忠实于其引用证据，且契约开销很低：计划准入p50为4.1毫秒，声明核验为3.3毫秒，合计远低于端到端任务时间的0.01%。提示规模不随原始图规模增长，测试规模下每任务保持6,000至10,000个token。该结果适用于当前代数可表达的问题，以及当前被门控的声明类型。
保证范围仍限于当前被门控的声明类型，时序模式声明会被检查但尚未被扣留；核验器是已实现并经变异测试，而非形式化验证。成员检查无法确立集合完整性：核验器确认每个所报实体出现在证据中，但在100个遗漏有效成员的案例中一个都未检出，因此完整集合声明需要更强的证明义务。由于双时态SQL基线未实现证据契约，评估并未确立声明检查必须依赖固定算子代数。独立撰写问题研究规模较小：110个问题中仅10个可由当前代数表达，其中仅5个的答案类型受当前评分器支持，跨三个种子产生9次CollegeMsg与6次Bitcoin-OTC运行。近似算子与智能体写回不在当前原型范围内。