Christopher Brix

Computer Science PhD Candidate at RWTH Aachen University, Germany

Hello! I'm a computer science PhD candidate at the RWTH Aachen University in Germany, focusing on proving safety properties of neural networks, such as robustness against adversarial examples. Previously, as a student research assistant, I've gained extensive experience in machine translation research using neural networks. I've published first-author papers at NeurIPS, ACL, and other venues, and have also had the opportunity to complete research internships at both Google and Amazon (twice). I'm one of the organizers of the international neural network verification competition VNN-COMP.

Download CV

Selected publications:

Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes
Conference on Neural Information Processing Systems (NeurIPS) 2024

Provably Bounding Neural Network Preimages
Conference on Neural Information Processing Systems (NeurIPS) 2023

2021-2025
Ph.D. Computer Science, RWTH Aachen University, Germany

For my PhD thesis, I am investigating approaches that allow to generate mathematical proofs for properties of neural network, such as the robustness against adversarial attacks.
2018-2020
M.Sc. Computer Science, RWTH Aachen University, Germany

I've continued to work as a student research assistant, co-authoring two publications. In my master thesis, I proposed and evaluated a new technique to prove the non-existance of adversarial examples in neural networks, using an improved version of symbolic propagation. It was graded 1.0. Final overall grade: 1.5
2014-2018
B.Sc. Computer Science, RWTH Aachen University, Germany

Early on, I decided to specialize in machine learning, and attended several lectures and seminars on this topic. I also started to work as a student research assistant at our local chair for natural language processing. My bachelor thesis "Extension of the Attention Mechanism in Neural Machine Translation" dealt with the application of two-dimensional LSTM cells that could replace the attention mechanism in neural machine translation. It was graded 1.2. Final overall grade: 1.6

CERTPHASH: Towards Certified Perceptual Hashing via Robust Training

Y. Yang, Q. Liu, C. Brix, H. Zhang, and Y. Cao.
USENIX Security Symposium, 2025

Perceptual hashing (PHash) systems — e.g., Apple's NeuralHash, Microsoft's PhotoDNA, and Facebook's PDQ — are widely employed to screen illicit content. Such systems generate hashes of image files and match them against a database of known hashes linked to illicit content for filtering. One important drawback of PHash systems is that they are vulnerable to adversarial perturbation attacks leading to hash evasion or collision. It is desirable to bring provable guarantees to PHash systems to certify their robustness under evasion or collision attacks. However, to the best of our knowledge, there are no existing certified PHash systems, and more importantly, the training of certified PHash systems is challenging because of the unique definition of model utility and the existence of both evasion and collision attacks.
In this paper, we propose CertPHash, the first certified PHash system with robust training. CertPHash includes three different optimization terms, anti-evasion, anti-collision, and functionality. The anti-evasion term establishes an upper bound on the hash deviation caused by input perturbations, the anti-collision term sets a lower bound on the distance between a perturbed hash and those from other inputs, and the functionality term ensures that the system remains reliable and effective throughout robust training. Our results demonstrate that CertPHash not only achieves non-vacuous certification for both evasion and collision with provable guarantees but is also robust against empirical attacks. Furthermore, CertPHash demonstrates strong performance in real-world illicit content detection tasks.

Read the abstract Read the paper

Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang.
Conference on Neural Information Processing Systems (NeurIPS) 2024

Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advances. However, GCP-CROWN currently relies on generic cutting planes ("cuts") generated from external mixed integer programming (MIP) solvers. Due to the poor scalability of MIP solvers, large neural networks cannot benefit from these cutting planes. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes specific for this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), which leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts. Furthermore, we design a multi-tree search technique to identify more cuts, effectively narrowing the search space and accelerating the BaB algorithm. Our results demonstrate that BICCOS can generate hundreds of useful cuts during the branch-and-bound process and consistently increase the number of verifiable instances compared to other state-of-the-art neural network verifiers on a wide range of benchmarks, including large networks that previous cutting plane methods could not scale to. BICCOS is part of the α,β-CROWN verifier, the VNN-COMP 2024 winner. The code is available at https://github.com/Lemutisme/BICCOS.

Read the abstract Read the paper

Provably Bounding Neural Network Preimages

S. Kotha*, C. Brix*, Z. Kolter, K. Dvijotham, and H. Zhang. *Shared first-authorship; spotlight poster
Conference on Neural Information Processing Systems (NeurIPS) 2023

Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the α,β-CROWN verifier, available at https://abcrown.org

Read the abstract Read the paper

First Three Years of the International Verification of Neural Networks Competition (VNN-COMP).

C. Brix, M. N. Müller, S. Bak, T. T. Johnson, and C. Liu.
International Journal on Software Tools for Technology Transfer (STTT) 2023

This paper presents a summary and meta-analysis of the first three iterations of the annual International Verification of Neural Networks Competition (VNN-COMP), held in 2020, 2021, and 2022. In the VNN-COMP, participants submit software tools that analyze whether given neural networks satisfy specifications describing their input-output behavior. These neural networks and specifications cover a variety of problem classes and tasks, corresponding to safety and robustness properties in image classification, neural control, reinforcement learning, and autonomous systems. We summarize the key processes, rules, and results, present trends observed over the last three years, and provide an outlook into possible future developments.

Read the abstract Read the paper

Successfully Applying the Stabilized Lottery Ticket Hypothesis to the Transformer Architecture

C. Brix, P. Bahar, and H. Ney.
Annual Conference of the Association for Computational Linguistics (ACL) 2020

Sparse models require less memory for storage and enable a faster inference by reducing the necessary number of FLOPs. This is relevant both for time-critical and on-device computations using neural networks. The stabilized lottery ticket hypothesis states that networks can be pruned after none or few training iterations, using a mask computed based on the unpruned converged model. On the transformer architecture and the WMT 2014 English-to-German and English-to-French tasks, we show that stabilized lottery ticket pruning performs similar to magnitude pruning for sparsity levels of up to 85%, and propose a new combination of pruning techniques that outperforms all other techniques for even higher levels of sparsity. Furthermore, we confirm that the parameter's initial sign and not its specific value is the primary factor for successful training, and show that magnitude pruning could be used to find winning lottery tickets.

Read the abstract Read the paper

Towards Two-Dimensional Sequence to Sequence Model in Neural Machine Translation

P. Bahar, C. Brix, and H. Ney.
Conference on Empirical Methods in Natural Language Processing (EMNLP) 2018

This work investigates an alternative model for neural machine translation (NMT) and proposes a novel architecture, where we employ a multi-dimensional long short-term memory (MDLSTM) for translation modelling. In the state-of-the-art methods, source and target sentences are treated as one-dimensional sequences over time, while we view translation as a two-dimensional (2D) mapping using an MDLSTM layer to define the correspondence between source and target words. We extend beyond the current sequence to sequence backbone NMT models to a 2D structure in which the source and target sentences are aligned with each other in a 2D grid. Our proposed topology shows consistent improvements over attention-based sequence to sequence model on two WMT 2017 tasks, German↔English.

Read the abstract Read the paper

Empirical Investigation of Optimization Algorithms in Neural Machine Translation

P. Bahar, T. Alkhouli, J.-T. Peter, C. Brix, and H. Ney.
The Prague Bulletin of Mathematical Linguistics (PBML) 2017

Training neural networks is a non-convex and a high-dimensional optimization problem. In this paper, we provide a comparative study of the most popular stochastic optimization techniques used to train neural networks. We evaluate the methods in terms of convergence speed, translation quality, and training stability. In addition, we investigate combinations that seek to improve optimization in terms of these aspects. We train state-of-the-art attention-based models and apply them to perform neural machine translation. We demonstrate our results on two tasks: WMT 2016 En→Ro and WMT 2015 De→En.

Read the abstract Read the paper

Jul 2024 -
Nov 2024
Applied Scientist Intern, Amazon (Seattle)

I worked on two projects: I developed a benchmark and evaluation pipeline for the robustness/consistency of the Seller Assistant, a chat bot for Amazon selling partners, in the face of input perturbations. This allowed to identify critical inconsistencies and generate a comprehensive robustness score of the system. Furthermore, I investigated the relation between task complexity, network capacity and attainable network robustness by training more than 30,000 networks.
Jul 2023 -
Nov 2023
Applied Scientist Intern, Amazon (Boston)

I replicated and extended AlphaDev, a reinforcement algorithm for code generation. AlphaDev requires extensive testing of the generated code to ensure its correctness. To extend the application to more complex tasks, I incorporated Dafny, a verification-aware programming language, to automatically prove code correctness.
Sep 2020 -
Jan 2021
Research SWE Intern, Google Zurich (remotely)

During my internship, I investigated the application of a fine-tuned BERT model for named entity recognition. To this end, I analyzed multiple datasets, wrote an augmentation script and evaluated a variety of different training techniques. I was able to improve key metrics by up to 25 percentage points (57% to 82%). As a side project, I managed a program that connected interns with each other for 1:1 chats, setting up approximately 700 meetings.
Nov 2016 -
Feb 2020
Student Research Assistant, RWTH Aachen University

At the Human Language Technology and Pattern Recognition chair (Professor Ney), I mainly focused on analyzing alternatives for the attention mechanism in NMT. I investigated the usage of two-dimensional LSTMs for machine translation tasks, implementing the corresponding code in C/CUDA and integrating it into the inhouse machine learning framework (RETURNN). Furthermore, I independently worked on a paper about comparisons and improvements of sparsity in complex network architectures.

2024
Heidelberg Laureate Forum

I was selected as one of 200 young researchers worldwide to participate in the Heidelberg Laureate Forum. The forum is a week-long event where laureates of the Abel Prize, the Fields Medal, the Nevanlinna Prize, and the Turing Award meet with young researchers. I received the Abbe Grant to cover the costs of my participation.
2021
Invited Talk at Google Munich

One of the teams working on privacy in machine learning invited me to talk about the current state of the art in network verification, as well as results from my master thesis.
2020
ICT Young Researcher Award

For my research work, especially on novel network architectures in machine translation, I received the ICT Young Researcher Award from the Information and Communication Technology Committee of the RWTH Aachen University. The award included a monetary prize of €1500.
2020
Invited Talk at Fraunhofer IAIS

The Fraunhofer Institute for Intelligent Analysis and Information Systems invited me to give a presentation. Topics included both my own research, as well as an overview over current research topics in neural machine translation. Slides: Current State of Research in NMT (German version).
2019
Google NLP Summit

As one of a limited number of master students, I was accepted to the 3rd NLP Summit organized by Google. In Zurich, we attended talks of Google researchers about cutting edge NLP technology. We discussed current open problems and presented our own research ideas. Total number of accepted attendees: 90.
2016, 2018
Received the scholarship "Deutschlandstipendium"

Awarded a monetary prize of €3600 each.
2016, 2017
Member of the Dean's List

Awarded to the top 5% of all CS students.

brix@cs.rwth-aachen.de

Christopher Brix
Willemslägerweg 15a
52159 Roetgen
Germany