Chencheng Liang: Learning to Guide Automated Reasoning: A GNN-Based Framework

Abstract

Symbolic methods play a crucial role in reasoning tasks such as program verification, theorem proving, and constraint solving. These methods rely on heuristic-driven decision processes to efficiently explore large or infinite state spaces. Traditional heuristics, while effective, are manually designed and often struggle with generalization across different problem domains. This dissertation introduces a deep learning-based framework to replace or augment heuristic decision-making in symbolic methods, enabling adaptive and data-driven guidance.

The framework leverages Graph Neural Networks (GNNs) to learn structural patterns from symbolic expressions, formulating decision problems as classification or ranking tasks. We propose novel graph representations for Constrained Horn Clauses (CHCs) and word equations, capturing both syntactic and semantic properties to facilitate effective learning. Various GNN architectures, including Graph Convolutional Networks (GCNs) and Relational Hypergraph Neural Networks (R-HyGNNs), are evaluated for their suitability in different symbolic reasoning tasks.

We implement the framework in a CHC solver and a word equation solver, demonstrating that learning-based heuristics can improve solver efficiency by guiding key decision processes such as clause selection and branch selection. The dissertation also explores different strategies for integrating trained models into solvers, balancing computational overhead with performance gains through caching, hybrid heuristics, and selective model querying.

Experimental results show that our framework consistently enhances solver performance, particularly in challenging problem domains. The findings suggest that deep learning can significantly improve symbolic reasoning by learning adaptive heuristics, paving the way for further integration of machine learning in formal methods.

Future research directions include extending the word equation solver, optimizing GNN architectures, and expanding training data sources.