Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LogicMP: A Neuro-symbolic Approach for Encoding First-order Logic Constraints

Weidi Xu, Jingwei Wang, Lele Xie, Jianshan He, Hongting Zhou, Taifeng Wang, Xiaopei Wan, Jingdong Chen, Chao Qu, Wei Chu

TL;DR

LogicMP introduces a differentiable neuro-symbolic layer that encodes first-order logic constraints via mean-field inference on Markov Logic Networks, enabling plug-and-play integration with any neural encoder. By reformulating MF updates as parallel tensor operations through clause-level simplifications and parallel Einstein summation, LogicMP reduces the traditional MF complexity and achieves scalable inference on groundings up to the order of 10^5–10^6, e.g., 262K variables within 0.03 seconds. Empirically, LogicMP delivers accuracy and efficiency gains across document image understanding, relational graph reasoning, and sequence labeling tasks, outperforming advanced neuro-symbolic baselines and enabling training on larger grounding sets. The approach demonstrates the practical value of combining MLN-based FOLCs with neural representations, enabling structured predictions that honor logical constraints in diverse real-world data domains.

Abstract

Integrating first-order logic constraints (FOLCs) with neural networks is a crucial but challenging problem since it involves modeling intricate correlations to satisfy the constraints. This paper proposes a novel neural layer, LogicMP, whose layers perform mean-field variational inference over an MLN. It can be plugged into any off-the-shelf neural network to encode FOLCs while retaining modularity and efficiency. By exploiting the structure and symmetries in MLNs, we theoretically demonstrate that our well-designed, efficient mean-field iterations effectively mitigate the difficulty of MLN inference, reducing the inference from sequential calculation to a series of parallel tensor operations. Empirical results in three kinds of tasks over graphs, images, and text show that LogicMP outperforms advanced competitors in both performance and efficiency.

LogicMP: A Neuro-symbolic Approach for Encoding First-order Logic Constraints

TL;DR

LogicMP introduces a differentiable neuro-symbolic layer that encodes first-order logic constraints via mean-field inference on Markov Logic Networks, enabling plug-and-play integration with any neural encoder. By reformulating MF updates as parallel tensor operations through clause-level simplifications and parallel Einstein summation, LogicMP reduces the traditional MF complexity and achieves scalable inference on groundings up to the order of 10^5–10^6, e.g., 262K variables within 0.03 seconds. Empirically, LogicMP delivers accuracy and efficiency gains across document image understanding, relational graph reasoning, and sequence labeling tasks, outperforming advanced neuro-symbolic baselines and enabling training on larger grounding sets. The approach demonstrates the practical value of combining MLN-based FOLCs with neural representations, enabling structured predictions that honor logical constraints in diverse real-world data domains.

Abstract

Integrating first-order logic constraints (FOLCs) with neural networks is a crucial but challenging problem since it involves modeling intricate correlations to satisfy the constraints. This paper proposes a novel neural layer, LogicMP, whose layers perform mean-field variational inference over an MLN. It can be plugged into any off-the-shelf neural network to encode FOLCs while retaining modularity and efficiency. By exploiting the structure and symmetries in MLNs, we theoretically demonstrate that our well-designed, efficient mean-field iterations effectively mitigate the difficulty of MLN inference, reducing the inference from sequential calculation to a series of parallel tensor operations. Empirical results in three kinds of tasks over graphs, images, and text show that LogicMP outperforms advanced competitors in both performance and efficiency.
Paper Structure (35 sections, 7 theorems, 23 equations, 18 figures, 9 tables, 2 algorithms)

This paper contains 35 sections, 7 theorems, 23 equations, 18 figures, 9 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Markov Logic Networks
  3. Mean-field Iteration for MLN Inference
  4. Computational Complexity Analysis
  5. Efficient Mean-field Iteration via LogicMP
  6. Less Computation per Grounding Message
  7. Parallel Aggregation using Einstein Summation
  8. Multiple MF Iterations as LogicMP
  9. Related Work
  10. Experiments
  11. Encoding FOLC over Document Images
  12. Encoding FOLCs over Relational Graphs
  13. Encoding FOLCs over Text
  14. Conclusion
  15. Mean-field Iteration Equation of MLN Inference
  16. ...and 20 more sections

Key Result

Theorem 3.1

(Message of clause considers true premise only.) For a clause formula $f(\cdot; \mathbf{n})$, the MF iteration of Eq. equ:meanfield is equivalent for $\hat{Q}_{i,g} (v_i) \gets \bm{1}_{v_i=\neg n_i} \prod_{j \in {g_{-i}}} Q_j(v_j=n_j)$.

Figures (18)

  • Figure 1: The document understanding task predicts whether every two tokens coexist in the same block in an input document image (a). The FOLC regarding the transitivity of coexistence can be used to obtain the structured output. The ground truth (b) typically forms several squares for the segments. Both NN DBLP:conf/kdd/XuL0HW020 (c) and advanced method DBLP:conf/icml/XuZFLB18 (d) struggle to meet the FOLC where many $\mathtt{coexist}$ variables are incorrectly predicted. In contrast, LogicMP (e) is effective while maintaining modularity and efficiency. See Sec. \ref{['sec:exp']} for complete experimental details.
  • Figure 2: A high-level view of LogicMP. NNs typically use the softmax layer for independent prediction (left), which can be replaced by a LogicMP encoding FOLCs (middle). LogicMP is implemented (right) by efficient mean-field iterations which leverage the structure of MLN (Sec. \ref{['sec:logicmp']}).
  • Figure 3: For the grounding message of $g$ w.r.t $\mathtt{C}(e_1,e_2) \wedge \mathtt{C}(e_2,e_3) \Rightarrow \mathtt{C}(e_1,e_3)$, only one assignment of $g_{-\mathtt{C}(e_1,e_3)}$ makes difference to $\mathtt{C}(e_1,e_3)$, i.e., useful.
  • Figure 4: Instead of sequentially generating groundings (left), we exploit the structure of rules and formalize the MF iteration into Einstein summation notation, which enables parallel computation (right).
  • Figure 5: Comparison of F1 on FUNSD. Better results are in bold. "full" denotes the full set while "long" only considers the blocks with more than 20 tokens. "-" means failure.
  • ...and 13 more figures

Theorems & Definitions (13)

  • Theorem 3.1
  • Theorem 3.2
  • Proposition
  • proof
  • Lemma C.1
  • proof
  • proof
  • proof
  • Corollary D.1
  • Theorem E.1
  • ...and 3 more