Influence Analysis of Vibration Control Parameters for High-Speed Maglev Train-Bridge Coupling
-
摘要:
磁浮列车悬浮系统控制参数取值不当可能导致车-桥系统异常振动. 因此，明确悬浮系统控制参数与磁浮车-桥系统动力响应之间的关系十分重要. 首先，建立包含比例-微分控制的5节编组磁浮列车动力学模型和20跨简支梁桥有限元模型；其次，与实测结果进行对比验证所建立模型的正确性；最后，计算车速430 km/h时不同控制参数下列车和桥梁的动力响应. 结果表明：增大比例系数会使悬浮和导向系统刚度增大，增大微分系数会使悬浮和导向系统阻尼增大；车体竖向加速度随比例和微分系数的增大而增大，车体横向加速度随比例系数的增大而增大；悬浮间隙和桥梁竖向加速度均随比例系数的增大而减小，随微分系数的增大而增大；导向间隙随微分系数的增大而减小，比例系数对导向间隙的影响较小；桥梁横向加速度随比例系数的增大而减小，随微分系数的增大而增大；桥梁竖向加速度主要受电磁力中悬浮电磁铁长度特征频率1倍～12倍频的影响，桥梁横向加速度主要受导向磁极长度特征频率及其2倍频和导向电磁铁长度特征频率2倍频及4倍频的影响；为减小车-桥系统动力响应，综合建议竖向比例和微分系数的取值范围分别为3000～4000和10～25，横向比例和微分系数的取值范围分别为4000～5000和10～25.
Abstract:Improper control parameters of the suspension system of maglev trains may lead to abnormal vibration of the train-bridge system. Therefore, it is important to clarify the relationship between the control parameters of the suspension system and the dynamic response of the maglev train-bridge system. Firstly, the dynamic model of a 5-car maglev train with proportional-differential control, as well as the finite element model of a 20-span simply supported beam bridge was established. Secondly, the correctness of the models was verified by comparing them with the measured results. Finally, the dynamic responses of the train and bridge under different control parameters at 430 km/h were calculated. The results show that increasing the proportional coefficient will increase the stiffness of the suspension and guidance system, and increasing the differential coefficient will increase the damping of the suspension and guidance system. The vertical acceleration of the car body increases with the increase in the proportional and differential coefficients, and the lateral acceleration of the car body increases with the increase in the proportional coefficient. The suspension gap and the vertical acceleration of the bridge decrease with the increase in the proportional coefficient, and they increase with the increase in the differential coefficient. The guidance gap decreases with the increase in the differential coefficient, and the proportional coefficient has little effect on the guidance gap. The lateral acceleration of the bridge decreases with the increase in the proportional coefficient and increases with the increase in the differential coefficient. The vertical acceleration of the bridge is mainly affected by a characteristic frequency of 1–12 times of the length of the suspended electromagnet in the electromagnetic force, and the lateral acceleration of the bridge is mainly affected by the characteristic frequency and frequency of 2 times of the length of the guidance pole, as well as the characteristic frequency of 2 times and 4 times of the length of the guidance electromagnet. In order to reduce the dynamic response of the train-bridge system, it is suggested that the values of vertical proportional and differential coefficients should be 3 000–4 000 and 10–25, respectively, and the values of lateral proportional and differential coefficients should be 4 000–5 000 and 10–25, respectively.
-
自动推理作为计算机科学和数理逻辑的交叉学科，是人工智能的核心分支. 一阶逻辑（first-order logic，FOL）自动定理证明最初仅为了自动地证明数学定理，而目前已广泛地应用于其他领域，例如电路设计、软件验证、硬件验证和管理等[1-3]. 先进的一阶逻辑自动定理证明器（automated theorem prover，ATP），如Vampire[4]和E[5]，擅长在TPTP （thousands of problems for theorem provers）[6]的某些限定领域中证明问题，但却很难高效地证明大型问题库中的问题（如，MizAR数学库[7]）. 这些大规模的问题被称为大理论问题，其通常包含成千上万个前提，但只有极少部分的前提能对问题结论的证明起到有效作用.
在FOL中，问题的前提和结论被形式化为一阶逻辑公式. 大多数ATP主要基于Given Clause算法[8]对从公式转换而来的子句（合取范式）进行证明搜索. 证明搜索是在两个集合上执行：未处理子句集和已处理子句集. 在证明搜索开始前，所有输入子句都是未处理的. Given Clause算法反复地从未处理子句集中选择一个子句作为给定子句，并将所有可能的推理规则应用于该子句和已处理子句集中的其他子句； 最后，新选择的给定子句被放入已处理子句集中，新生成的子句被置于未处理子句中. 此证明搜索过程将一直持续直到超出计算资源限制，或推断出空子句或已处理子句集变得饱和（无法推断出任何新子句）.
传统ATP在证明大理论时，由于问题包含了数量极多的前提，在上述证明搜索的过程中，搜索空间会呈爆炸型增长. 因此，计算机资源会很快地被耗尽，进而导致ATP证明问题的性能大幅降低. 该问题导致了ATP无法在证明大理论问题时充分发挥作用. 解决该问题的一种有效方法是在ATP试图找到结论的证明之前，尽可能地选择出最可能参与证明构造的前提. 该过程被称为前提选择，通常作为ATP预处理的一部分，其对解决大规模问题至关重要.
起初，前提选择通常采用基于公式中符号的启发式方法[9-10]，主要通过计算和比较公式中的符号，对公式的相关性进行分析. 最近，结合传统机器学习技术[11-13]的前提选择模型展现了具有竞争力的结果，但基于传统机器学习的前提选择在编码逻辑公式时强烈地依赖于手工设计的特征（如，符号和子项等）. 因为深度学习方法，如长短期记忆神经网络（long-short term memory，LSTM）[14]和图神经网络（graph neural network，GNN）[15-17]，在编码逻辑公式时不需要依赖于任何人工设计的特征，得到了越来越多学者的关注. 又因为逻辑公式可以自然而然地表示为能够保留公式句法和语义信息的有向无环图（directed acyclic graph，DAG），所以定理证明与GNN的结合是当前最热门的研究主题之一.
目前，主流的图神经网络框架通常通过聚集邻接节点的信息来更新目标节点的特征表示. 在此框架下的图神经网络模型常用于处理无向图，如图卷积神经网络（graph convolutional network，GCN）[18]、图注意力神经网络（graph attention network，GAT）[19]等. 然而，公式图是有向，当前的图神经网络模型只能单向地沿着公式图的边进行信息传播. 除此之外，逻辑图中相应的子节点之间是有顺序的，而目前的图神经网络模型的信息聚集操作通常与子节点的顺序无关. 为发挥逻辑公式图表示的优势，理想的方法是根据公式的特性对公式图中的节点进行排序并双向地传递邻接节点的信息.
针对上述问题，提出一种带有边类型的双向图用于表示一阶逻辑公式. 图中相邻的两个节点由不同方向的两条边连接且每条边都有一种对应的边类型. 通过确定每条边特定的边类型，可以对双向图中的节点进行排序. 基于新的公式图表示，提出了一种基于边权重的图神经网络模型，即EW-GNN （edge-weight-based graph neural network）. 对图中的每一个方向，EW-GNN首先利用节点的信息更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重. 传递给中心节点的信息是邻接节点信息的加权和. EW-GNN最后汇聚中心节点来自两个方向上的信息，并对节点进行更新. 实验比较分析表明：当前主流模型在测试集上的分类准确率两两之差均小于1%，而提出的EW-GNN在相同的测试集上比表现最优的模型还能提高约1%的分类准确率. 因此，EW-GNN能够在前提选择任务中表现得更加优越.
1. 一阶逻辑公式图表示
1.1 一阶逻辑公式
在一阶逻辑中[20]，给定一个变量符号集
$ \mathcal{V} $ ，一个函数符号集$ \mathcal{F} $ ，以及一个谓词符号集$ \mathcal{P} $ . 一阶逻辑项（term）是一个变量项$ v\in \mathcal{V} $ 或者形如$ f \left({t}_{1}, \right. \left.{t}_{2},\cdots ,{t}_{n}\right) $ 的函数项，其中，$ f\in \mathcal{F} $ 为$n $ （$n\geqslant 0$ ）元函数符，$ {t}_{1} $ ，$ {t}_{2},\cdots , $ $ {t}_{n} $ 是项. 一阶逻辑原子（atom）形如$ P\left({t}_{1},{t}_{2},\cdots ,{t}_{n}\right) $ ，其中，$ P\in \mathcal{P} $ 为$ n $ （$n\geqslant 1$ ）元谓词符. 一阶逻辑公式是由一阶逻辑联结词$\mathcal{C}=\{ \sim ,{\wedge} ,{\vee} ,{\to} ,{\leftrightarrow} \}$ 、量词$ \mathcal{Q}=\{\forall ,\exists \} $ 和原子联结而成.1.2 图定义
带有边类型的双向图定义为
$ \;\;\;\;G=\left(V,E,{R}_{E}\right) $ ，其中：节点集$ V={\{v}_{1},{v}_{2},\cdots ,{v}_{n}\}$ 包含G中所有节点；边集$ E=\{ 〈 {v}_{i},{v}_{j} 〉 |{v}_{i},{v}_{j}\in V\} $ 包含G中所有边，有向对$ {e}_{ij}= 〈 {v}_{i},{v}_{j} 〉 $ 表示从节点vi到节点vj的有向边；边类型集${R}_{E}=\left\{{r}_{{e}_{ij}}|{e}_{ij}\in E \right\}$ 包含G中所有边对应的边类型. 节点vi的邻接节点集定义为$ \mathcal{N}\left({v}_{i}\right)=$ $\left\{{v}_{j}|{e}_{ji}\in E \right\}$ . 图中的每一个节点v都伴随着一个初始节点特征向量${\boldsymbol{x}}_{v}\in {\bf{R}}^{{d}_{v}}$ ，每一条边e也伴随着一个初始边特征向量${\boldsymbol{x}}_{e}\in {\bf{R}}^{{d}_{e}}$ ，表示其对应的边类型. dv和de分别为xv和xe的初始向量维度.1.3 表 示
一阶逻辑公式能够自然地表示为语义解析树（abstract semantic tree，AST）. 通过添加从量词节点指向到相应被约束的变量节点的边以及合并所有相同的子表达式对应的子树，可以将表示公式的AST扩展为含有根节点的DAG.
为了保持逻辑公式图中部分节点之间有序性以及双向传递邻接节点的信息，设计了双向图表示，其中图中相邻的两个节点由方向不同的两条边连接且每条边都具有一种对应的边类型.
逻辑公式图中的节点大致可分为5种类型：量词、逻辑联结词、谓词、函数和变量. 在定义边类型时，逻辑连接词节点、量词节点和特殊的相等谓词（=）节点的名称为其类型，而其他谓词、函数以及变量节点的类型为其对应的类型，分别记为pred、func和var.
然而，对逻辑公式图中的子节点进行排序仍是一个难题. 利用文献[16]中提出的排序方案，从上往下单向地定义节点顺序，即在给定相应父节点类型的情况下，对其子节点进行排序：
1） 如果父节点是逻辑联结词 ~、
$ \wedge $ 、$ \vee $ 、${\leftrightarrow}$ 或 =，则它们对应的子节点的顺序一样；2） 如果父节点是量词
$ \forall $ 或$ \exists $ ，则其变量子节点具有相同的顺序，而其他子节点是线性排序的；3） 如果父节点是其他谓词、逻辑连接词或函数，则其子节点是线性排序的.
正式地，一阶逻辑表达式s的双向图表示
$ {G}_{s}=\left({V}_{s},{E}_{s},{R}_{s}\right) $ 构造如下：1） 如果s是一个变量项或常量项（0元函数项），则
$ {V}_{s}=\left\{s\right\} $ ，$ {E}_{s}=\left\{\varnothing \right\} $ ；2） 如果
$s=f\left({s}_{1},{s}_{2},\cdots ,{s}_{n}\right)$ ，其中，$ f\in \mathcal{F}\cup \mathcal{P}\cup \mathcal{C} $ 且$ {s}_{1} $ ,$ {s}_{2} ,\cdots,$ $ {s}_{n} $ 为子表达式，则$ {V}_{s}\in {\bigcup }_{i=1}^{n}{V}_{{s}_{i}}\cup \left\{f\right\} $ ，$ {E}_{s}= {\bigcup }_{i=1}^{n}\left({E}_{{s}_{i}}\cup \{ 〈 f,{H(s}_{i}) 〉 \}\cup \{ 〈 {H(s}_{i}),f 〉 \}\right) $ ，其中，$ {H(s}_{i}) $ 为表达式si的最外层符号. 如果s包含相同的子表达式，则在Gs上合并（merge）相同的子图；3） 如果
$ s={\phi }\hat{s} $ ，其中，$ \phi \in \mathcal{Q} $ ，$ \hat{s} $ 是包含变量x的表达式，则$ {V}_{s}={V}_{\hat{s}}\cup \left\{\phi \right\} $ ，${E}_{s}={E}_{\hat{s}}\cup \{ 〈 \phi ，H\left(\hat{s}\right) 〉 \}\cup \{ 〈 H\left(\hat{s}\right)，\phi 〉 \}\cup \{ 〈 \phi ,x 〉 \}\cup \{ 〈 x,\phi 〉 \}$ . 随后，在Gs上合并所有由量词$ \phi $ 约束的变量x；4） 在递归构造完Gs后，用统一的标记 * 更替Gs中所有变量节点的名称；
5） Rs中的每一个边类型由对应连接的两个节点的类型和节点顺序决定.
图1为一阶逻辑公式
${\forall }x,y{(p(f(x),a) { \vee}} { q(a,f(y)))}$ 的双向图表示，其中：$ y({\text{•}}) $ 为变量；$p( {\text{•}})$ 和$ q({\text{•}}) $ 为谓词函数；$f({\text{•}})$ 和$ a $ 分别为一元函数和零元函数（常元）.
图 1 一阶逻辑公式的双向图表示Figure 1. Bidirectional graph representation of first-order logical formula在图1中，变量节点
$ x $ 和$ y $ 被替换成了统一的标记 *，替换后的双向图能在变量更名下保持一致. 两种不同颜色的边分别代表了图中两个不同的方向. 与单向图相比，双向图中的每个节点有来自两个方向上邻接节点，如$ \forall $ 、P和Q都是图中的节点$ \vee $ 的邻接节点. 通过给图中的边添加类型，可以在一定程度上对图中的相关节点进行排序. 如在节点$ \forall $ 下，变量节点x和y （即节点*）的顺序相同且记为1，因此节点$ \vee $ 的顺序自然地记为2. 连接节点$ \forall $ 和$ \vee $ 的两条边上的顺序均为$ \vee $ 在从上到下的单向图的中作为$ \forall $ 的子节点的顺序. 除此之外，边类型同样也反映出了边的方向. 边类型$ \forall $ _$ \vee $ _2和$ \vee $ _$ \forall $ _2分别表示从节点$ \forall $ 指向节点$ \vee $ 的边和从节点$ \vee $ 指向节点$ \forall $ 的边.2. 模 型
所有前提选择模型都具有相似的框架，即，对逻辑公式进行表示并计算公式间的相关性. 其正式定义如下：
定义1[11] 给定一个结论c和其前提集
$ A $ ，前提选择需要预测并选择$ A $ 中可能对证明c有用的前提.如图2所示，一个完整的端到端基于图神经网络的前提选择模型应包含以下3部分：公式图表示、图神经网络模型和二元分类器. 在本文中，首先，将一阶逻辑公式转化为带有边类型的双向图；其次，通过使用新提出的EW-GNN模型，将逻辑公式图编码为特征向量；最后，二元分类器将一个结论向量和一个候选前提向量的拼接作为输入，并输出一个
$ \left[\mathrm{0,1}\right] $ 之间的实数得分，该得分表明在证明结论中使用候选前提的概率.给定一个大理论问题和训练后的前提选择模型，可以将所有的{结论,前提}对反馈给前提选择模型，并输出每个前提对结论有用（无用）的概率. 根据输出的概率，可以对前提进行排序，并从排序中选择出前
$ {n}_{{\rm{p}}} $ 个前提作为给定结论的有用前提. 最后，ATP将使用$ {n}_{{\rm{p}}} $ 个选定的前提自动地证明对应的结论，从而解决ATP搜索空间爆炸增长的问题.2.1 基于边权重的图神经网络
EW-GNN模型包括4个阶段：初始化、消息聚合、消息传播（节点更新）以及图聚合.
在初始化阶段，模型通过不同的嵌入函数
$ {F}_{v} $ 和$ {F}_{e} $ 将任意初始节点特征向量$ {\boldsymbol{x}}_{v} $ 和初始边特征向量$ {\boldsymbol{x}}_{e} $ 分别映射为初始节点状态向量$ {\boldsymbol{h}}_{v}^{\left(0\right)} $ 和初始边状态向量$ {\boldsymbol{h}}_{e}^{\left(0\right)} $ ：h(0)v=Fv(xv), (1) h(0)e=Fe(xe), (2) 式中：
${\boldsymbol{h}}_{v}^{\left(0\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{v}}}$ ；${\boldsymbol{h}}_{e}^{\left(0\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{e}}}$ ；$ {d}_{{h}_{v}} $ 和$ {d}_{{h}_{e}} $ 分别为节点状态向量和边状态向量的维度.$ {F}_{v} $ 和$ {F}_{e} $ 在本文中被设计为不同的查找表，用于存储固定字典和大小的嵌入，并将用热独（one-hot）向量表示的$ {\boldsymbol{x}}_{v} $ 和$ {\boldsymbol{x}}_{e} $ 分别编码为固定大小的初始状态向量.在第
$ k $ （$k=\mathrm{1,2},\cdots ,K$ ）次信息聚集阶段，EW-GNN根据边的方向，分别聚集目标节点$ {v}_{i} $ 来自两个方向上的邻接节点$ {v}_{j} $ 的信息. 这里，简单地把边的方向分为从上往下和从下往上. 为计算$ {v}_{j} $ 对$ {v}_{i} $ 的权重，首先利用$ {v}_{j} $ 和$ {v}_{i} $ 第k − 1次状态向量$ {\boldsymbol{h}}_{{v}_{j}}^{\left(k-1\right)} $ 和$ {\boldsymbol{h}}_{{v}_{i}}^{\left(k-1\right)} $ ，以及第k − 1次边状态向量$ {\boldsymbol{h}}_{{e}_{ji}}^{\left(k-1\right)} $ 对第k次边状态向量$ {\boldsymbol{h}}_{{e}_{ji}}^{\left(k\right)} $ 进行更新：如果
$ {e}_{ji} $ 的方向是从上往下的，则h(k)eji=W(k)i([h(k−1)vj;h(k−1)eji;h(k−1)vi]), (3) 如果
$ {e}_{ji} $ 的方向是从下往上的，则h(k)eji=W(k)o([h(k−1)vj;h(k−1)eji;h(k−1)vi]), (4) 式中：
${\boldsymbol{W}}_{{\rm{i}}}^{\left(k\right)}、{\boldsymbol{W}}_{{\rm{o}}}^{\left(k\right)}$ 分别为第k次入边、出边的学习矩阵，$ {\boldsymbol{W}}_{{\rm{i}}}^{\left(k\right)},{\boldsymbol{W}}_{{\rm{o}}}^{\left(k\right)}\in {\bf{{{R}}}}^{{d}_{{h}_{e}}}{\times {\bf{{R}}}}^{2{d}_{{h}_{v}} + {d}_{{h}_{e}}}$ .利用更新后的边状态向量，领接节点
$ {v}_{j} $ 对中心节点$ {v}_{i} $ 的权重$ {a}_{ji}^{\left(k\right)} $ 的计算如下：如果
$ {e}_{ji} $ 的方向是从上往下的，则a(k)ji=σ(W(k)wi(h(k)eji)), (5) 如果
$ {e}_{ji} $ 的方向是从下往上的，则a(k)ji=σ(W(k)wo(h(k)eji)), (6) 式中：
${\boldsymbol{W}}_{{{\rm{wi}}}}^{\left(k\right)}、{\boldsymbol{W}}_{{{\rm{wo}}}}^{\left(k\right)}$ 分别为权重计算时第k次入边、出边的学习矩阵，$ {\boldsymbol{W}}_{{{\rm{wi}}}}^{\left(k\right)},{\boldsymbol{W}}_{{{\rm{wo}}}}^{\left(k\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{e}}}$ ；$ \sigma \left(x\right) = \dfrac{1}{1 + {{\rm{e}}}^{-x}} $ 为sigmoid激活函数.节点
$ {v}_{i} $ 来自邻接节点$ {v}_{j} $ 的聚合信息为m(k)vi=∑vj∈N(vi)a(k)jiF(k)m(h(k−1)vj), (7) 式中：
$ {F}_{m}^{\left(k\right)} $ 为第m层的全连接层.$ {e}_{ji} $ 的方向不同，$ {F}_{m}^{\left(k\right)} $ 也随之不同：如果
$ {e}_{ji} $ 的方向是从上往下的，则F(k)m(h(k−1)vj)=W(k)mih(k−1)vj+b(k)mi, (8) 如果
$ {e}_{ji} $ 的方向是从下往上的，则F(k)m(h(k−1)vj)=W(k)moh(k−1)vj+b(k)mo, (9) 式中：
${\boldsymbol{W}}_{{m{\rm{i}}}}^{\left(k\right)}、{\boldsymbol{W}}_{{m{\rm{o}}}}^{\left(k\right)}$ 和${\boldsymbol{b}}_{m{\rm{i}}}^{\left(k\right)}$ 、${\boldsymbol{b}}_{m{\rm{o}}}^{\left(k\right)}$ 分别为权重计算时第m层第k次入边、出边的学习矩阵和偏差向量，$ {\boldsymbol{W}}_{{m{\rm{i}}}}^{\left(k\right)},{\boldsymbol{W}}_{{m{\rm{o}}}}^{\left(k\right)}\in {\mathbf{R}}^{{d}_{{h}_{v}}}\times {\mathbf{R}}^{{d}_{{h}_{v}}}，{\boldsymbol{b}}_{m{\rm{i}}}^{\left(k\right)},{\boldsymbol{b}}_{m{\rm{o}}}^{\left(k\right)}\in {\mathbf{R}}^{{d}_{{h}_{v}}}$ .因此，节点
$ {v}_{i} $ 的状态向量的第$ k $ 次更新为h(k)vi=m(k)vi+h(k−1)vi. (10) 第K次迭代后，EW-GNN在图聚合阶段对图中所有节点状态向量进行池化，以生成最后的公式图向量：
hG=1|V|K∑k=1h(k)vi,vi∈V. (11) 这里，采用了平均池化对整个节点维度上的节点特征求平均值.
2.2 二元分类器
分类模型的输入是图向量对
$({\boldsymbol{h}}_{{\rm{conj}}},{\boldsymbol{h}}_{{\rm{prem}}})$ ，分别表示结论和候选的前提. EW-GNN通过分类函数${F}_{{\rm{class}}}$ 对前提在结论证明中的有用性进行预测：ˆz=Fclass([hconj;hprem]), (12) 式中：
$\hat{\textit{z}}\in {\bf{R}}^{2}$ 为候选前提在给定结论有用和无用类别的对应得分.${F}_{{\rm{class}}}$ 在本文中被设计为多层感知机（multi-layer perceptron，MLP）. 具体为Fclass(•)=W2(ReLU(W1(•)+b1))+b2, (13) 式中：
${\boldsymbol{W}}_{1}\in {{{\bf{R}}}}^{{d}_{{h}_{v}}}\times {{{\bf{R}}}}^{2{d}_{{h}_{v}}}$ 和${\boldsymbol{W}}_{2}\in {{{\bf{R}}}}^{2}\times {{{\bf{R}}}}^{{d}_{{h}_{v}}}$ 为不同的学习矩阵；${\boldsymbol{b}}_{1}\in {{{\bf{R}}}}^{{d}_{{h}_{v}}}$ 和${\boldsymbol{b}}_{1}\in {{{\bf{R}}}}^{2}$ 为学习偏差向量.$ \mathrm{R}\mathrm{e}\mathrm{L}\mathrm{U}({\text{•}}) $ 为修正线性单元（rectified linear unit，ReLU）函数：ReLU(x)={x,x>0,0,x⩽0. (14) 因此，前提在两个类别下的预测概率为
ˆy=softmax(ˆz), (15) 式中：
$ \mathrm{s}\mathrm{o}\mathrm{f}\mathrm{t}\mathrm{m}\mathrm{a}\mathrm{x} ({\text{•}})$ 为归一化函数.$\hat{\boldsymbol{y}}$ 中的每一元素$\hat{y}_{a}$ 在$ \mathrm{s}\mathrm{o}\mathrm{f}\mathrm{t}\mathrm{m}\mathrm{a}\mathrm{x} ({\text{•}})$ 函数中的计算为ˆya=eˆza∑beˆzb, (16) 式中：
${\hat{{\textit{z}}}_{a}} $ 、${\hat{{\textit{z}}}_{b}} $ 分别为${\hat{{\textit{z}}}} $ 中第a、b个元素.2.3 损失函数
在均衡数据集下，对于每一个{结论,前提}对，损失函数
$ \mathcal{L} $ 定义为预测值$ \hat{\boldsymbol{y}} $ 和真实值y之间的交叉熵：L(y,ˆy)=∑CyCln(ˆyC)+(1−yC)ln(1−ˆyC), (17) 式中：
$ \boldsymbol{y} $ 为真实值的一个独热编码；${y}_{C}$ 和${\hat{y}}_{C}$ 分别为真实值$ \boldsymbol{y} $ 和预测值$ \hat{\boldsymbol{y}} $ 在第$C$ 类别下的对应值.在非均衡数据集下，对于每一个{结论，前提}对，损失函数
$ \mathcal{L} $ 定义为预测值$ \hat{\boldsymbol{y}} $ 和真实值$ \boldsymbol{y} $ 之间的加权交叉熵：L(y,ˆy)=∑Cw+yCln(ˆyC)+w−(1−yC)ln(1−ˆyC), (18) 式中：
$ {w}_{ + } $ 、$ {w}_{-} $ 分别为正、负样本的权重，且$ {w}_{ + } > {w}_{-} $ .在本文的模型训练中，
$ {w}_{ + } $ 和$ {w}_{-} $ 分别设置为w+=NP+NNNP, (19) w−=NP+NNNN, (20) 式中：
$ N_{\rm{P}} $ 、$ N_{\rm{N}} $ 分别为数据集中正、负样本的数量.3. 数据集
本文基于MPTP2078问题库[11]建立了一个用于训练、验证和测试前提选择模型的数据集.
MPTP2078问题库中一共包含2 078个问题，均来自Mizar数学库（Mizar Mathematical Library，MML）[21]中与Bolzano-Weierstrass公理相关的问题. 问题库所有问题的前提和结论均被TPTP系统形式化为一阶逻辑公式，且公式按照它们在Mizar数学库中出现的顺序线性排序. 即，出现在每一个结论之前的公式（前提和其他结论）均可作为证明该结论的前提. 问题的前提数量在区间[10, 4563]中，且前提的平均数量为1 876. 表1具体地描述了问题库中结论和前提的情况.
表 1 MPTP2078问题库描述Table 1. Description of MPTP2078 benchmark条 名称 公式 结论 最小前提 最大前提 平均前提 数量 4 564 2 078 10 4 563 1 876 数据集中每一个例子是一个三元组{结论,前提,标签}. 其中：前提是给定结论的候选前提，标签是二元分类中的类别；标记为1的样本记为正样本，表示前提对结论有用；标记为0的样本记为负样本，表示前提对结论无用. 在问题库中，ATPboost[13]证明了1469个结论并一共产生了24087个证明，这意味着一个结论可能对应多个证明.
正式地，每一个被证明的结论
$ c $ 有${n_{\rm c}}$ （${n_{\rm c}}\geqslant 1$ ）个证明$ {P}_{1} $ ，$ {P}_{2} ,\cdots,{P}_{r},\cdots,$ $ {P}_{n_{{\rm c}}} $ ，且$ {P}_{r}=\{{p}_{r1},{p}_{r2},\cdots, {p}_{rt},$ $ \cdots,{p}_{r{n_{{\rm c }r}}}\}$ ，其中：$ {p}_{rt} $ 为构造证明$ {P}_{r} $ 的一个前提，$ {n_{{\rm c}r}} $ 是$ {P}_{r} $ 中有用前提的总数. 因此，有用前提集$ {\mathcal{U}}_{P}\left(c\right)= {\bigcup }_{r=1}^{n_{\rm c}}{P}_{r} $ 包含至少在结论$ c $ 的所有证明中出现一次的前提.在数据集的构造中，对每一个已证明结论
$ c $ ，其对应的正样本中的前提来自$ {\mathcal{U}}_{P}\left(c\right) $ . 因此，结论$ c $ 对应的正样本为$ \left(c,p,1\right) $ （$ \forall p\in {\mathcal{U}}_{P}\left(c\right) $ ）且正样本的总数为$ \left|{\mathcal{U}}_{P}\left(c\right)\right| $ .然而，问题库中极大部分结论都对应了一个大规模的前提集且
$ {\mathcal{U}}_{P}\left(c\right) $ 包含的有用前提数量仅仅只占总前提数量非常小的一部分. 例如，MPTP2078问题库中的结论$ \mathrm{t}12\_\mathrm{y}\mathrm{e}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{w}\_6 $ 一共包含3836个前提，但只有5个前提被用于证明结论. 这表明结论对应的无用前提数量远远大于有用前提数量. 因此，如果使用$ c $ 的所有无用前提来构造负样本，则正负样本的分布将极度不平衡.为构建与正样本数量相等的负样本，使用文献[22]设计的手工特征表示公式，并使用K近邻（K-nearest neighbor，KNN）[23]算法粗略地对结论的所有前提进行排序. 随后，选择对结论无用但排名靠前的前提构造负样本，其中，无用前提的数量和有用前提大致相同. 最终，整理得到的数据集如表2所示.
表 2 数据集划分Table 2. Division of datasets个 样本 训练集 验证集 测试集 正 27663 3417 3432 负 27556 3485 3471 总样本 55219 6902 6903 4. 实验结果与分析
本文使用Python编程实现了本模型. 在模型搭建的过程中，使用Pytorch库[24]进行深度学习算法的实现，并使用Pytorch_Geometric库[25]处理数据和对实现文中提及的所有图神经网络. 本次实验在超微 4029GP-TRT服务器上进行，具体软硬件配置环境如下：CenterOS7.6 X64，Intel至强银牌4114，256 GB内存，2 TB SSD, 所用GPU为NViDIA RTX 2080Ti.
4.1 实验参数
使用Adam[26]优化器对模型进行训练. 初始化的学习率为0.0010，在50个训练轮次后，学习率衰减为0.0001. 在每个轮次后，对模型进行保存并在验证集上进行评估. 经过所有轮次的训练和验证后，选择在验证集上表现最佳（损失最小）的模型作为最优模型，并在测试集上对其进行评估. 为了保证实验结果的公平性，文章中所有涉及到的模型参数设置均一致. 具体参数如表3所示.
表 3 参数设置Table 3. Setting of parameters参数 设置 节点向量维度$ {d}_{{h}_{v}} $ 64 边向量维度$ {d}_{{h}_{e}} $ 32 迭代次数 K/次 1 学习率 0.0010 学习率衰减系数 0.1 学习率衰减步长 50 轮次/轮 100 权重衰减 0.0001 批量大小/个 8 4.2 评价指标
为评估所提EW-GNN模型的性能，将该模型与具有代表性的图神经网络模型进行比较. 在前提选择任务中，需要根据模型的输出概率对前提进行排序. 因此，需要同时评估正、负样本的正确预测率. 若仅关心正样本的正确预测率，则过多的负样本被错误预测为正时会严重地影响前提的排序，即无用的前提可能会在排序的前列. 当数据集中正、负样本分布均衡时，本文选择准确率
$ {A}_{{\rm{ccuracy}}} $ 指标对模型进行对比分析.$ {A}_{{\rm{ccuracy}}} $ 代表模型判断当前前提对给定结论是否有用的准确程度：Accuracy=TP+TNTotal, (21) 式中：
$ {T}_{{\rm{otal}}} $ 为数据集中所有样本的数量；$ {T}_{{\rm{P}}} $ 为分类正确的正样本的数量；$ {T}_{{\rm{N}}} $ 为分类正确的负样本的数量.本文同时增加召回率
$ {R}_{{\rm{ecall}}} $ 、精确度$ {P}_{{\rm{recision}}} $ 和F1指标F1对模型进行评估：Recall=TPTP+FN, (22) Precision=TPTP+FP, (23) F1=2PrecisionRecallPrecision+Recall, (24) 式中：
$ {F}_{{\rm{N}}} $ 为分类错误的负样本的数量；$ {F}_{{\rm{P}}} $ 为分类错误的正样本的数量.4.3 实验结果分析
为保证对比结果的有效性，实验过程中，只改变前提选择模型中图神经网络模型的部分，而不改变初始化模型以及二元分类模型. 所有方法在均衡数据集上的评估结果如表4所示，最佳结果以黑体突出显示.
表 4 数据集上的对比实验结果Table 4. Comparision of experimental results on datasets实验结果表明，所提出的基于边权重的图神经网络EW-GNN在前提选择任务中明显优于目前其他流行的图神经网络模型：EW-GNN在相同的测试集上至少提高了1%的分类准确率. 从表3中可以看出：除了本文提出的EW-GNN模型，没有另一个模型的分类准确率能够高于其他模型1%. 这说明双向地传播邻接节点的信息有助于帮助图神经网络模型生成更有表征能力的逻辑公式图向量. EW-GNN在更新节点状态向量之间，会首先对边状态向量进行更新. 根据对边类型的构造，边向量既能反映由对应边连接的节点类型，也能反映出节点的顺序. 这对表征一阶逻辑公式非常重要. 因为在一阶逻辑公式图中，不同类型的邻接节点对中心节点的贡献度是不同的. 直觉地，函数节点的贡献明显要大于变量节点，因为变量在一阶逻辑公式的表征中通常都被忽略. 同样地，节点的顺序同样也是逻辑公式图表征不可忽略的重要特性. 如，
$ \forall xp(x,a) $ 和$ \forall xp(a,x) $ 是两个不同的逻辑公式，如果忽略了$ x $ 和$ a $ 的顺序，会导致这两个逻辑公式最终生成的图向量是一样的. 因此，EW-GNN根据更新后的边状态向量为中心节点的每个邻接节点赋予权重，更加符合一阶逻辑公式的特性. 相比之下，本文所提出的EW-GNN模型更加适用于一阶逻辑中的前提选择任务.5. 结 论
1） 本文针对一阶逻辑公式的特性，提出了双向图表示方法，并对每条边设计了能够表示对应节点类型和顺序的边类型.
2） 根据双向图的特性，本文设计并实现了一种基于边权重的图神经网络模型EW-GNN. 该模型既能够双向地传播节点信息，也能利用边向量编码对应节点的类型和顺序.
3） 与当前流行的图神经网络模型相比，本文提出的模型明显在前提选择任务中更具有优势.
4） 针对一阶逻辑公式的特性，未来计划提出更加具有针对性的表征学习模型.
-
图 5 不同控制参数下车体竖向加速度最大值
Figure 5. Maximum values of vertical acceleration of car body under different control parameters
图 6 不同控制参数下悬浮电磁力最大值
Figure 6. Maximum values of suspended electromagnetic force under different control parameters
图 7 不同控制参数下悬浮电磁力幅值谱
Figure 7. Amplitude spectrum of suspended electromagnetic force under different control parameters
图 8 不同控制参数下中间悬浮磁极间隙变化量
Figure 8. Variation of intermediate suspended pole gap under different control parameters
图 9 不同控制参数下悬浮间隙时程曲线及其幅值谱（KD1=25）
Figure 9. Suspension gap time history curve and amplitude spectrum under different control parameters （KD1 = 25）
图 10 不同控制参数下主梁跨中竖向加速度最大值
Figure 10. Maximum values of vertical acceleration at midspan of girder under different control parameters
图 11 不同KD1下主梁跨中竖向加速度幅值谱（KP1=6000）
Figure 11. Amplitude spectrum of vertical acceleration at midspan of girder under different KD1 （KP1 = 6 000）
图 12 不同控制参数下车体横向加速度最大值
Figure 12. Maximum values of lateral acceleration of car body under different control parameters
图 13 不同控制参数下导向电磁力最大值
Figure 13. Maximum values of guidance electromagnetic force under different control parameters
图 14 不同控制参数下导向电磁力幅值谱
Figure 14. Amplitude spectrum of guidance electromagnetic force under control parameters
图 15 不同控制参数下中间导向磁极间隙变化量
Figure 15. Variation of intermediate guidance pole gap under different control parameters
图 16 不同控制参数下主梁跨中横向加速度最大值
Figure 16. Maximum values of lateral acceleration at midspan of girder under different control parameters
图 17 不同KD2下主梁跨中横向加速度幅值谱（KP2=6000）
Figure 17. Amplitude spectrum of lateral acceleration at midspan of girder under different KD2 （KP2 = 6 000）
表 1 车辆模型参数
Table 1. Parameters of train model
参数 数值 车体质量/（× 104 kg） 3.90 车体侧滚质量惯性矩/（× 104 kg•m2） 6.46 车体摇头质量惯性矩/（× 104 kg•m2） 1.75 车体点头质量惯性矩/（× 104 kg•m2） 1.76 一系/二系弹簧竖向刚度/（×106 N•m−1） 20/2 一系/二系弹簧竖向阻尼/（×103 N•s•m−1） 5/5 一系/二系弹簧横向刚度/（×106 N•m−1） 28/2 一系/二系弹簧横向阻尼/（×102 N•s•m−1） 5/20 空气弹簧刚度竖向/（× 106 N•m−1） 1.90 
下载: 导出CSV
表 2 桥梁模型参数
Table 2. Parameters of bridge model
参数 数值 主梁/钢轨/桥墩密度/（kg•m−3） 2551/7850/2500 主梁/钢轨/桥墩弹性模量/GPa 44.5/206.0/30.0 主梁/钢轨/桥墩泊松比 0.2/0.3/0.2
下载: 导出CSV
-
[1] SU X Y, XU Y L, YANG X F. Neural network adaptive sliding mode control without overestimation for a maglev system[J]. Mechanical Systems and Signal Processing, 2022, 168: 108661.1-108661.12. [2] 马卫华,胡俊雄,李铁,等. EMS型中低速磁浮列车悬浮架技术研究综述[J]. 西南交通大学学报,2023,58(4): 720-733.MA Weihua, HU Junxiong, LI Tie, et al. Technologies research review of electro-magnetic suspension medium-low-speed maglev train levitation frame[J]. Journal of Southwest Jiaotong University, 2023, 58(4): 720-733. [3] 熊嘉阳,邓自刚. 高速磁悬浮轨道交通研究进展[J]. 交通运输工程学报,2021,21(1): 177-198.XIONG Jiayang, DENG Zigang. Research progress of high-speed maglev rail transit[J]. Journal of Traffic and Transportation Engineering, 2021, 21(1): 177-198. [4] WANG L D, BU X M, HU P, et al. Dynamic reliability analysis of running safety and stability of a high-speed maglev train on a guideway bridge[J]. International Journal of Structural Stability and Dynamics, 2023: 1-41. [5] 翟明达,朱朋博,李晓龙,等. 常导电磁型高速磁浮列车主动导向能力的评估与验证[J]. 西南交通大学学报,2022,57(3): 514-521.ZHAI Mingda, ZHU Pengbo, LI Xiaolong, et al. Evaluation and verification for active guidance ability of EMS maglev train[J]. Journal of Southwest Jiaotong University, 2022, 57(3): 514-521. [6] 陆海英,韩霄翰,李忠继,等. 中低速磁浮系统起浮阶段的振动特性分析[J]. 中国机械工程,2019,30(3): 318-324.LU Haiying, HAN Xiaohan, LI Zhongji, et al. Analysis of vibration characteristics of low-medium speed maglev levitation systems in lifting stages[J]. China Mechanical Engineering, 2019, 30(3): 318-324. [7] 翟婉明,赵春发. 现代轨道交通工程科技前沿与挑战[J]. 西南交通大学学报,2016,51(2): 209-226.ZHAI Wanming, ZHAO Chunfa. Frontiers and challenges of sciences and technologies in modern railway engineering[J]. Journal of Southwest Jiaotong University, 2016, 51(2): 209-226. [8] 韩霄翰,李忠继,池茂儒. 轨道梁结构对中低速磁浮车轨耦合振动的影响[J]. 铁道机车车辆,2019,39(5): 36-42.HAN Xiaohan, LI Zhongji, CHI Maoru. Influence of track beam structure on the mid-low maglev vehicle-rail coupling vibration[J]. Railway Locomotive & Car, 2019, 39(5): 36-42. [9] FENG Y, ZHAO C F, WU D H, et al. Effect of levitation gap feedback time delay on the EMS maglev vehicle system dynamic response[J]. Nonlinear Dynamics, 2023, 111(8): 7137-7156. doi: 10.1007/s11071-022-08225-5 [10] 赵春发,翟婉明. 常导电磁悬浮动态特性研究[J]. 西南交通大学学报,2004,39(4): 464-468.ZHAO Chunfa, ZHAI Wanming. Dynamic characteristics of electromagnetic levitation systems[J]. Journal of Southwest Jiaotong University, 2004, 39(4): 464-468. [11] 蔡文涛,王春江,滕念管,等. 高速磁浮双向主动控制系统模型参数分析[J]. 力学季刊,2020,41(3): 477-485.CAI Wentao, WANG Chunjiang, TENG Nianguan, et al. Study on the parameters of bi-directional active control system for high speed maglev[J]. Chinese Quarterly of Mechanics, 2020, 41(3): 477-485. [12] 梁鑫,罗世辉,马卫华. 单磁铁悬浮控制系统反馈参数动力学特性分析[J]. 噪声与振动控制,2012,32(5): 62-66,135.LIANG Xin, LUO Shihui, MA Weihua. Dynamic characteristics of feedback coefficient of single magnet suspension control system[J]. Noise and Vibration Control, 2012, 32(5): 62-66,135. [13] 汤港归,汪斌,夏翠鹏,等. 磁浮车辆起浮参数控制及其动力性能研究[J]. 铁道科学与工程学报,2023,20(3): 790-801.TANG Ganggui, WANG Bin, XIA Cuipeng, et al. Control of levitation parameters and dynamic performance of maglev vehicle[J]. Journal of Railway Science and Engineering, 2023, 20(3): 790-801. [14] SUN Y G, HE Z Y, XU J Q, et al. Dynamic analysis and vibration control for a maglev vehicle-guideway coupling system with experimental verification[J]. Mechanical Systems and Signal Processing, 2023, 188: 109954.1-109954.18. [15] 杨志南,冯洋,刘东生,等. 悬浮控制参数对磁浮车辆与道岔梁耦合振动的影响分析[J]. 机械,2022,49(2): 38-46.YANG Zhinan, FENG Yang, LIU Dongsheng, et al. Influence of levitation control parameters on coupled vibration between maglev vehicles and switch girder[J]. Machinery, 2022, 49(2): 38-46. [16] XIANG H Y, TIAN X F, LI Y L, et al. Dynamic interaction analysis of high-speed maglev train and guideway with a control loop failure[J]. International Journal of Structural Stability and Dynamics, 2022, 22(10): 2241012.1-224101228. [17] GUO W, CHEN X Y, YE Y T, et al. Coupling vibration analysis of high-speed maglev train-viaduct systems with control loop failure[J]. Journal of Central South University, 2022, 29(8): 2771-2790. doi: 10.1007/s11771-022-5119-1 [18] 谢云德,常文森. 电磁型(EMS)磁悬浮列车系统铅垂方向的建模与仿真[J]. 铁道学报,1996,18(4): 47-54.XIE Yunde, CHANG Wensen. Modeling and simulation of electromagnetic (EMS) maglev train system in vertical direction[J]. Journal of the China Railway Society, 1996, 18(4): 47-54. [19] ZHANG L, HUANG J Y. Dynamic interaction analysis of the high-speed maglev vehicle/guideway system based on a field measurement and model updating method[J]. Engineering Structures, 2019, 180: 1-17. doi: 10.1016/j.engstruct.2018.11.031 [20] 张宝安,虞大联,李海涛,等. 高速磁浮悬浮架柔性特征对曲线通过性能的影响[J]. 西南交通大学学报,2022,57(3): 475-482.ZHANG Baoan, YU Dalian, LI Haitao, et al. Influence of flexibility characteristics of levitation chassis on curve negotiation performance of high-speed maglev vehicle[J]. Journal of Southwest Jiaotong University, 2022, 57(3): 475-482. [21] ZHAO C F, ZHAI W M. Maglev vehicle/guideway vertical random response and ride quality[J]. Vehicle System Dynamics, 2002, 38(3): 185-210. doi: 10.1076/vesd.38.3.185.8289 [22] SHI J, FANG W S, WANG Y J, et al. Measurements and analysis of track irregularities on high speed maglev lines[J]. Journal of Zhejiang University-Science A, 2014, 15(6): 385-394. doi: 10.1631/jzus.A1300163 [23] WANG Z L, XU Y L, LI G Q, et al. Modelling and validation of coupled high-speed maglev train-and-viaduct systems considering support flexibility[J]. Vehicle System Dynamics, 2019, 57(2): 161-191. doi: 10.1080/00423114.2018.1450517 [24] SHI J, WANG Y J. Dynamic response analysis of single-span guideway caused by high speed maglev train[J]. Latin American Journal of Solids and Structures, 2011, 8(3): 213-228. doi: 10.1590/S1679-78252011000300001 [25] XU Y L, WANG Z L, LI G Q, et al. High-speed running maglev trains interacting with elastic transitional viaducts[J]. Engineering Structures, 2019, 183: 562-578. doi: 10.1016/j.engstruct.2019.01.012 [26] 徐金辉,王平,汪力,等. 基于频域分析方法的轨道高低不平顺敏感波长的研究[J]. 中南大学学报(自然科学版),2016,47(2): 683-689.XU Jinhui, WANG Ping, WANG Li, et al. Sensitive wavelengths of vertical track irregularities by frequency-domain method[J]. Journal of Central South University (Science and Technology), 2016, 47(2): 683-689. -
下载:
下载:
点击查看大图
计量
- 文章访问数: 500
- HTML全文浏览量: 246
- PDF下载量: 77
- 被引次数: 0