Projects
Community Building
We're advancing a new AI architecture that provides provable safety properties by constraining AI outputs with specifications. Advancing a new architecture requires increasing the number of people aware of and working on this architecture until it's a ubiquitous mechanism for assuring safety.
Jobs
Work Opportunities in Provable Safety Properties
We started a list of good ways for you to put your hard work towards Provable Safety Properties goals.
Check it out if you're looking for a role, and feel free to comment in the doc if you're hiring relevant for talent.
Note, this is separate from our jobs page.
Mailing List
Community mailing list on Guaranteed Safe AI
In collaboration with FAR AI, we started a public google group mailing list dedicated to discussing AI architectures designed to have provable safety properties.
We have new users request to join rather than enabling joining directly to prevent spammers, but we're very welcoming!
Events
Current and past events
See the events that we have and are looking forward to organizing or co-organizing!
If you'd like to organize something with us, please email us at [email protected]
Cyber
We think AI shouldn't be a black box to users, but instead should output a formal specification of solution properties as a reviewable intermediary result. The first step is building tools that (1) help users generate specifications for software, (2) generate programs from those specifications, and (3) generate proofs that the programs satisfy the specifications. Our early experiments are focused on understanding and describing the state-of-the-art research on the intersection of AI and formal methods, laying the foundations to build these tools.
Whitepaper (2-pager)
The Opportunity for AI and Formal Verification
A nontechnical explanation of (1) why AI is increasing the vulnerability of cyber physical infrastructure,
(2) the current difficulties in deploying formal verification, which is the highest standard for security robustness today,
(3) how recent and near-term advances in language models could overcome these limits, and
(4) next steps to advance the usage of formal verification.
Experiment
Porting Libraries Between Coq and Lean with ChatGPT
Making high-quality proof libraries takes a ton of work. It would be a shame to duplicate all that work for each ITP language, or to get locked out of using a specific ITP because it doesn't have the right libraries.
These experiments found that ChatGPT significantly reduced the work to (a) write a toy ISA model and example assembly programs in Coq (~400 SLOC), (b) translate these to Lean, (c) compare the Coq vs. Lean programs for semantic differences, and (d) port a Coq bugfix to Lean as an incremental patch.
Wireframe
Safely Generating Splitwise
Soon, AI will let anyone generate their own apps. Without strong safeguards, this will be a security nightmare: probabilistically-correct software is not a safe (or legal) way to handle payments, health data, or other risky tasks. Formalized code gen provides a safe alternative.
Report
AI Assisted FV Toolchain
Formally verifying software involves generating (a) the software itself, (b) a specification of how the software should behave, and (c) a mathematical proof that the software satisfies the specification.
Bio
To demonstrate that we can specify what "safe" means for general AI systems, we need to show we can generate new specification languages. Our initial work here will be advancing toxicity forecasting tools, which also enables the encoding of subjective preferences around toxicity into criteria that can be evaluated objectively.
Program Proposal (2-pager)
A competition for computational toxicity forecasting
This is a proposal to start a focused research organization (FRO) to assess AI tools for toxicity forecasting, analogous to the Critical Assessment of the Structure of Proteins (CASP), which became famous when AlphaFold "won" the "competition".
Get involved