PhD positions on the POSTMAN project in Prague ================================================ Czech Technical University in Prague, Czech Institute of Informatics, Robotics and Cybernetics Contact: Mikolas.Janota@gmail.com Website: http://people.ciirc.cvut.cz/~janotmik/postman Starting Salary: EUR 1800 - 2200 gross/month for 1,0 fte Job description =============== You will be working on the project POSTMAN (Powering SMT Solvers by Machine Learning). The project POSTMAN aims at a breakthrough in the field of Satisfiability Modulo Theories (SMT) by developing Machine Learning (ML) methods targeted at critical parts of SMT procedures. To solve real-world problems, many tools rely on SMT by translating the problems into a logic formulation and delegating their solution to a solver. SMT is thus at the heart of today's large verification toolchains, run continuously on thousands of CPUs by major software and hardware companies around the world. The project will advance SMT solving by developing ML methods that prune the search space of the solvers. Unlike the current search methods, ML allows taking into account a large number of observations made during the search. Guiding methods will be developed at various levels of abstraction, focusing on two critical problems in SMT: solving of quantified formulas and solving of sets of related formulas. The grand challenges for ML are to learn and represent abstract objects under semantic constraints and to employ interpretable learning in combination with reasoning. The expected outcome of the project is a range of new powerful methods combining ML techniques with current logic-based SMT approaches, providing a significant improvement over the state-of-the-art. The methods will be integrated in a number of systems and deployed in major SMT applications, benefiting large parts of today's formal methods. Topics of interest include: - machine learning procedures over large sets of benchmarks - methods that propose useful intermediate lemmas for long proofs - methods that efficiently apply learned knowledge during solving (e.g. quantifier instantiation, decision selection) - feedback loops between learning and automated reasoning - novel ML methods suitable in the considered context The work will include close collaboration with several international partners: Xerox PARC, University of Innsbruck, University of Miami, Radboud University Nijmegen, University of Lisbon, and others. Requirements ============ You should meet the following requirements: - A master's degree (or equivalent) in Computer Science, Mathematics or a related field, with a strong interest in Machine Learning, AI and/or Automated Reasoning; - Commitment and a cooperative attitude; - Proficiency in written and spoken English. You will enroll in the PhD program in Artificial Intelligence at CTU with an individual study plan. Research Environment ==================== The research will take place at the recently established Czech Institute of Informatics, Robotics, and Cybernetics (CIIRC) of the Czech Technical University (CTU) in Prague, which is with over 1700 members of academic staff one of the largest research institutions in the Czech Republic. CIIRC has been founded by CTU in July 2013 as a research and teaching institute and a center of excellence in the Czech Republic. CIIRC is the home of the Prague Automated Reasoning Group (http://arg.ciirc.cvut.cz/) - an international research group working on various aspects of Automated Reasoning, AI and Machine Learning, Formalization of Mathematics, and related fields. The group has a large and active network of collaborations around the world. The project POSTMAN, led by Mikolas Janota, is funded by the Czech ministry of education within the prestigious ERC CZ scheme. Prague is the capital of the Czech Republic, considered one of the most beautiful cities in the world and attracting millions of tourists every year. It has the highest Quality of Living Worldwide ranking among the eastern European cities and over 160,000 foreign residents. It boasts a rich history and culture, long tradition of university education and scientific research, and a dynamic economy. The cost of living in Prague is about one half of the living costs in Amsterdam, Paris or Munich. Application =========== Inquiries and applications should be sent via email to Mikolas.Janota@gmail.com with "POSTMAN PhD" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, including the names of two references. Deadlines: Until the positions are filled. Earlier applications are welcome and early start date is an advantage.