Expert on formal verification
In a nutshell: Formal verification — using formal methods of mathematics to prove (or disprove) whether algorithms will do what they’re intended to do — could be an important tool for the safe deployment of AI (and potentially for addressing other pressing problems). While we haven’t looked into formal verification much, further research in this area and applying existing techniques to important issues both seem potentially promising to us.
Sometimes recommended — under-researched
This career is potentially high-impact, but we haven't yet researched it enough to recommend it confidently.
Review status
Based on a shallow investigation
We’ve interviewed several people with relevant expertise about this path and spent at least half a day reading the best existing advice (or similar). The purpose of these profiles is to help our readers prioritise further investigation -- our conclusions do not represent fully considered views.
Why might becoming an expert in formal verification be high impact?
‘Proof assistants’ are programs used to formally verify that computer systems have various properties — for example, that they are secure against certain cyberattacks — and to help develop programs that are formally verifiable in this way.
Currently, proof assistants are not well-developed, but the ability to create programs that can be formally verified to have important properties seems like it could be helpful for addressing a variety of issues, perhaps including AI safety and cybersecurity. So improving proof assistants seems like it could be very high value.
For example, we might eventually be able to use proof assistants to generate programs for solving some parts of the AI alignment problem. This would require us to be able to correctly formally specify the sub-problems, for which training in formal verification is plausibly useful.
We haven’t looked into formal verification much, and although it seems potentially promising to us, you can see some pushback to this idea in this thread and this writeup of the path.
You can enter this career path by studying formal verification at the undergraduate or graduate level, or learning about it independently if you have a background in computer science. Jobs in this area exist both in industry and in academia.
Want one-on-one advice on pursuing this path?
If you think this path might be a great option for you, but you need help deciding or thinking about what to do next, our team might be able to help.
We can help you compare options, make connections, and possibly even help you find jobs or funding opportunities.
Learn more
- High Impact Careers in Formal Verification: Artificial Intelligence
- Podcast: Nova DasSarma on why information security may be critical to the safe development of AI systems
Read next: Learn about other high-impact careers
Want to consider more paths? See our list of the highest-impact career paths according to our research.