Marijn Heule
Office 9107 Gates and Hillman Centers
Email marijn@cmu.edu
Department
Computer Science Department
Administrative Support Person
Tracy Farbacher
Research Interests
Formal Methods
Pure and Applied Logic
Advisees
Cayden Codel
Joseph Reeves
Bernardo Anibal Subercaseaux Roa
Emre Yolcu
James Gallicchio
Research/Teaching Statement
My research focuses on solving hard problems automatically with having high confidence in the results. While humans are great at many aspects of problem solving, we are no match for computers in a range of ways, including precise logical reasoning. Such reasoning is crucial in industry and academia, for instance to ensure that computer systems work exactly as intended, in fields ranging from health care to finance to aviation. The main themes of my research are described below.
Trusted Computing. Fully automated reasoning tools are frequently used in industry to determine the presence or absence of bugs in hardware or software and in academia to solve long-standing open problems. Yet these tools are often highly complex, which raises the question of whether we can trust their results. This question is particularly important when such tools are used to determine the correctness of safety-critical systems. Here, correctness means that there exists no input that violates the safety requirements. I have been working on developing proof systems that can compactly express that the entire search space has been explored and, in addition, on efficient, formally-verified tools to validate statements in these proof systems.
Reasoning and Understanding. Human proofs and computer-generated proofs differ in many aspects. An argument often heard is that human proofs provide us with understanding whereas computer-generated proofs merely show the correctness of a statement. While there is some truth to this argument, it is also true that modern proof-checking tools can actually provide us with many important insights into the nature of a problem. Ultimately, I aim to transform computer-generated proofs into humanly understandable arguments. Such arguments could provide us with insights into how problems have been solved, which in turn could allow mathematicians to construct smaller proofs.
Strong Proof Systems. Automated reasoning can fail miserably on seemingly easy problems due to the weakness of commonly used proof systems that do not support reasoning at a high level of abstraction. To deal with this issue, I have been developing new proof systems that not only generalize strong existing proof systems, but that are also well suited for mechanization. There exist short arguments in these proof systems for many well-known problems that are hard for existing automated-reasoning approaches. The key to solving problems that require some form of abstract reasoning is not the ability to simulate human thinking, but rather to equip the machine with appropriate reasoning capabilities to find its own short arguments.
Representing Problems. A common approach in automated reasoning is to translate a given application instance into propositional logic and then solve the resulting formula with a dedicated solver. Since the quality of the translation has a big impact on the solver performance, it is no coincidence that solvers are highly successful in the field of hardware verification: digital electronic circuits have a direct translation to propositional logic which is often adequate for solving. However, the same is not true for many other applications. I have been studying how to automatically fix translations so that non-experts can achieve strong solver performance on their applications.
Reasoning in the Cloud. Supercomputers offer enormous potential to solve hard reasoning problems. However, to capitalize on this potential, we need to find ways to distribute computation evenly over many different cores, which is far from trivial. I have been working on a new parallel solving paradigm, called Cube-and-Conquer, that has been successful in realizing this goal for some long-standing open problems in mathematics. I envision a future in which automated reasoning will be a cloud service to solve both easy and hard problems. This service will not only be able to answer many important questions in industry and academia; it will also allow external validation of enormous proofs and provide explanations that help us understand its results.