This job has expired

Research Associates on Theorem Proving

Huawei Technologies Research & Development Ltd
Closing date
27 Jul 2021

View more

Technology & New Media
Contract Type
You need to sign in or create an account to save a job.

Job Details

About Huawei Research and Development UK Limited

Founded in 1987, Huawei is a leading global provider of information and communications technology (ICT) infrastructure and smart devices. We have more than 194,000 employees, and we operate in more than 170 countries and regions, serving more than three billion people around the world.

Our vision and mission is to bring digital to every person, home and organization for a fully connected, intelligent world. To this end, we will drive ubiquitous connectivity and promote equal access to networks; bring cloud and artificial intelligence to all four corners of the earth to provide superior computing power where you need it, when you need it; build digital platforms to help all industries and organizations become more agile, efficient, and dynamic; redefine user experience with AI, making it more personalized for people in all aspects of their life, whether they're at home, in the office, or on the go.

Huawei Research and Development UK Limited Overview

Huawei's vision is to enhance the lives of humanity and improve the environment by building a fully connected and intelligent world. Huawei has the largest Research and Development organisation in the world with 96,000+ employees in research centres around the globe. In the UK, we already have design centres in Cambridge, London, Edinburgh, Ipswich and Bristol. With a further £3bn of investment committed to the UK over the next 5 years we invite you to join us and drive your career forward.

Project Background

What is the nature of human reasoning and problem solving? How can machines exploit the known skills of problems solving to solve new problems automatically? Is it possible to work out general patterns of discovery and reasoning, such that machines can develop new methods and systems? We try to answer these problems and shrink the gap between machine learning and human wisdom.

Mathematical discovery and reasoning is considered the most creative activity of human wisdom. Mathematicians have been investigating the nature of human reasoning and problem solving since classical Greece. Even if the development of interactive theorem provers provides rigorous tools for people to formalise mathematics and to verify hardware and software designs, there is still a big gap between human reasoning and mechanical theorem proving: precious human intelligence is wasted on proving tedious and trivial lemmas, which are indispensable for machines to check the correctness and the integrity of a proof, but are quite obvious for well-educated mathematicians or computer scientists. Even worse, it is hard to recover the original intentions by reading these mechanical proofs.

During the first year of this project, we will focus on developing an automated theorem prover towards human reasoning. Except the automation of proof strategies and skills, the main planned innovation is: deriving theories automatically. We want to investigate and implement such a mechanism: to generate conjectures from cases, concepts, proofs, and known theorems, then produce automatically human readable and machine checkable proofs. We also plan to design and implement the mechanism to discover and exploit morphisms between algebraic structures, so as to simplify proofs by making use of abstract domains. It doesn't mean that we don't need human interference; on the contrary, we want to make use of human experience whenever possible --- machines will learn from humans when, for example, they are stuck, the computation diverges, the solution space is too big, and so on. We believe that human skills of problem solving will enable machines to think like us and to make plausible reasoning at the end.

Three full-time research associate (RA) positions on theoretical computer science, foundations of mathematics, and formal hardware verification, in Huawei R&D UK Ltd, have been released now. They are 12 month fixed term positions leading to permanent positions, subject to the funding, progress, and performance. Several summer internship positions are open as well. There will be a competitive salary and benefits package in line with top tier industrial R&D positions in UK.

Responsibility Description

RA is supposed to hold a PhD degree in theoretical computer science or pure mathematics. Research experience on constructing theorem provers, formal hardware verification, or mathematical logic is preferred. RA is required to have strong computer science background and has to be familiar with all branches of computer science in general. RA will be responsible for the design, implementation, testing, and release of the proposed automated theorem prover, and its applications in formalisation of mathematics and formal hardware verification. You will also be responsible for creating benchmarks, libraries, and improve the design and implementation of the tool. Publications on top conferences are strongly encouraged.

Professional Knowledge

RA is required to be familiar with the imperative programming languages like Python, the functional programming languages like Haskell, and the web programming languages like JavaScript. Experience of using theorem provers is necessary. The design and development experience of programming languages, theorem provers, or model checkers are preferred. Knowledge of recursive functions, Lambda calculus, formal logics, type theory, or category theory is preferred.

Business Skills

Excellent communication, learning, and writing skills.

Closing date

1st August 2021

Privacy Notice

Through applying for this position you agree to our privacy notice. For further details please follow the link:
You need to sign in or create an account to save a job.

Get job alerts

Create a job alert and receive personalised job recommendations straight to your inbox.

Create alert