Description du poste
This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. Here I set the stage for a panel I’ll moderate at MIT, on the potential for formal verification to defend against a set of related cybersecurity risks from highly capable AI.
This week, I want to announce a panel I’m moderating at MIT. It’s on the subject of how formal verification can help against cybersecurity threats by increasingly powerful AI systems. It will take place on Tuesday, November 17th, at 4:30 PM, followed by a 5:30 PM reception, in MIT room 32-155.
This event is run by our College of Computing, and please visit their web page for the event if you would like to register for free. Registration, open to the public, is only for in-person participation. There is no livestreaming online, though we will record the panel and post a video online, not too long after the event.
The Panel and the PanelistsWorry is growing around AI agents escaping containment and acting against the interests of the organizations that built them. The latest LLMs are also finding cybersecurity vulnerabilities in important software at an alarming pace. This panel surveys an old computer-science technique with new promise: formal verification, mathematical proof about the behavior of programs. Can such proofs be applied to important computing infrastructure, to guarantee agent containment and find all security bugs of certain kinds, future-proofing against more-powerful LLMs? Our discussion brings together experts on the topic from across academia, government, and industry. We hope to hit on topics of interest both to experts in this technical field and to a broader audience concerned with policy and other strategic questions.
Our panelists:
Byron Cook started his journey through formal verification with PhD work in formalizing the interface between CPUs and software. He then worked for many years at Microsof