[Om-announce] PhD positions on the AI4REASON project in Prague

[Josef Urban]

PhD positions on the AI4REASON project in Prague
================================================

Czech Technical University in Prague,
Czech Institute of Informatics, Robotics and Cybernetics
Contact: Josef.Urban at gmail.com

Starting Salary: EUR 1,200 gross/month for 1,0 fte

Job description
===============

You will be working on the ERC project AI4REASON (http://ai4reason.org).
The project's goal is to develop new combinations of AI, Machine Learning
and Theorem Proving methods that learn reasoning guidance from large proof
corpora and use such guidance to steer the automated reasoning processes at
various levels of granularity.  Our motivation is to (i) facilitate
automated computer encoding, understanding and large-scale verification of
mathematics, science, software and hardware designs, and to (ii) research
AI methods that combine learning and reasoning over large repositories of
complex mathematical knowledge, getting closer to human-level scientific
thinking.

Topics of interest include:
- machine learning procedures over large proof libraries
- methods that propose useful intermediate lemmas for long proofs
- methods that efficiently apply learned knowledge in proof search
- feedback loops between learning and automated reasoning
- statistical and deductive methods for automated formalization of informal
mathematics
- learning from aligned informal, semiformal and formal corpora

The work will include close collaboration with several international
partners: University of Innsbruck, Google Research, University of Miami,
Radboud University Nijmegen 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 AI4REASON project
led by Josef Urban is funded by the European Research Council (ERC) which
targets highest-quality investigator-driven frontier research in Europe (
https://erc.europa.eu/about-erc/mission).

Prague is the capital of the Czech Republic, considered one 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 Josef.Urban at gmail.com
with "AI4REASON 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: March 1, 2017, or until the positions are filled. Earlier
applications are welcome and and early start date is an advantage.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://openmath.org/pipermail/om-announce/attachments/20161211/fdf4fe98/attachment.html>