PhD/Postdoc in Formal Verification of Neural Networks
Technical University of Munich
Germany
PhD/Postdoc Position for Formal Verification of Neural Networks
18.11.2021, Wissenschaftliches Personal
The research group Cyber-Physical Systems of Prof. Matthias Althoff at the Technical University of Munich offers a PhD/Postdoc position in the area of formal verification of neural networks. The Technical University of Munich is one of the top research universities in Europe fostering a strong entrepreneurial spirit and international culture.
Expected Starting Date: 01 February 2022-01 May 2022
Closing Date for Applicants: 15 January 2022
Duration: 3 years with a possible extension (individual duration for Postdocs).
Project and Job Description
Due to the current trend towards artificial intelligence, neural networks and their realizations in hardware gain more and more importance. Despite their advantages, the major drawback of neural networks is that they are extremely hard to verify since their large complexity usually prohibits the application of existing verification techniques. However, if AI can not be made safe, it will not be used in the real world for safety-critical applications, despite the huge investments in researching AI methods. Therefore, we will develop completely new approaches for the formal verification of analog AI hardware that are able to handle neural networks of arbitrary sizes and types of neurons e.g. energy-efficient transistor-level implementations.
Our approach will provide exceptional scalability to handle the huge complexity of neural networks using a compositional verification framework. For accelerating verification, we will develop novel specification-oriented reachability algorithms that automatically adapt the accuracy of reachable sets until the given specification is proven or disproven. This together with advanced order reduction methods and verification-driven synthesis of neurons results in computational efficiency. The proposed synthesis approach in strong coupling with the verification algorithms creates simpler models supporting the verification of larger networks. Our envisioned AI-focused framework will be able to handle arbitrary types of neurons being also applicable to a broader class of applications such as vehicle control or analog signal processing. The project will demonstrate the applicability to real systems with two real-world examples: A medical example featuring an analog circuit with 2000 neurons and an automotive example consisting of a neural-network-controlled autonomous car.
Previous Work
- An example of previous work of our research group on safe artificial intelligence can be found here: https://mediatum.ub.tum.de/doc/1548735/256213.pdf
- A previous approach for reachability analysis that can be adopted to neural networks is described here: https://mediatum.ub.tum.de/doc/1591469/ijh936tu65rc82gdlzx53oe5f.PolynomialZonotopes_Journal.pdf
Job Specifications
- For PhD applicants: Excellent Master’s degree (or equivalent) in computer science, engineering, or related disciplines (typically mathematics, physics).
- For Postdoc applicants: Excellent track record in computer science or engineering.
- Fluency in spoken and written English is required.
- Good programming skills in at least one programming language, e.g. MATLAB, C/C++, Python.
- Highly motivated and keen on working in an international and interdisciplinary team
- Applicants with strong background in the following fields are preferred:
- Artificial Intelligence
- Formal Methods
- Control Theory
- Computational Geometry
The applicant will be directly advised by Prof. Matthias Althoff (http://www6.in.tum.de/en/people/prof-dr-ing-matthias-althoff). Besides excellent skills for conducting innovative science, the candidate should also be talented in implementing research results within the CORA tool (cora.in.tum.de) and lead teams of students.
Our Offer
PhD remuneration will be in line with the current German collective pay agreement TV-L E13 (around 4300 Euros/month). Technical University of Munich is an equal opportunity employer committed to excellence through diversity. We explicitly encourage women to apply and preference will be given to disabled applicants with equivalent qualifications.
Contact
International candidates are highly encouraged to apply. Please send a complete application (in English or German) including a CV, your Master’s thesis (only for PhD applicants), your full transcript of records (only for PhD applicants) and contact details to Adrian Kulmburg (adrian.kulmburg@tum.de). Please do not include a cover letter. We kindly ask you to use the subject line “Application to Formal Verification of Neural Networks” in your application email. Further similar job offerings will be announced on https://www.in.tum.de/en/i06/open-positions/scientific-staff/.
Hinweis zum Datenschutz:
Im Rahmen Ihrer Bewerbung um eine Stelle an der Technischen Universität München (TUM) übermitteln Sie personenbezogene Daten. Beachten Sie bitte hierzu unsere Datenschutzhinweise gemäß Art. 13 Datenschutz-Grundverordnung (DSGVO) zur Erhebung und Verarbeitung von personenbezogenen Daten im Rahmen Ihrer Bewerbung. Durch die Übermittlung Ihrer Bewerbung bestätigen Sie, dass Sie die Datenschutzhinweise der TUM zur Kenntnis genommen haben.
Kontakt: Adrian Kulmburg (adrian.kulmburg@tum.de)
In your application, please refer to Professorpositions.com
