LASER：面向长距离协议依赖的可废止证书搜索

LASER 是一种带证明的搜索方法，用于处理稀疏、可废止的协议证据，将缺失支撑与未决修正表示为显式义务，由符号检查器判定证书是支持、反驳还是无法判定某行为。在 91 个 BehaviorCheck 家族、2K 预算下，LASER 在两个模型家族上把 Joint Edge+Proof 提升 Δ=+.132（p=.017）和 Δ=+.198（p<.001），假发现减少 2–3 倍。