# Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)

arXiv: https://arxiv.org/abs/2206.06986 · HTML: https://mlsanity.com/paper/2206.06986/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 57 references that are in the map.
- First posted on arXiv 14 Jun 2022.

## Builds on (most cited first, 29 of 29)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Auto-Encoding Variational Bayes](https://mlsanity.com/paper/1312.6114/) (2013)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Modeling Relational Data with Graph Convolutional Networks](https://mlsanity.com/paper/1703.06103/) (2017)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [Gated Graph Sequence Neural Networks](https://mlsanity.com/paper/1511.05493/) (2015)
- [CodeXGLUE: A Machine Learning Benchmark Dataset for Code Understanding and Generation](https://mlsanity.com/paper/2102.04664/) (2021)
- [CodeSearchNet Challenge: Evaluating the State of Semantic Code Search](https://mlsanity.com/paper/1909.09436/) (2019)
- [Hypergraph Neural Networks](https://mlsanity.com/paper/1809.09401/) (2018)
- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Syntax-Directed Variational Autoencoder for Structured Data](https://mlsanity.com/paper/1802.08786/) (2018)
- [A Convolutional Attention Network for Extreme Summarization of Source Code](https://mlsanity.com/paper/1602.03001/) (2016)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Neural Code Comprehension: A Learnable Representation of Code Semantics](https://mlsanity.com/paper/1806.07336/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [LambdaNet: Probabilistic Type Inference using Graph Neural Networks](https://mlsanity.com/paper/2005.02161/) (2020)
- [Structural Deep Embedding for Hyper-Networks](https://mlsanity.com/paper/1711.10146/) (2017)
- [Learning and Evaluating Contextual Embedding of Source Code](https://mlsanity.com/paper/2001.00059/) (2019)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Convolutional Neural Networks over Tree Structures for Programming Language Processing](https://mlsanity.com/paper/1409.5718/) (2014)
- [Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)](https://mlsanity.com/paper/1301.4973/) (2013)
- [Competition Report: CHC-COMP-21](https://mlsanity.com/paper/2109.04635/) (2021)

## Built on by (most cited first, 1 of 1)

- [Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)](https://mlsanity.com/paper/2411.15194/) (2024)

## Abstract (arXiv)

Learning program semantics from raw source code is challenging due to the complexity of real-world programming language syntax and due to the difficulty of reconstructing long-distance relational information implicitly represented in programs using identifiers. Addressing the first point, we consider Constrained Horn Clauses (CHCs) as a standard representation of program verification problems, providing a simple and programming language-independent syntax. For the second challenge, we explore graph representations of CHCs, and propose a new Relational Hypergraph Neural Network (R-HyGNN) architecture to learn program features. We introduce two different graph representations of CHCs. One is called constraint graph (CG), and emphasizes syntactic information of CHCs by translating the symbols and their relations in CHCs as typed nodes and binary edges, respectively, and constructing the constraints as abstract syntax trees. The second one is called control- and data-flow hypergraph (CDHG), and emphasizes semantic information of CHCs by representing the control and data flow through ternary hyperedges. We then propose a new GNN architecture, R-HyGNN, extending Relational Graph Convolutional Networks, to handle hypergraphs. To evaluate the ability of R-HyGNN to extract semantic information from programs, we use R-HyGNNs to train models on the two graph representations, and on five proxy tasks with increasing difficulty, using benchmarks from CHC-COMP 2021 as training data. The most difficult proxy task requires the model to predict the occurrence of clauses in counter-examples, which subsumes satisfiability of CHCs. CDHG achieves 90.59% accuracy in this task. Furthermore, R-HyGNN has perfect predictions on one of the graphs consisting of more than 290 clauses. Overall, our experiments indicate that R-HyGNN can capture intricate program features for guiding verification problems.