Olaf Beyersdorff: A researcher with a recurrent academic home in Chennai
October 10, 2024 | Bharti Dharapuram
Olaf Beyersdorff is a Professor of Theoretical Computer Science at Friedrich Schiller University Jena who works on proof complexity. He first came to IMSc as a PhD student and has continued to collaborate with researchers here ever since, introducing many of his own students to the campus. While on a recent visit, we caught up with him to chat about his research interests and his enduring association with IMSc.
What is the broad area of your research?
The area that we work in is called proof complexity, which is a branch of theoretical computer science. Proof complexity is a special facet of complexity (or computational complexity), which started about fifty to sixty years ago as a theoretical endeavour to understand the complexity of proofs for mathematical statements. It is a meeting point of a couple of disciplines fundamental to theoretical computer science, namely, logic, algorithms and complexity.
Imagine that we have a mathematical statement, which we know is true and, therefore, has a valid proof. We specify this theorem and want to understand how complex or long the proof needs to be. In order to make that a rigorous question, we need to define a formal proof system – a language in which to write down the proof succinctly and formally. Once we have these two things at hand [a theorem and a formal proof system], one can ask - ‘What is the shortest proof of the theorem in that formal system?’ This is the basic question that we are interested in, and the field has a long tradition of investigating many proof systems.
A surprising discovery over the last 20 years has been that proof complexity has close connections to another area called solving. It is an area where practitioners try to solve complex computational problems that arise in many areas such as software verification, hardware verification and model checking. These problems often don't have good algorithmic solutions, but existing algorithms try to solve them as efficiently as possible. While they do not always succeed to give an answer, they do so in many industrial instances. And we don’t really understand why. Proof complexity comes into the picture here, because it provides the main theoretical framework to try and answer this question.
We have been looking at proof complexity of Quantified Boolean Formulas (QBF), which is an extension of satisfiability (SAT) testing. This area has seen a lot of development in the past 20 years and we have been contributing to its theoretical foundations over the last decade. This includes defining the number of proof systems for QBF, defining a number of interesting formulas, looking at proving precise bounds on the size of the proofs, etc.
Can you tell us about your long association with IMSc?
The ongoing visit is at least the second academic generation of collaborations with IMSc. My first visit was 23 years ago when I was a young PhD student with Johannes Köbler at Humboldt University, Berlin. He has a long-standing collaboration with V Arvind from IMSc [retired theoretical computer science faculty and former Director] and still visits on a very regular basis. This was on graph isomorphism, an interesting problem in computational complexity that doesn't neatly fit into any one of the standard complexity classes. I vividly remember that both Johannes and Arvind involved their PhD students in the collaboration.
My next stage was at Leibniz University in Hannover with Heribert Vollmer who happened to have an [Indo-German] DAAD-DST project; there have been multiple iterations of this program over the years. He had a project with Meena on algebraic circuit complexity, and I was very happy to return to IMSc. It is one of the best exchanges that we’ve had, and quite fruitful in terms of publications that emerged. And this time something quite beautiful happened - I got Meena interested in proof complexity.
This wasn’t one of her research topics before, she is an expert in complexity and algorithms, in particular, algebraic complexity. At first, we started looking into algebraic aspects of proof complexity, in a specific class of proof systems called NC0 proof systems, where verification of proofs is done by very restricted resources. A couple of years later when I moved to the University of Leeds, we continued our collaboration, and I consider it one of my biggest successes that I got her interested in QBF proof complexity.
This is the third generation of my own PhD students that I have involved in the project, first from Leeds and now from the University of Jena. I don't exactly remember how many generations of PhD students I got to know at IMSc, but it was quite many. Meena is one of my most frequent collaborators, and it is great that our expertise is complementary. We not only meet in Chennai but regularly organize seminars together and meet in cities around the world. There is usually a series of visits where we discuss ideas and new directions, and try to get some work done, following it up when we return to our own institutions.
IMSc is a recurring home in my academic life. It is a very special place in having one of the best and largest theoretical computer science groups internationally. What I really appreciate is that IMSc seems like a haven for research where they focus on the right things.
What is your advice for young researchers?
I think it is good to be open-minded. I've been to a number of places - my career goes through Berlin, Hanover, Sapienza University in Rome, Leeds and Jena. I think it is good to see how things are done in different places and how different systems work, because you gain diverse perspectives. It is good to collaborate, to meet new people, and to introduce them to your research area and what you are doing. I have had a couple of changes of direction in what I have looked into and it was influenced by the people I met. You need to have your own agenda but also be open to listening to what other people have to say. I think that is quite important.
What other fun things are you involved in when you visit Chennai?
I didn't know much when I first came to India, but I have been quite fascinated about it culturally and historically ever since. While visiting Chennai in December, I’ve been to many Carnatic concerts during the music season and really enjoyed the music scene. I am quite into Western classical music and I find this parallel musical cosmos very interesting. It was striking at first, it felt like coming from the moon and seeing this other musical universe that is so rich and different. I find it interesting that rasikas are real experts in Carnatic music but may not know much about Western music, and vice versa for people trained in Western music. I have been to Kalakshetra several times and seen performances. India has fascinated me a lot culturally, I must say.
