NB. This call is already closed.
NB. There is another researcher call that we are currently advertising. The current call may be closed early if we have a good candidate for this other call.
ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD) invites applications for a postdoc researcher. We aim to develop a comprehensive set of techniques for proving the safety of automated driving. Its core consists of a custom-made program logic and its proof checker; however, elements outside conventional theorem proving studies will be pursued, too, such as heuristics for proof discoveries, implementation of safety proofs in automated driving cars, studying the roles of safety proofs in explainability and social acceptance of automated driving, etc. The position is highly recommended for theorem proving researchers who wish to apply their expertise to a hot application domain (namely automated driving), and furthermore, obtain novel theoretical insights in return from the real-world application. The commercialization of the research output is also planned, with the founding of a spin-off startup (cf. our call for a scientific programmer).
JOB DESCRIPTION
The candidate will work at National Institute of Informatics, Tokyo, Japan, on the logical foundations for mathematical proofs of automated driving safety. The research is largely that of automated/interactive theorem proving, but with a distinctively expanded focus that is required by the complex nature of the application. We will tackle the practical challenges we describe in the paragraphs below, which we believe are highly rewarding theoretically and scientifically, too. The practical challenges below are general and foundational, ones that we will encounter anyway when we aim to use theorem proving as an effective means of quality assurance, safety explanation, and social acceptance of real-world autonomous systems.
One challenge in theorem proving for automated driving safety is the difficulty of modeling. Cars are complex systems with hundreds of chips and millions of LoC; automated driving cars are equipped with statistical machine learning components (neural networks) for object recognition and other purposes; furthermore, their physical environments—weather, road condition, behaviors of other cars and pedestrians, etc.—are complex and unpredictable. All these point to the fact that a complete logical white-box modeling, one that would enable theorem proving on top of it, is all but impossible in the case of automated driving safety.
Another challenge is to identify the relevance of “safety proofs” in the broader context of quality assurance. It is widely acknowledged that quality assurance of real-world autonomous systems is a never-ending effort. Since such systems have both internal uncertainties (such as the behaviors of neural networks) and external ones (such as unexpected operation scenarios), we have to continuously monitor the systems’ operation, find unexpected failures, fix the systems and update the safety cases. This dynamic and iterative nature of quality assurance does not sit well with the conventional view of mathematical theorems that is static and one-shot.
Yet another challenge is cost-effectiveness. Compared to the aerospace industry, the automotive industry tends to be more cost-sensitive, with model cycles imposing tighter limits on development costs. This requires our theorem proving techniques to be cost-effective, in terms of the amount of effort for proofs as well as the expertise required of proof engineers. Therefore we will work on proof automation by search heuristics and user interface, too. That the target systems exhibit hybrid dynamics poses unique research opportunites here.
To tackle the challenges above, we have been working on the basis of the RSS methodology (see Mobileye’s intro; the original paper; a logical introduction), which we find to be a very good answer to the question of what to model, and what not to model. Our recent paper introduces a formal logic for RSS safety proofs (Hasuo et al., IEEE Trans. Intell. Vehicles, 2022; its arXiv version). It is heavily inspired by Platzer’s differential dynamic logic. Here (EN/JP) is an introduction video to the paper. The candidate’s work will be based on this recent paper.
The candidate will work closely with Prof. Ichiro Hasuo and a few other team members. It is possible that the candidate be granted an academic title (such as Project Assistant/Associate Professor).
ESSENTIAL SKILLS AND REQUIREMENTS
- Motivated, dedicated, and able to work both independently and collaboratively
- Proven publication record
- Familiarity with formal logic and deductive verification
- Experience in using an interactive theorem prover
- Eagerness to bridge theoretical research and real-world problems
- PhD degree (or be close to completion)
- Courage to learn and experiment with new techniques (Some theoreticians cannot stand the unpredictability of running experiments and waiting for their results)
- Eagerness and experience in collaborative theoretical research
- Must be able to communicate and work well with other team members
- Fluency in English, both orally and in paper writing
DESIRABLE SKILLS
The following skills are not at all mandatory. They however will be a plus
- Experience in hybrid system research
- Experience in implementing theorem provers
- Experience in functional programming
- (Japanese language skills will be useful for everyday life, but not mandatory at all)
PRACTICAL
- This call was posted in October 2022. It will remain open until the position is filled.
(There is another researcher call that we are currently advertising. The current call may be closed early if we have a good candidate for this other call.) - Annual gross salary: JPY 4,260,000 — 7,368,000 yearly, gross (depends on qualifications and experience).
- The contract is initially until the end of a fiscal year (March 31), with the possibility of extension (maximum until the project ends in March 2025).
- Our admin staff will provide support for moving, visa application, etc.
- Starting date: as early as possible
- Location: Tokyo, Japan (remote work from abroad is not allowed)
APPLICATIONS AND INQUIRIES
Applications should be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Application (Automated Driving).” Please include
- your brief CV,
- short description of research interests (can be very informal and short),
- the list of papers (a dblp or Google scholar link will do, for example),
- a couple of representative papers (in pdf), and
- (preferably) the contact of two references.
We will contact you for further material, provided that we find sufficient relevance in your application.
Inquiries should also be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Inquiry (Automated Driving).”
LIVING AND WORKING IN TOKYO
We have employed 10+ researchers and scientific programmers from abroad–see our list of members/former members. We have ample experience in supporting them in coming to and living in Tokyo.
PRICES
Tokyo is not an expensive city. On actual prices and availabilities you will find a lot of information sources on the web (including this). Some sample prices:
- An studio apartment, 30m2, 30min door-to-door to our Tokyo site: JPY 80,000 / month
- A 2-bedroom apartment, 40m2, 20min door-to-door to our Tokyo site: JPY 130,000 / month
- A 15-min metro ride: JPY 200
- A quick (but nice) Japanese set meal: JPY 600-1000
- An exquisite sushi set meal (which even locals rarely have 🙂 ): JPY 30,000
- A pint of beer: JPY 800
APARTMENTS
You can easily find an apartment using the following websites: www.sabbaticalhomes.com, www.sakura-house.com/en, gaijinpot.com, and others.
LANGUAGE
The working environment is totally in English, with more than half of the team coming from abroad. Japanese language skills will help everyday life, but one can definitely live without them, as we know from our colleagues’ experience.