Email Gateway (Jun 19 2021 at 10:42): Email Gateway (Jun 19 2021 at 10:42):From: David Aspinall <David.Aspinall@ed.ac.uk>
Verification #
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.
We will soon open the following positions for this project. There will
be a competitive salary and benefits package in line with top tier
industrial R&D positions in UK.
Work Location: Edinburgh UK
Two Full-Time Research Associates on Theoretical Computer Science. RA
is supposed to hold a PhD degree. RA is required to have strong computer
science background and has to be familiar with all branches of computer
science in general. Research experience of formal verification, theorem
provers, machine learning, programming languages, or compilers is
necessary. RA will be responsible for the design and implementation of
the proposed automated theorem prover, and its applications in automated
formal verification of hardware and software designs.
A Full-Time Senior Software Engineer. SE is supposed to hold a BSc or
MSc degree. SE 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. The
development experience of programming languages is preferred. SE is
responsible for the implementation, testing, and release of the proposed
automated theorem prover.
Also, we are recruiting interns on mathematics or computer science. We
hope you can help create benchmarks or libraries, and improve the design
and implementation of the tool. You are required to have a strong
mathematical background. Basic programming skills of Haskell and Python
are necessary. Knowledge of recursive functions, Lambda calculus, formal
logics, type theory, or category theory is preferred.
You are very welcome to join us on this ambitious exploration journey.
Informal enquiries on details of the project and these positions can be
made to:
Dr. Wei Chen
weichen8@huawei.com
Research Scientist on Theoretical Computer Science
Hisilicon Advanced Research Department
Huawei Edinburgh Research Centre
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Last updated: Apr 18 2024 at 16:19 UTC