A neural network verification tool is learning to make smarter decisions about where to search for hidden flaws in AI systems, rather than blindly checking every possibility. This matters because AI systems are now being deployed in safety-critical settings—self-driving cars on British motorways, and NHS diagnostic tools for cancers and strokes—where a single wrong prediction could have serious consequences. Current verification methods can theoretically prove that a neural network will behave correctly, but they do not scale to large models. The state-of-the-art tools focus on efficient bounding techniques while relying on hand-crafted branching strategies that lag behind. This project develops a methodology for learning branching heuristics—essentially teaching the verifier which paths through the search space are most promising. It also tackles the representation problem for these heuristics, the first comprehensive study of its kind. If successful, the techniques will be integrated into a state-of-the-art tool and evaluated on VNN-COMP benchmarks and medically critical use-cases from NHS partners. The result could make formal verification practical for the large neural networks already entering everyday infrastructure, from transport to healthcare.
View original technical description
Despite significant progress in developing more scalable neural network (NN) verification tools, efficient verification of large models is not feasible yet. Verification can help to build trust in Artificial Intelligence (AI) technologies that are being increasingly deployed across various domains, including safety-critical ones, such as autonomous driving vehicles and medical diagnosis. For instance, a first hands-free self-driving system has been recently approved for British motorways. Notably, key components of autonomous vehicles, such as vision systems, rely heavily on AI. In the National Health Service (NHS), AI technology has the potential to transform healthcare by diagnosing conditions such as cancers, strokes and heart conditions earlier: the Health and Social Care Secretary announced a new £21 million AI Diagnostic Fund to accelerate the deployment of AI imaging and decision support tools at NHS Trusts. Reliability of such tools is essential, given that automation bias affects even very experienced medical professionals. This project develops novel techniques to improve scalability of the state-of-the-art NN verification tools: branching heuristics for more efficient navigation of the search space and learning representations for fast heuristic computation. The promise of the formal verification approach is that it can detect possible issues with neural network models or provide theoretical guarantees to the correctness, fairness, etc, of their behaviour. For instance, for a road sign recognition model, we can check if introducing noise to a stop sign image may force the classifier to change its prediction to a speed limit sign. A verifier would either find a possible perturbation that results in the wrong prediction, or would declare local robustness of the model in this instance. Similarly, for a loan approval model, we can check that inputs agreeing on all attributes save for the protected ones (e.g., gender, race and age) are classified in the same way. A major limitation of the verification approach is that it does not scale with the size of NNs. The state-of-the-art NN verification tools employ the branch-and-bound method to systematically search the space. They mainly focus on deriving efficient bounding techniques, but overlook the branching component, relying on hand-crafted branching strategies. The tools that specifically focus on the branching heuristics, on the other hand, lag behind the state-of-the-art tools. In this project we will develop a novel methodology for learning branching heuristics. In addition to that, to make sure that the learned heuristics can be efficiently computed, we will study the representation problem for branching heuristics, the first comprehensive study of its kind. We will use our framework to produce good and efficiently computable branching heuristics and integrate them into a state-of-the-art tool. We evaluate our techniques against the state-of-the-art tools on VNN-COMP benchmarks and on medically critical use-cases from our NHS partners.
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know