First-Order Logical Premise Selection Method Based on Symbol Weight
-
摘要:
为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力，首先，提出符号权重计算公式，基于符号在问题中出现的频率获取不同符号对应的权重；其次，提出相关度计算公式，利用分配的符号权重计算问题中前提和结论间的相关度；同时，研究自适应相关度边界，用于判断前提与给定的结论是否相关；最后，在自动定理证明器中交互地结合前提选择和自动推理两个过程，可在充分选择相关前提的情况下及时停止前提选择过程. 实验结果表明：在最优情况下，新提出的前提选择方法能够把参与证明的平均前提数量从1876个降低到174个；与广泛使用的前提选择方法E-SInE和Vampire-SInE相比，使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.
Abstract:To enhance the ability of automated theorem provers to select relevant premises from large-scale premises of first-order logic problems, a symbol weight calculation formula is first proposed, obtaining various weights corresponding to different symbols based on the frequency of symbols in the problem. Secondly, the correlation calculation formula is proposed, using assigned symbol weights to compute the correlation between a premise and the conjecture in a problem. At the same time, the adaptive correlation boundary is studied, which is used to determine whether the premise is correlated with the given conjecture. Finally, both processes of premise selection and automated reasoning are interactively combined in automated theorem provers, achieving the goal of stopping the premise selection process in time when the relevant premises are fully selected. The experimental results show that in the optimal case, the proposed premise selection method can reduce the average number of premises involving in proving process from 1876 to 174, and compared with widely used premise selection methods E-SInE and Vampire-SInE in automated theorem provers, the propoed method can help the automated theorem prover E improve the proof rate by 19.49% and 10.49% respectively on the MPTP2078 benchmark.
-
Key words:
- premise selection /
- automated theorem proving /
- first-order logic
-
自动定理证明是人工智能的核心部分之一，致力于生成高效的计算机程序，从而使计算机能够完全或几乎完全自动地进行推理. 即，将形式化为一阶逻辑公式的前提和结论作为计算机程序的输入，并试图利用程序自动从前提中推导出结论. 这样的程序通常被称为自动定理证明器（automated theorem prover，ATP）.
随着形式化技术的发展，ATP的应用范围从理论上的数学定理逐渐拓展到知识编译[1]、软（硬）件模型检验[2-5]、管理规划[6-7]、集成电路设计[8-10]及软件测试[11]等实际问题上. 因此，旨在推理小规模数学问题的ATP越来越多面对从一些大型知识库（CYC[12]、SUMO[13]以及Mizar[14]等）和实际应用中转换而成的大规模的问题. 这些大规模问题通常被称为大理论（large theory），通常包含成千上万个前提，但是仅有非常少的一部分前提才对问题结论的证明有用. 大规模的冗余前提集会使得ATP在证明问题时搜索空间呈指数型增长，甚至可能立即超出计算机的运行能力，这大大地限制ATP自动推理能力. 假设可以直接使用在证明中出现的前提，ATP则能够轻松快速地证明问题的结论. 因此，从问题中去除不必要的前提，可以减少搜索空间，并降低搜索难度. 在ATP开始证明之前选择出对问题结论证明有用的前提的过程被称为前提选择（premise selection）. 前提选择是ATP预处理中非常关键的一环，对解决大理论的自动推理至关重要.
早期的前提选择方法[15-16]通过不断对当前选择的前提和结论否定的模型进行语义分析来指导前提的选择. 然而，基于语义的前提选择方法非常耗时，且严重依赖模型检查器的能力. 随后，一些基于符号相关性的前提选择方法[17-19]不断被提出. 此类方法主要通过计算和比较出现在公式（前提和结论）符号中，分析公式间的相关性. 当前，一些机器学习[20-22]和深度学习[23-27]技术也开始应用在前提选择中. 基于学习的前提选择方法强烈地依赖于大规模成功证明的领域经验，需要从形式化证明构造不同领域（如集合论、代数以及管理等）问题的语料库. 然而，在形式化时不同领域问题使用的符号是随机制定的，使得对应的语料库无法在学习训练中跨领域通用. 因此，当ATP面临一个新领域中的大规模问题时，由于缺乏新领域中的形式化证明，将导致当此类学习方法在前提选择任务中失效.
因此，从效率和可行性出发，当前ATP主要使用基于符号相关性的方法作为主要前提选择方法. 然而，当前方法终止前提选择过程的条件是，无法再选择任何的前提作为相关前提. 在此情况下，现有方法缺少在选择过程中对所选择前提的充分性进行判断，因此，可能在已经充分选择了相关前提的情况下，仍不会停止选择过程. 这直接导致当前选择过程将大量与结论证明无关的前提标记为相关的. 此外，当前的方法在选择前提时仍需人工设置相关度边界，这导致相关度边界值不具有普遍性和广泛适用性.
针对以上问题，本文提出了一种新的基于符号权重的一阶逻辑前提选择方法SymbolWeight. 新方法通过考虑问题中符号出现的频率，为每个符号赋予不同的权重. 在新的权重定义下，若符号是通用符号（高频符号），其权重就越小；若符号是稀有符号（低频符号），其权重就越大. 新定义符号的权重能够削弱通用符号造成的负面影响，以及体现稀有符号的重要性，从而保证基于新权重的相关度计算更加稳定. 同时，为减少手工参数的数量，提高前提选择的精确度，新方法提出一种自适应相关度边界，用于判断前提是否与结论相关. 此外，为了在充分选择相关前提的情况下及时停止前提选择过程，新方法交互结合了前提选择过程和结论自动推理过程. 实验结果表明，和自动定理证明器中广泛使用的通用前提选择方法相比，新方法能够帮助自动定理证明器E在MPTP2078基准测试集上提高10%以上的证明率.
1. 预备工作
在一阶逻辑[28]中，给定一个变元符号集
$ \mathcal{V} $ 、一个函数符号集$\mathcal{{{F}}}$ 、一个谓词集$ \mathcal{P} $ . 一阶逻辑项是一个变量项$v\;（v\in \mathcal{V} ）$ 或者形如$f\left({t}_{\mathrm{u}1},{t}_{\mathrm{u}2},\cdots ,{t}_{\mathrm{u}{{g}}}\right)$ 的函数项. 其中：$ f({\text{•}})\in \mathcal{F} $ ，是$ g $ （$ g\geqslant 0 $ ）元函数符；$ {t}_{\mathrm{u}1} $ ,$ {t}_{\mathrm{u}2} $ ,…,${t}_{\mathrm{u}{{g}}}$ 是项. 一阶逻辑原子（atom）形如${p}_{\mathrm{r}\mathrm{e}\mathrm{d}}\left({t}_{\mathrm{r}1},{t}_{\mathrm{r}2},\cdots ,{t}_{\mathrm{r}{{o}}}\right)$ ，其中：$ {p}_{\mathrm{r}\mathrm{e}\mathrm{d}}({\text{•}})\in \mathcal{P} $ ，是$ o $ （$ o\geqslant 0 $ ）元谓词符；$ {t}_{\mathrm{r}1} $ ，$ {t}_{\mathrm{r}2} $ ，…，$ {t}_{\mathrm{r}{\rm{o}}} $ 是项. 一阶逻辑公式是由一阶逻辑联结词$\mathcal{C}= \{ ～ ,\wedge ,\vee ,\to , \leftrightarrow \}$ 、量词$ {Q}=\{\forall ,\exists \} $ 和原子联结而成. 其中：$～$ 表示否定；$ \wedge $ 表示且；$ \vee $ 表示或；$ \to $ 表示蕴含；$\leftrightarrow$ 表示等价；$ \forall $ 表示全称量词；$ \exists $ 表示存在量词.在自动定理证明中，问题的前提和结论均被形式化为一阶逻辑公式. 因此，符号是前提和结论最直观的特征. 若要为大理论问题的结论选择最相关的前提，最自然的方法是使用基于符号的前提选择方法.
2. 前提选择方法
基于符号相关性的前提选择方法意味着需要根据出现在前提中符号计算前提与当前结论证明的相关性，并据对应的相关度对前提进行选择.
2.1 基本思想
令c和P分别为一个大理论问题中的结论和前提集，基于符号相关性的前提选择方法的基本框架为：
1） 若符号s出现在c中，则s与c是1度相关的；
2） 若前提
$ p\in P $ 中的符号（或符号集）与c是k度相关的，则p是$ k + 1 $ 度相关的；3） 若p与c是k度相关的，则p中的所有符号与c是k度相关的.
在此过程中，首先需要定义两个相关集，即相关前提集
$ {R}_{\mathrm{p}} $ 和相关符号集$ {R}_{\mathrm{s}} $ .$ {R}_{\mathrm{p}} $ 包含结论及与结论证明相关的前提.$ {R}_{\mathrm{s}} $ 包含$ {R}_{\mathrm{p}} $ 中所有公式的所有符号，即Rs=⋃func∈RpF(func), (1) 式中：
$ {f}_{\mathrm{u}\mathrm{n}\mathrm{c}} $ 为结论c或与结论证明相关的任意前提p；$ F\left({f}_{\mathrm{u}\mathrm{n}\mathrm{c}}\right) $ 为$ {f}_{\mathrm{u}\mathrm{n}\mathrm{c}} $ 中所有符号组成的集合.开始时，
$ {R}_{\mathrm{p}} $ 仅包含结论c，$ {R}_{\mathrm{s}} $ 仅包含c中所有的符号. 即初始时，$ {R}_{\mathrm{p}}=\left\{c\right\} $ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ . 前提选择方法基于每个前提p的符号集$ F\left(p\right) $ 和当前$ {R}_{\mathrm{s}} $ , 计算p与c的相关度，不断地选择新的p加入$ {R}_{\mathrm{p}} $ 中，同时更新$ {R}_{\mathrm{s}} $ ，直到无法再将任何前提加入$ {R}_{\mathrm{p}} $ 中. 在完成前提选择后，由相关前提集$ {R}_{\mathrm{p}} $ 中的所有前提和结论组成的缩减问题将作为自动定理证明器新的输入，用于自动地证明问题的结论. 现有基于符号相关性的前提选择方法的通用流程如算法1所示.算法1 现有的基于符号相关性的前提选择方法
输入：结论c、前提P、相关前提集
$ {R}_{\mathrm{p}} $ 、相关符号集
$ {R}_{\mathrm{s}} $ 、无关前提集$ {I}_{\mathrm{p}} $ 、选择前提集SP、相关度阈值h、循环标记
$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}} $ 输出：
$ {R}_{\mathrm{p}} $ ${R}_{\mathrm{p}}=c$ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ ，$ {I}_{\mathrm{p}}=P $ ，$ {S}_{\mathrm{p}}=\varnothing $ ，${F}_{\mathrm{l}\mathrm{a}\mathrm{g}}=\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}$ while
$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}} $ dofor
$ p\in {I}_{\mathrm{p}} $ do根据当前的
$ {R}_{\mathrm{s}} $ ，计算$ p $ 的相关度if
$ p $ 的相关度$ \geqslant h $ then$ {S}_{\mathrm{p}}:={S}_{\mathrm{p}}\cup \left\{p\right\} $ end if
end for
if
$ {S}_{\mathrm{p}}=\varnothing $ then$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}}=\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e} $ else
${R}_{\mathrm{p}}:={R}_{\mathrm{p}}\cup {S}_{\mathrm{p}}$ ，${R}_{\mathrm{s}}:=({\bigcup }_{p\in {S}_{\mathrm{p}}}F(p))\cup {R}_{\mathrm{s}}$ ，${I}_{\mathrm{p}}:={I}_{\mathrm{p}}|{S}_{\mathrm{p}}$ $ {S}_{\mathrm{p}}=\varnothing $ end if
end while
完整的前提选择方法必须包含两个部分：前提选择和结论证明. 给定一个大理论，前提选择方法首先需要对大理论中的前提进行选择，随后利用自动定理证明器在选定的前提集上对问题的结论进行自动推理. 现有基于符号相关性的前提选择方法均将这两个部分分离开来，即，必须在结束前提选择过程之后，再利用自动定理证明器证明缩减后的问题. 尽管通过调整和添加实验参数对选择前提的数量进行限制，现有方法最后选择的前提仍有大量是与结论证明无关的.
2.2 基于符号权重的前提选择方法
由算法1可知，如何计算前提和相关符号集相关度是基于符号相关性的前提选择方法的重点. 简单地，可通过前提中的符号是否出现在相关符号集中，从而确定前提的相关性. 如果前提至少包含相关符号集中的一个符号，则可认为该前提是相关的. 在此情况下，若前提包含相关符号集中的一个符号，则该前提中的所有符号都会变为相关符号（加入相关符号集中）. 这种做法的弊端在于，几次迭代后，问题中几乎所有的前提都将被选择加入相关前提集中. 其中，最主要的原因是大理论问题中某些符号（通常被称为通用符号）频繁地出现在不同的前提中. 若通用符号被标记为相关符号，则所有包含此类符号的前提都将被认为是与结论证明相关的. 因此，前提的选择方法的重心应该放在解决通用符号的问题上.
与通过符号对应的是稀有符号，即在问题中出现的频率较低，基于此类符号的选择方法能够避免选择过多的前提. 因此，符号的权重定义应该遵循两个原则：削弱通用符号造成的负面影响，以及体现稀有符号的重要性. 给定一个前提集
$ P $ ，任意符号$s\in \bigcup\limits_{p \in P}F\left(p\right)$ 的权重$ w\left(s\right) $ 定义为w(s)=1−occ(s)|P|+1， (2) 式中：
$ {o}_{\mathrm{c}\mathrm{c}}\left(s\right) $ 为包含符号s的所有前提数量；$ \left|P\right| $ 为P中的前提总数.显而易见，对任意符号
$ s $ ，$ 0 < w\left(s\right) < 1 $ .$ w\left(s\right) $ 满足符号权重定义的两个原则. 若符号s是通用符号，则s的权重就越小；若符号s是稀有符号，则s的权重就越大. 式（2）定义的符号权重均在区间$ \left(\mathrm{0,1}\right) $ ，这能够保证基于该符号权重的相关度更加稳定.给定相关符号集
$ {R}_{\mathrm{s}} $ ，前提$ p $ 在$ {R}_{\mathrm{s}} $ 下与结论证明的相关度为r(p)=∑si∈Rs∩F(p)w(si)∑sj∈F(p)w(sj), (3) 式中：
$ {s}_{\mathrm{i}} $ 为$ {R}_{\mathrm{s}} $ 与$ F\left(p\right) $ 的交集中的任意符号；$ {s}_{\mathrm{j}} $ 为$ F\left(p\right) $ 中的任意符号.前提p与结论证明的相关度
$ r\left(p\right) $ 是在区间$ \left[\mathrm{0,1}\right] $ 内的实数. 如果p中的符号均不在相关符号集$ {R}_{\mathrm{s}} $ 中，则p与结论证明的相关度为0. 这说明p与当前的相关前提集$ {R}_{\mathrm{p}} $ 毫无符号上的关联. 如果p中的符号均在$ {R}_{\mathrm{s}} $ 中，则p与结论证明的相关度为1. 这说明p与当前的相关前提集$ {R}_{\mathrm{p}} $ 在符号上非常相关. 值得注意的是，随着相关前提集$ {R}_{\mathrm{p}} $ 和相关符号集$ {R}_{\mathrm{s}} $ 的变化，前提p的相关度也会发生变化.由式（3）可知，每个前提都存在一个基于当前相关符号集的相关度. 给定任意两个前提，通过比较其与结论证明的相关度大小，可以形式化两个前提间“更相关”的关系. 根据相关度的高低能够将对应的前提进行排序，但不能直接形式化“最相关前提”这一概念. 最相关前提的相关度大于最不相关前提的相关度, 因此，最直观的做法是设定一个相关度边界，用于区分最相关前提和最不相关前提.
定义1 给定一个相关度边界h（
$0\leqslant h\leqslant 1$ ），前提p被标记为最相关前提, 当且仅当$r\left(p\right)\leqslant h$ .由定义1可知，如果将h设置为0，所有的前提均为最相关前提. 如果将h设置为1，仅有非常少（甚至为0）的前提被标记为最相关的. 显然，相关度边界值过大或过小都会直接影响选择的结果，甚至问题结论的证明. 通过人工设置的相关度边界不具有普遍性和广泛适用性.
为解决以上问题，本文提出了一种自适应相关度边界. 该边界仅由当前选择过程中前提的相关度而决定，从而不再需要提前进行人工设置.
假定问题中包含n个前提
$ {p}_{1} $ ,$ {p}_{2} $ ,…,${p}_{{{{{n}}}}}$ ，$n \in {{{\bf{N}}}}, n \geqslant 1$ ，其对应的相关度分别为$ r\left({p}_{1}\right) $ ,$ r\left({p}_{2}\right) $ ,…,$ r\left({p}_{{n}}\right) $ . 在n个相关度中，部分相关度的值相同. 因此，合并相同的相关度值，能够从$ r\left({p}_{1}\right) $ ,$ r\left({p}_{2}\right) $ ,…,$ r\left({p}_{{n}}\right) $ 中获取M个不同的数值,$M \in {\bf{N}},1 \leqslant M \leqslant n$ . 这里将M个数值从高到低进行排序，序号为m的数值即为第m级自适应相关度边界$ {h}_{m} $ ，$m \in {\bf{N}},1 \leqslant m \leqslant M$ .显然，自适应相关度边界因问题而异，且会随着选择过程的变化而变化. 在选择过程中，所有相关度小于
$ {h}_{m} $ 的前提均不会被选择.前提选择方法的主旨在于选择尽可能少但充分与问题结论证明相关的前提. 一种可能的方法是选择一级自适应相关度边界
$ {h}_{1} $ 作为选择前提的条件. 实验发现，在大部分情况下，$ {h}_{1}=1 $ . 由式（3）可知，若一个前提的相关度为1，则该前提的所有符号均在相关符号集中. 若在相关前提集中加入相关度为1的前提，并不会使对应的相关符号集$ {R}_{s} $ 发生任何变化（加入新的符号）. 因此，仅选择相关度为1的前提作为最相关前提，会导致选择的前提不够充分. 因此，本文进一步细化地定义了自适应相关度边界$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ .定义2 给定一个前提集和前提对应的相关度，
1） 若第1级自适应相关度边界
$ {h}_{1}=1 $ ，则自适应相关度边界为第2级自适应相关度边界，即$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}={h}_{2} $ ；2） 此外，自适应相关度边界为第1级自适应相关度边界，即
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}={h}_{1} $ .由定义2可知，利用自适应相关度边界
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ ，新提出的基于符号权重的前提选择方法不再依赖任何人工设置的相关度边界.给定一个前提集
$ P $ ，现在可以根据前提$ p\in P $ 的相关度和自适应相关度边界，从$ P $ 中选择最相关前提. 然而，当前仍无法直观地判断所选择的前提对问题的结论证明是否足够充分. 因此，本文将前提选择过程和ATP的证明过程进行交互地结合. 在新的框架下，每一次选择的结果均将作为ATP的输入，开始尝试证明问题的结论. 若结论能够被自动地证明，则说明当前选择的前提是充分的，且整个过程可以停止.新提出的基于符号权重的前提选择算法流程如算法2所示. 最初的相关前提集仅包含问题的结论，对应的相关符号集仅包含结论中的符号，且无关前提集为问题的整个前提集. 在每次选择结束后，当前相关前提集中的前提和结论组成了新的缩减问题，ATP开始尝试在给定的CPU （central processing unit）运行时间内对该缩减问题进行证明. 若ATP能够证明该问题的结论，则不需要再继续选择前提，整个选择和证明过程立即停止. 否则，开始基于当前的相关符号集计算前提的相关度，并依据相关度边界, 将符合条件的前提标记为选择前提. 在旋转过程中，若没有满足条件的前提，则整个过程立即停止；否则, 利用当前新选择的前提更新相关前提集和相对应的关符号集，并从无关前提集中移除新选择的前提. 因此，整个过程将在K次循环后停止，
$k \in {\bf{N}}, k \geqslant 1$ .算法2 基于符号权重的前提选择算法
输入： 结论c、前提P、相关前提集
$ {R}_{\mathrm{p}} $ 、相关符 号集$ {R}_{\mathrm{s}} $ 、无关前提集IP、选择前提集SP、 相关度集R、自动定理证明器${{A}}_{\mathrm{T}\mathrm{P}}$ 、迭代 次数K、 CPU运行时间T输出：
$ {R}_{\mathrm{p}} $ $ {R}_{\mathrm{p}}=c $ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ ，$ {I}_{\mathrm{p}}=P $ ，$ {S}_{\mathrm{p}}=\varnothing，R=\varnothing $ for
$ k\in [\mathrm{1,2},\dots ,K] $ do利用
$ {{A}}_{\mathrm{T}\mathrm{P}} $ 尝试在时间T内证明由$ {R}_{\mathrm{p}} $ 中的前提（和结论）组成的缩减问题
if 问题被
${{A}}_{\mathrm{T}\mathrm{P}}$ 证明 then停止
else
for
$ p\in {I}_{\mathrm{p}} $ do根据当前的
$ {R}_{\mathrm{s}} $ ，计算$ p $ 的相关度$ r\left(p\right) $ $ R:=R\cup \left\{r\left(p\right)\right\} $ end for
根据R决定自适应相关度
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ for
$ p\in {I}_{\mathrm{p}} $ doif
$r\left(p\right)\geqslant {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}$ then$ {S}_{\mathrm{p}}:={S}_{\mathrm{p}}\cup \left\{p\right\} $ end if
end for
if
$ {S}_{\mathrm{p}}=\varnothing $ then停止
else
$ {R}_{\mathrm{p}}:={R}_{\mathrm{p}}\cup {S}_{\mathrm{p}} $ ，${R}_{\mathrm{s}}:=(\bigcup\limits_{p \in {S_{\rm{p}}}} {F(p)} )\cup {R}_{\mathrm{s}}$ ，$ {I}_{\mathrm{p}}:={I}_{\mathrm{p}}|{S}_{\mathrm{p}} $ $ {S}_{\mathrm{p}}=\varnothing $ ，$ R=\varnothing $ end if
end if
end for
3. 实验和分析
本节使用MPTP2078问题库作为实验的基准测试集. MPTP2078问题库一共包含2078个问题，均来自Mizar问题库与Bolzano-Weierstrass定理相关的问题. 问题库中, 所有问题的前提和结论均被形式化为一阶逻辑公式，且公式按照其在Mizar数学库中出现的顺序线性排序. 即出现在每一个结论之前的公式（前提和其他结论）均可作为证明该结论的前提. 问题的前提数量在区间
$ \left[\mathrm{10,4\;563}\right] $ 内，且前提的平均数量为1876个. 有关问题库前提数量和符号的具体分析见表1.表 1 MPTP2078问题库描述Table 1. Description of MPTP2078 benchmark个 项目 公式 结论 最小前提 最大前提 平均前提 符号 数量 4564 2078 10 4563 1876 784 在本文的实验中，使用的操作系统为CentOS Linux 7.4.1708；CPU为octa-core Intel（R） Xeon（R） E5-2667 3.20 GHz；内存128 G. 使用自动定理证明器E作为实验默认ATP. 除证明结论的数量外，还使用选择精准度
${S} _{\mathrm{p}\mathrm{r}\mathrm{e}}$ （selected precision）和选择度${S} _{\mathrm{e}\mathrm{l}}$ （selectivity）[29]作为评估各种选择方法性能的指标, 如式（4）、（5）所示.${S} _{\mathrm{p}\mathrm{r}\mathrm{e}}$ 的值越高越好，而${S} _{\mathrm{e}\mathrm{l}}$ 的值越低越好.Spre=1|Proved|∑prob∈ProvedNUiP(prob)NSel(prob)， (4) Sel=1|Proved|∑prob∈ProvedNSel(prob)NAxP(prob)， (5) 式中：
$ {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ 为被证明的问题集；$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\in {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ ，是$ {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ 中的一个被证明的问题；$ {N}_{\mathrm{U}\mathrm{i}\mathrm{P}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right) $ 为出现在$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}} $ 证明中的有用前提的数量；${N}_{{\rm{S}}\mathrm{e}\mathrm{l}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right)$ 为选择的前提的数量；$ {N}_{\mathrm{A}\mathrm{x}\mathrm{P}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right) $ 为$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}} $ 包含的原始前提的数量.表2列出了实验所涉及的基于符号的前提选择方法. 为了保证实验的公平性，本文将每个问题在自动定理证明器E上运行的CPU时间设定为60 s. 若一个问题的选择过程迭代K次，则每次迭代后生成的缩减问题仅在自动定理证明器E上运行
$ 60/K $ s. 显然地，需要权衡每次自动定理证明器运行的CPU时间和选择的迭代次数.表 2 参与实验的基于符号的前提选择方法的说明Table 2. Description of symbol-based premise selection methods in experiments提出的SymbolWeight能够根据前提的相当度自动地决定合适的相关度边界. 因此，SymbolWeight的性能仅与选择的迭代次数K有关. 表3评估了其在不同迭代次数K下对自动定理证明器E的性能影响. 由于每个问题运行CPU的时间最多为60 s，继续增加迭代次数会使得每次迭代中证明问题的CPU时间过小. 因此，SymbolWeight在实验中的最大迭代次数设置为30次. 随着K的不断增加，证明问题的数量在不断增加. 当
$ K= 30 $ 时，自动定理证明器E能够证明1077个问题. 值得注意的是，增加迭代次数并不会限制SymbolWeight的选择能力. 实验发现，SymbolWeight能够大大地减少选择前提的数量. 即使当K增加到30时，SymbolWeight平均选择前提数仅约为174个. 这表明，提出的自适应相关度边界在不损害自动定理证明器E证明能力的前提下，能够有效解决相关度边界的阈值设定问题. 随着K的增加，自动定理证明器CPU时间在逐渐减少（${{K}}=30$ 时，CPU时间仅为2 s）. 然而，证明问题的数量在不断增加. 这说明如果能够正确地选择出证明大理论问题结论所需要的全部前提，自动定理证明器E能够轻易地搜索到结论的证明. 因此，有效的前提选择方法能够大大地帮助证明器提高证明问题的能力.表 3 自动定理证明器E在SymbolWeight下的证明性能Table 3. Performance of automated theorem prover E with SymbolWeight$ K $ 证明数
量/个平均选择前提数量/个 选择精
确度选择度 2 288 13.0 0.358 0.054 4 599 22.6 0.336 0.060 6 818 33.3 0.322 0.054 8 862 44.5 0.309 0.053 10 920 55.9 0.302 0.055 12 932 68.4 0.295 0.057 14 967 81.1 0.288 0.059 16 980 94.0 0.285 0.060 18 1003 106.3 0.280 0.061 20 1014 117.3 0.278 0.061 22 1028 128.7 0.275 0.064 24 1045 140.7 0.271 0.068 26 1057 151.5 0.268 0.070 28 1071 162.4 0.265 0.074 30 1077 174.2 0.264 0.076 表4比较了自动定理证明器E在不同基于符号的前提选择方法下的证明性能. E-SInE和Vampire-SInE分别表示在证明器E和Vampire中的SInE[19]方法. 自动定理证明器E在使用SymbolWeight作为前提选择方法时能够证明MPTP2078问题库中超过半数的问题. 与E-SInE和Vampire-SInE相比，SymbolWeight能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.
表 4 自动定理证明器E在不同的基于符号的前提选择方法下的证明性能Table 4. Performance of automated theorem prover E with different symbol-based premise selection methods前提选择方法 证明数量/个 证明率/% no-selection 663 30.90 E-SInE 672 32.34 Vampire-SInE 859 41.34 SymbolWeight 1077 51.83 4. 结 论
1） 提出了新的符号权重和相关度计算方法，并基于此设计并实现了用于解决大理论问题的前提选择的方法；
2） 提出了自适应相关度边界，解决了在基于符号的前提选择方法中需要人工地设置相关度边界的问题；
3） 新提出的前提选择方法能够大大地提高自动定理证明器E在MPTP2078问题库上的证明能力.
-
表 1 MPTP2078问题库描述
Table 1. Description of MPTP2078 benchmark
个 项目 公式 结论 最小前提 最大前提 平均前提 符号 数量 4564 2078 10 4563 1876 784 
下载: 导出CSV
表 2 参与实验的基于符号的前提选择方法的说明
Table 2. Description of symbol-based premise selection methods in experiments
下载: 导出CSV
表 3 自动定理证明器E在SymbolWeight下的证明性能
Table 3. Performance of automated theorem prover E with SymbolWeight
$ K $ 证明数
量/个平均选择前提数量/个 选择精
确度选择度 2 288 13.0 0.358 0.054 4 599 22.6 0.336 0.060 6 818 33.3 0.322 0.054 8 862 44.5 0.309 0.053 10 920 55.9 0.302 0.055 12 932 68.4 0.295 0.057 14 967 81.1 0.288 0.059 16 980 94.0 0.285 0.060 18 1003 106.3 0.280 0.061 20 1014 117.3 0.278 0.061 22 1028 128.7 0.275 0.064 24 1045 140.7 0.271 0.068 26 1057 151.5 0.268 0.070 28 1071 162.4 0.265 0.074 30 1077 174.2 0.264 0.076
下载: 导出CSV
表 4 自动定理证明器E在不同的基于符号的前提选择方法下的证明性能
Table 4. Performance of automated theorem prover E with different symbol-based premise selection methods
前提选择方法 证明数量/个 证明率/% no-selection 663 30.90 E-SInE 672 32.34 Vampire-SInE 859 41.34 SymbolWeight 1077 51.83
下载: 导出CSV
-
[1] DARWICHE A. Compiling knowledge into decomposable negation normal form[C]//Proceedings of the Sixteenth International Joint Conference on Artifical Intelligence. New York: ACM, 1999: 284-289. [2] KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems, 1999, 4(2): 123-193. doi: 10.1145/307988.307989 [3] JACKSON D, SCHECHTER I, SHLYAHTER H. Alcoa: the alloy constraint analyzer[C]//Proceedings of the 22nd International Conference on Software Engineering. New York: ACM, 2000: 730-733. [4] LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115. [5] KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM, 2009: 207-220 [6] KAUTZ H, SELMAN B. Planning as satisfiability[C]// Proceedings of the 10th European Conference on Artificial Intelligence. New York: ACM, 1992: 359-363. [7] RINTANEN J, HELJANKO K, NIEMELÄ I. Planning as satisfiability: parallel plans and algorithms for plan search[J]. Artificial Intelligence, 2006, 170(12/13): 1031-1080. [8] LARRABEE T. Test pattern generation using boolean satisfiability[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992, 11(1): 4-15. doi: 10.1109/43.108614 [9] WOOD R G, RUTENBAR R A. FPGA routing and routability estimation via Boolean satisfiability[J]. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 1998, 6(2): 222-231. doi: 10.1109/92.678873 [10] EGGERSGLUSS S, DRECHSLER R. Efficient data structures and methodologies for SAT-based ATPG providing high fault coverage in industrial application[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2011, 30(9): 1411-1415. doi: 10.1109/TCAD.2011.2152450 [11] CLARKE E, KROENING D, LERDA F. A tool for checking ANSI-C programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springe, 2004: 168-176. [12] LENAT D. CYC: a large-scale investment in knowledge infrastructure[J]. Communications of the ACM, 1998, 38(11): 33-38. [13] NILES I, PEASE A. Towards a standard upper ontology[C]//Proceedings of the international conference on Formal Ontology in Information Systems. New York: ACM, 2001: 2-9. [14] KALISZYK C, URBAN J. MizAR 40 for mizar 40[J]. Journal of Automated Reasoning, 2015, 55(3): 245-256. doi: 10.1007/s10817-015-9330-8 [15] SUTCLIFFE G, PUZIS Y. SRASS-A semantic relevance axiom selection system[C]//International Conference on Automated Deduction. Berlin: Springer, 2007: 295-310. [16] PUDLÁK P. Semantic selection of premisses for automated theorem proving[C]//Cade-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. Bremen: [s.n.], 2007: 1-18. [17] ROEDERER A, PUZIS Y, SUTCLIFFE G. Divvy: an ATP meta-system based on axiom relevance ordering[C]//International Conference on Automated Deduction. Berlin: Springer, 2009: 157-162. [18] MENG J, PAULSON L C. Lightweight relevance filtering for machine-generated resolution problems[J]. Journal of Applied Logic, 2009, 7(1): 41-57. doi: 10.1016/j.jal.2007.07.004 [19] HODER K, VORONKOV A. Sine Qua Non for large theory reasoning[C]//International Conference on Automated Deduction. Berlin: Springer, 2011: 299-314. [20] ALAMA J, HESKES T, KÜHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52(2): 191-213. doi: 10.1007/s10817-013-9286-5 [21] KALISZYK C, URBAN J, VYSKOCIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2015: 3084-3090. [22] PIOTROWSKI B, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[C]//International Joint Conference on Automated Reasoning. Cham: Springer, 2018: 566-574. [23] IRVING G, SZEGEDY C, ALEMI A A, et al. Deep-math−deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. New York: Curran Associates Inc. , 2016: 2243-2251. [24] WANG M Z, TANG Y H, WANG J, et al. Premise selection for theorem proving by deep graph embedding[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. New York: ACM, 2017: 2787-2797. [25] CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[C]// KDD’20 Deep Learning on Graphs Workshop. San Diego: [s.n.], 2019: 1-7. [26] LIU Q H, XU Y, HE X X. Attention recurrent cross-graph neural network for selecting premises[J]. International Journal of Machine Learning and Cybernetics, 2022, 13(5): 1301-1315. doi: 10.1007/s13042-021-01448-9 [27] 刘清华,徐扬,吴贯锋,李瑞杰. 基于边权重图神经网络的一阶逻辑前提选择[J]. 西南交通大学学报,2022,57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134LIU Q H, XU Y, WU G F, et al. Edge-eighted-based graph neural network for first-order premise selection[J]. Journal of Southwest Jiaotong University, 2022, 57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134 [28] HARRISON J. Handbook of practical logic and automated reasoning[M]. Cambridge: Cambridge University Press, 2009. [29] LIU Q H, WU Z S, WANG Z H, et al. Evaluation of axiom selection techniques[C]// 10th International Joint Conference on Automated Reasoning. Paris: CEUR-WS, 2020: 63-75. -
下载:
下载: 
点击查看大图
计量
- 文章访问数: 341
- HTML全文浏览量: 110
- PDF下载量: 38
- 被引次数: 0