Page 61 - 《软件学报》2025年第8期

3484 软件学报 2025 年第 36 卷第 8 期

的失败分支中提取失败信息.
本文提出的剪枝算法在算法 1 中描述. 我们首先确定学习的程序的最大子句数 N 和发明谓词 M. 我们通过搜
[
]
索其对应的 SLD-树来证明每个例子 Atom ∈ E. 在探索过程中, 如果要被证明的 Atom = P|Args 是一个常量化目
[ ]
标, 我们提取其失败信息为 Goal f = Depth,Sig,P|Args , 其中 Depth 表示剩余子句的数量, Sig 代表谓词签名. 否则,
([ ] [ ])
v
如果 Atom 是一个非常量化目标, 我们首先通过子句 extract P|Args , P|Args ′ 提取 Atom, 该子句用统一符号 替
[
]
′
′ Goal f = Depth,Sig,P,Args |H . 注意, 在一阶
换 Args 中的所有匿名变量以得到 Args . 然后, 我们提取其失败信息为
系统中有一个附加的剪枝条件以防止正确的程序被移除. 在第 4.1 节中将解释在一阶系统中引入此条件的原因.
)
(
随后, 算法 1 首先检查动态 faulty 数据库 DB 中是否已经记录了子句 faulty Goal f . 一旦在数据库中发现该
子句, MIL 学习器将跳过证明过程并回溯到前一步以证明其他目标. 如果数据库中未记录 Atom 的失败信息, 即
( )
faulty Goal f , 则应立即将其添加到数据库中, 并在下一步中证明 Atom. Atom 的证明过程由通用元解释器完成. 一
旦所有目标都被证明, 一个一致的假设 H 将被完成并返回. 在生成假设后, 失败数据库中的所有事实或子句将被
移除.
定理 1 (算法 1 的正确性). 给定背景知识 B、实例集 E =< E ,E > 和元规则集 MS, MIL 的任务是找到一个程
+
−
+ − e ,B,H/ ⊨ e . 可以断言, 算法 1 的操作不会从程序空间中删除正确的程序
−
−
序 H 使得 B,H ⊨ E 并且对于 E 中的所有 H.
证明: 我们通过数学归纳法证明该定理. 设 N 为最大子句数, M = N −1 为最大发明谓词数, S 为子句理论集,
即程序空间. 根据 MIL 的深度优先搜索策略, 程序空间 S 可以分为 S 1,0 ∪S 2,0 ∪S 2,1 ∪...∪S N,0 ∪...∪S N,N−1 . 其中元
i
j
s ∈ S i,j (1 ⩽ i ⩽ N,0 ⩽ j ⩽ M) 是具有 条子句和 个发明谓词的程序.
素
情况 1. 首先考虑 N = 1 的情况. 在这种情况下, 程序空间为 S = S 1,0 . 算法 1 在这种情况下不起作用. 因此程序
空间不会减少, 正确的程序 H 不会被删除. 因此, 该定理成立.
情况 2. 假设当 N = k(k ⩾ 2) 时, 定理 1 成立. 设程序空间为 S = S 1,0 ∪S 2,0 ∪S 2,1 ∪...∪S k,0 ∪...∪S k,k−1 , 所有由算
法 1 找到的常量化目标和非常量化目标构成一个失败集 F k . 因此, 每个元素 f ∈ F k 都被证明是失败的. 也就是说,
由失败目标 f ∈ F k 生成的程序不可能是正确的程序.
情况 3. 我们考虑 N = k +1 的情况. 程序空间为 S = S 1,0 ∪S 2,0 ∪S 2,1 ∪...∪S k,0 ∪...∪S k,k−1 ∪S k+1,0 ∪...∪S k+1,k . 失
F k+1 = F k ∪ F . 根据情况 2, F k 的失败目标生成的程序不可能是正
′
败集为 S 1,0 ∪S 2,0 ∪S 2,1 ∪...∪S k,0 ∪...∪S k,k−1 中由
确的程序. 现在我们只需要证明由失败目标生成的剩余集 S k+1,0 ∪...∪S k+1,k 中的程序不可能是正确的程序. 设
s = {s 1 , s 2 ,..., s i ,..., s k+1 } ∈ S k+1,0 ∪...∪S k+1,k 为 MIL 学到的程序, 其中 s 包含 k +1 条子句且 s i = Atom : −Body 是程
i
i
i
序的第 i 条子句. 很容易发现, Atom 的失败信息不会出现在失败数据库中. 否则, 算法 1 将其识别为失败并进行回
i
溯, Atom 无法生成正确的程序.
综上所述, 算法 1 的操作不会删除程序空间中的正确程序.
引理 1 (MIL 假设空间 [20] ) 给定 p 个谓词符号和 m 个在 M 中的元规则, 当元规则的体中最多有 个文字且每
i
j
j
)
i ( j+1 n
个文字最多有 i 个参数时, 该元规则属于片段 M . 用 n 条子句表达的程序数目最多为 mp .
j
由于子句数从 1 增加到 n, 我们可以通过引理 1 汇总 MIL 任务搜索空间中的程序数目. 结果 (即 MIL 搜索空
间) 被形式化为推论 1.
推论 1 (MIL 搜索空间). 给定 p 个谓词符号和 m 个在 M 中的元规则, 当元规则的体中最多有 j 个文字且每个
i
j
∑ ) k
n (
i mp j+1 .
文字的参数最多为 i 时, 该元规则属于片段 M . 由最多 n 条子句组成的所有可能程序的数量为 k=1
j
推论 1 表明 MIL 的搜索空间可以根据程序子句的数量分为多个子空间. 这些子空间中的程序可能包含相同
的子程序. 因此, 这些子程序被反复证明和计算.
定理 2 计算剪枝后的 MIL 搜索空间中的程序数目 (其中所有子程序仅被证明一次) 并估计通过剪枝减少的
MIL 搜索空间的比例.
定理 2 (剪枝后的 MIL 搜索空间). 假设有无限量的内存可用, 给定 p 个谓词符号和 m 个在 M 中的元规则, 一
i
j
l l = 1,2,...,n−1. 设
个程序包含最多 n 条子句, 剪枝子树的深度为 , t = mp j+1 , 通过修剪常量化目标和非常量化目