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.
Spreadsheet
Neglected catastrophic risks from AI
We've started a list of potential risks that would noticably and negatively affect most humans if they came to pass.
We consider a problem neglected if there isn't someone full-time focused solving it.
Mailing List
Community mailing list on Guaranteed Safe AI
We started a public google group mailing list dedicated to discussing AI architectures designed to have provable safety properties.
You can see past conversations or join directly
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.
Project
Specification IDE
We're prototyping a tool to show users with no formal methods experience could understand a formal specification; the tool maps subsections of that spec to natural language description and annotates the comparison
Whitepaper (2-pager)
The Opportunity for AI and FV
A nontechnical explanation of (1) why AI poses a cybersecurity risk, (2) the value and difficulties in deploying formal verification (FV), (3) how 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
At Atlas, Jason Gross developed a testbed to demonstrate that language models are sufficiently capable to convert from Coq proofs to Lean proofs by developing an verification tool to show that compiled Coq proofs and transpiled Lean proofs were equivalent to isomorphism.
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.