About the programme
AI for Program Reasoning aims to design novel agentic AI techniques for cost-effective automatic program reasoning. This project targets both legacy systems and future AI-assisted software, where AI-generated code is integrated into existing systems. By developing approaches that advance agentic program analysis and proof with augmented code Large Language Models (LLMs), the project aims to establish versatile toolkits to reason about complex software systems, such as components in kernels, network and consensus protocols, and multilingual codebases.
Beyond software engineering, we aim to develop novel agentic AI architectures designed for structured reasoning that are applicable to other scientific fields. This approach could be translated for various applications, such as medical devices, one-health response, and smart cities.
The challenge
Software bugs and security vulnerabilities pose critical threats to systems our society depends on, leading to economic losses, privacy breaches, accidents, and hindered scientific progress. With the advent of LLMs, an increasing amount of code is generated automatically by autonomous coding agents. However, this can result in generated code that introduces or propagates security vulnerabilities.
As AI-driven code generation outpaces program reasoning approaches, conventional techniques become prohibitively slow and expensive to support fast-evolving systems. For instance, proving the correctness of a highly secure operating system component required 200,000 lines of manual specifications and 20 person-years of PhD-level effort. We need cost-effective automated program reasoning solutions.
Our research themes
Theme A: Democratising Program Reasoning via Agentic Analysis Generation
Building program analysis tools has always required significant and sustained effort. The symbolic analysis engine, a widely used tool for finding bugs in software, took years to develop and has been used to find vulnerabilities in hundreds of real-world projects.
Existing tools struggle to keep up with the growing diversity of programming languages and increasing volume of code generated by LLMs. Generative AI offers a way to change this.
We are developing AI systems that can automatically analyse what a program does and summarise it in plain language, making complex code understandable without years of manual effort.This works across any programming language including the specialised languages used in scientific research, where existing tools have historically offered little support. We are also developing AI systems that can break down complex software problems into smaller, manageable steps and solve them automatically.
ConcoLLMic is the first language- and theory-agnostic concolic executor powered by LLM agents.
Theme B: Advancing Code LLM Technology
LLMs excel at generating structurally accurate code, but they struggle to reason deeply about what that code actually does – its control flow, data dependencies and formal correctness. This is a significant limitation for reliability and verification.
We are developing structured training approaches that teach LLMs to reason about programs with genuine semantic understanding, rather than pattern matching. This involves training our models on specialised datasets rich in formal reasoning content, teaching them to perform tasks such as constructing proofs, identifying and fixing errors in code, and verifying that software behaves as intended.
A distinctive feature of AI for Program Reasoning is self-reflection, where, after generating a proof or a fix, the model critiques its own output – evaluating whether constraints are satisfied, whether the proof aligns with its goals, and whether edge cases are addressed. This iterative generation, reflection and revision cycle equips the model with the ability to detect inconsistencies and adapt to novel reasoning scenarios.
We are also building a comprehensive benchmark suite for code reasoning and verification, covering runtime behaviour prediction, control and data flow analysis, type inference, proof synthesis, and domain-specific formal reasoning. All datasets and evaluation tools will be released publicly to support reproducibility and community adoption.
Theme C: Program Verification Agents
Formal program verification has produced landmark achievements in computer science, but the cost has historically been a significant barrier.
We are using generative AI to automate the most labour-intensive stages of verification. We are developing LLM agents that can infer formal specifications from code, construct proof candidates, and refine those proofs based on feedback from theorem provers. This builds a reinforcement learning loop that continuously improves the agent's proof construction capability.
We are also tackling the combined problem of program and proof repair. Given a buggy program and a failed proof attempt, our system can propose modifications to fix the system.
These techniques are demonstrated on real-world software providing practical evidence of their effectiveness at scale.