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

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


                 其中,  ite(a,b 1 ,b 2 ) 表示若  a 为真, 则  , 否则为  . 假设我们要证明   sorted(insertsort(xs)) 成立, 即插入排序后的  list
                                                    b 2
                                            b 1
                 被正确排序, 通过对      xs 进行结构归纳可以得到基础步骤和归纳步骤:

                                         
                                         sorted(insertsort(nil)) = ⊤
                                         
                                                                               .
                                         
                                          sorted(insertsort(xs)) → sorted(insertsort(x :: xs))
                    对上述的归纳步骤应用归纳定义重写可得到:

                                        sorted(insertsort(xs)) → sorted(insert(x,insertsort(xs)),
                                            insertsort(xs). 于是可以应用泛化技术生成辅助子公式:
                 注意到这个公式两边有相同的子项

                                                sorted(ys) → sorted(insert(x,ys)),
                 这一公式具有更简单的形式, 将会更易于定理证明工具进行求解.
                    这一技术在定理证明工具          ACL2 [36] 、Zeno  [37] 中均有所实现. 本文第  3  节中提到在  superposition  推理系统中引
                 入泛化归纳技术也可以视作是这一类子公式生成技术. 这一技术的优势在于当合适的泛化方法被使用时, 可以快
                 速高效地找到正确的子公式. 但这一方法容易产生过度泛化的问题, 而且在证明系统中何时应用泛化没有一个统
                 一的原则, 只能根据具体的问题和推理系统选择启发式方法.
                    基于失败证明生成辅助引理: 主要思路是当证明失败时, 通过分析造成失败的原因然后尝试生成对应的辅助
                 引理. 这一方法在早期基于重写规则的定理证明系统受到关注, 发展出了                        rippling [38] 方法, 在自动定理证明系统
                 RRL  [39] 中也实现了类似思路的方法用于自动生成归纳引理. 另外              Murali 等人  [40] 对于带有最小不动点定义的一阶
                 逻辑问题, 提出了一个利用一阶逻辑推理过程中计算出来的反例模型来引导生成归纳引理的方法. 这一类型技术
                 的优势在于应用时机相比基于泛化的方法更加明确, 且可以找到一些泛化技术无法找到的引理项. 缺点在于该方
                 法的使用可能依赖启发式方法, 且可能生成过于复杂的公式导致搜索空间增大, 反而造成求解效率下降的问题                                  [41,42] .
                    基于理论探索      (theory exploration) 生成引理: 该方法的思路是从可用的符号, 包括函数和代数数据类型构造子
                 等, 来构建一个候选引理集合, 在构造时主要通过枚举或公式模板等方法, 然后通过反例检查, 或者启发式的过滤
                 方法来从候选集合中生成相关的引理用于证明原命题, 然后基于这个引理集合来证明待验证公式                                 [43,44] . 这一方法
                 的应用和发展比较广泛, 我们在第           2.4.1  节中提到在  SMT  求解器中进行子目标生成的方法则可以归于这一类, 其
                 中通过公式项的      size 来枚举候选引理. 而    Yang  等人  [45] 则是通过语法定义可能的公式模板来生成引理. Sivaraman
                 等人  [46] 提出将引理生成问题转换为一个数据驱动           (data-driven) 的程序综合问题. 并提出了一些用于过滤子引理和
                 评估候选引理的技术. 这一方法的效率决定于对候选引理集合的评估方式, 即如何找到与证明目标最相关的引理,
                 缺点在于难以生成比较复杂或规模较大的引理, 因而能处理的问题规模受到限制, 可扩展性                            (scalability) 可能受限.
                    归纳友好的引理生成: 针对现有方法在生成辅助引理时过于依赖基于启发式方法的枚举等技术, 推理过程中
                 生成大量无用引理而造成求解时间浪费的问题, Sun 等人               [47] 提出了一种“定向引理生成      (directed lemma synthesis)”方
                 法. 该方法首先定义两种称为“归纳友好            (induction-friendly)”的公式形式, 在这种形式的公式上可以高效地应用归
                 纳假设进行归纳推理. 然后问题则转变为如何将待验证目标转换为归纳友好形式的公式. 这项工作中提出了两种
                 技术通过生成和应用辅助引理来进行转换, 其中生成合适引理的主要思路是将引理生成问题转为一个程序合成问
                 题, 其中待合成的程序是一个给定的递归结构的函数模板. 由于待生成函数具有较清晰的函数结构, 使用现有的程
                 序合成工具可以较好地完成这一合成任务. 这一方法相比非定向基于枚举生成引理的方法, 可以较为有效地减少
                 无用引理所浪费的时间, 其局限性是目前只能处理等式的问题, 另外求解效率比较依赖后端的程序合成工具.
                  2.5   求解递归函数可满足性赋值技术

                    前文主要介绍使用       SMT  求解器证明递归函数性质成立          (即求解器返回     UNSAT) 的技术. 与之相对, 本节我们
                 简单介绍和讨论      SMT  求解器寻找递归函数可满足性赋值           (返回  SAT  并给出反例) 的工作.
                    该方向面临的主要挑战和代表性工作: 递归函数可满足性求解需要考虑参数取值可能为无穷域                                  (如整数或
                 ADT  类型) 的问题. 对包含全称量词和未解释函数公式的否定形式寻找可满足模型, 传统的量词实例化方法                               [48,49]
                 表现较差. Reynolds 等人  [50] 在  2016  年提出一种转换技术, 该技术通过定义抽象类型, 并给抽象类型施加约束, 将
   38   39   40   41   42   43   44   45   46   47   48