Page 57 - 《软件学报》2026年第2期
P. 57

536                                                        软件学报  2026  年第  37  卷第  2  期


                 实验一样.
                  5.3   实验结果
                    整数递归函数样例结果如表           5  所示. 对于总的  222  个样例, 如表  5  中加粗数字所示, 基于     SMT  求解和归纳推
                 理算法的求解器      (Z3/cvc5/Vampire) 中求解数最多的工具是     Vampire, 可求解数为   84/222=37.84%, 基于  CHC  归纳
                 不变式生成的求解器       (Spacer/Eldarica) 中求解数最多的工具是    Eldarica, 求解数为  105/222=47.30%. 下面分别介绍
                 在两类样例来源上的表现.

                                           表 5 整数递归函数样例不同求解器实验结果

                      样例来源           总数        Z3      cvc5        Vampire       Spacer       Eldarica
                    文献[55]样例         120       0        29           76           62            84
                    手工构造样例           102       4        29           8            15            21
                      总解出数           222       4        58       84 (37.84%)      77        105 (47.30%)

                    在  120  个文献  [55] 样例中, Eldarica 和  Vampire 解出数最多, Vampire 在这部分样例上求解数达到        76/120=
                 63.33%, 远多于  SMT  求解器  Z3  和  cvc5. 这一表现符合预期. 因为文献    [55] 样例正是  Vampire 团队提供, 他们某种
                 意义上针对这部分样例的形式进行了专门的整数归纳推理优化, 并实现在                         Vampire 中. 相比之下, Z3  没有实现归
                 纳推理, 解出数为     0, 而  cvc5  虽然实现了归纳推理增强, 但它在整数归纳推理上实现较为简单, 无法应对整数变量
                 小于  0, 以及具有非常数边界的情况, 因此         cvc5  可以求解较少数量的例子.
                    CHC  求解器方面的求解能力稍微有些超出预期. 其中              Eldarica 解出了  84/120=70%  的样例, 甚至超过了  Vampire.
                 以往文献中并缺少整数递归函数样例上              CHC  求解器与其他    SMT  求解器或自动定理证明器的对比实验结果, 本文
                 的实验可以作为补充. 结果表明          CHC  求解器即使没有专门实现归纳推理技术, 仅靠基于归纳不变式生成算法在求
                 解整数递归函数的问题上就具有较好的求解能力. 其原因可能是                     CHC  求解器对整数理论的支持较好, 且整数实验
                 样例中的递归函数形式相对简单, 且性质公式中线性计算为主, 易于                     CHC  求解器计算出归纳不变式, 完成待验证
                 性质的证明.
                    对于  102  个手工构造的样例, 用于实验的工具均表现不佳, 其中求解数最多的是                    cvc5  和  Eldarica, 求解的数目
                 分别为样例总数的       29/102=28.43%  和  21/102=20.59%. 手动构造样例的主要求解难点来源于两部分, 一部分是递归
                 函数定义和相关性质公式, 如取模计算等带来的非线性. 非线性理论的求解一直都是求解理论判定算法中非常具
                 有挑战性的难点问题. 另一部分是根据            bitLen  和递推数列问题中包含的递归函数定义, 求解带有这些递归函数的
                 性质公式依赖强数学归纳法求解. 但目前的求解器归纳推理算法中均没有实现强归纳法. 其主要原因可能是: 1) 强
                 归纳推理的归纳假设需要在公式中额外引入全称量词; 2) 在                  ADT  理论的问题中进行强归纳推理, 需要能够判定
                 任意两个项之间的子项关系          (subterm relation). 这些都将增加求解过程中的计算开销, 带来一定的挑战性. 且现有
                 开源样例中需要通过强归纳法进行自动推理求解的问题比较少, 使得研究者缺少研究动力                              (motivation).
                    总的来看, CHC    求解器基于归纳不变式生成的验证方法和                Vampire 整数归纳技术的引入, 在整数递归函数
                 样例上都具有一定的效果. 主流          SMT  求解器在整数理论的递归函数问题上, 尽管如                cvc5  实现了基于弱数学归
                 纳法的归纳推理增强技术, 但实现较为简单, 无法处理复杂的问题类型. 主流求解器可以完成相对简单的归纳推
                 理或归纳不变式生成的求解任务, 但难以应对复杂计算公式和函数定义的问题. 根据调研和实验结果, 现有工作
                 对于整数递归函数       SMT  公式自动求解的研究非常欠缺. 其原因可能是: 整数归纳推理问题更多来源于数学背
                 景  (如本文中提供的斐波拉契递推数列问题) 而不是程序验证背景. 对于数学背景问题的求解目前主流思路还
                 是基于交互式定理证明工具           (如  Lean、Coq  等) 进行人工证明而不是机器自动证明. 因此学术界对自动归纳推
                 理证明的研究更偏向从程序验证背景中获得的                 ADT  相关问题, 从而缺少整数理论         SMT  公式自动归纳推理的开
                 源样例和研究工作. 但随着当前人工智能的流行, 许多人开始对人工智能辅助进行数学问题的自动求解感兴趣,
                 作为自动求解的底层引擎, 对带有整数递归函数的                 SMT  公式进行归纳推理等自动求解的技术或许将成为未来
                 的研究热点.
   52   53   54   55   56   57   58   59   60   61   62