Post-Doctoral Research Visit F/M Formal proofs for Machine Learning

Post-Doctoral Research Visit F/M Formal proofs for Machine Learning

Level of qualifications required : PhD or equivalent

Fonction : Post-Doctoral Research Visit

About the research centre or Inria department

The Inria University of Lille centre, created in 2008, employs 360 people including 305 scientists in 15 research teams. Recognised for its strong involvement in the socio-economic development of the Hauts-De-France region, theInria University of Lille centre pursues a close relationship with large companies and SMEs. By promoting synergies between researchers and industrialists, Inria participates in the transfer of skills and expertise in digital technologies and provides access to the best European and international research for the benefit of innovation and companies, particularly in the region.For more than 10 years, theInria University of Lille centre has been located at the heart of Lille's university and scientific ecosystem, as well as at the heart of Frenchtech, with a technology showroom based on Avenue de Bretagne in Lille, on the EuraTechnologies site of economic excellence dedicated to information and communication technologies (ICT)

Context

This is a postdoctoral position in the Scool team, which specializes in machine learning applied to sequential decision making. The position is funded by the Inria exploratory action FORMAL.

The goal of the postdoc is to formalize machine learning algorithms in the Lean theorem prover and eventually explore the use of AI to design algorithms and prove theoretical guarantees about them. The starting goal will be to formalize bandit algorithms.

Lean is a programming language and theorem proving assistant.
We can write programs in Lean, but also write theorems and proofs about those programs or any mathematical objects. Mathlib is the mathematical library of Lean. It contains most of the content of a Masters degree in mathematics, in particular many results of probability theory and analysis.
The obvious advantage of formal proofs is correctness: if the system accepts a proof, it is correct.
The real gain is however in what the certainty allows.
Since the computer checks the proofs, many people can work on a project without needing to trust each other.
Furthermore, once an algorithm and its proof are described in a formal language it becomes easier for a machine learning algorithm to interact with it, for example by generating new algorithms or proofs and getting feedback from Lean about their correctness.
Lean is therefore at the center of the recent efforts to use AI to assist in mathematical proofs.

Assignment

The goal of the postdoc project is to formalize machine learning algorithms in Lean, starting with bandit algorithms, as well as the tools needed to run them on simulated environments and prove their performance guarantees.
The result will be a library in which we have algorithms and a list of theorems stating that the implementation behaves as expected and providing performance guarantees on several tasks.
The code will be available on a public repository, and we will encourage external contributions.
The role of the postdoc will be to work on the project content itself, but also to generate interest from the community to increase the size of the team working on it.

Main activities

• Implement bandit algorithms in Lean
• Develop the tools needed to prove theoretical guarantees about them in Lean
• Manage a collaborative project: coordinate contributions, review pull requests
• Disseminate research results (publications, talks at conferences)

Skills

• Proficiency with Lean or a similar theorem prover
• Knowledge of the mathematical tools needed for machine learning theory, in particular probability theory.
• Ideally, knowledge of machine learning or even bandit algorithms.
• Scientific communication skills (speaking, writing). Proficiency in English.

A candidate who is proficient in Lean and knows basic probability theory, but not necessarily machine learning, would be preferred to a candidate with machine learning skills but without any Lean experience.

Benefits package

• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Theme/Domain :Optimization, machine learning and statistical methods

Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.

Instruction to apply

Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.

Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.

Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.