Neural Reasoning for Program Analysis

Abstract

Neural reasoning models are revolutionizing the way we address long-standing chal-
lenges in software development. From program synthesis and debugging to code
optimization and translation, these models leverage deep learning to understand,
generate, and refine code with unprecedented efficiency. By learning patterns from
vast code repositories, these technologies promise to make programming more acces-
sible, efficient, and collaborative, bridging the gap between human creativity and
computational intelligence.
This thesis explores these advancements by applying neural reasoning to program
analysis and transformation. The first part focuses on predicting program termination
using Graph Neural Networks (GNNs), such as Graph Convolutional Networks
(GCNs) and Graph Attention Networks (GATs). This approach identifies likely
causes of nontermination and localizes issues within the program’s abstract syntax
trees (ASTs).
The second part addresses the challenges of long-term planning in Large Language
Models (LLMs) through a novel hybrid architecture. Here, a Reinforcement Learning
(RL) agent guides the exploration of solution spaces, evaluating the quality of
intermediate reasoning steps based on domain-specific metrics. This setup allows
the LLM to focus on generating immediate next steps while enabling non-linear
reasoning through backtracking and alternative path exploration. Evaluated on the
program equivalence task, this approach demonstrates improved performance in both
reasoning and classification compared to traditional methods like Chain of Thought
and Tree of Thoughts.
In the third part, we evaluate the capability of large language models to predict
program termination. We evaluate the ability of general-purpose large language
models to accurately classify and reason about the termination properties of programs.
Building on these findings, we propose enhancing large language models by fine-
tuning their encoder transformer to function as a program feature extractor, equipped
with a classification head for binary termination prediction.

Date of Award	30 Sept 2025
Original language	English
Awarding Institution	University of Bristol
Supervisor	Cristina David (Supervisor)