Atlas Computing updates: starting Q2
Evan Miyazono
Hello Atlas community,
Here’s our a quick update (since our late Q1 update posted in March):
Project updates
Most exciting: Feels like things are starting to heat up. There seems to be appetite for large-scale, well-funded coordinated efforts to dramatically accelerate (1) hardware compute governance, (2) formal verification of software with AI, and even a little preliminary interest in (3) formalizing non-software policies to ensure AI systems follow rules. As a result, we’re building up proposals that either we at Atlas or other experts could pursue, for instance, contributing to Convergent Research’s new bottlenecks roadmap.
Events: We just organized the Guaranteed Safe AI Summit - a meeting of about 40 experts from research, industry, and philanthropies interested in advancing this architecture for AI with quantifiable safety properties. There are a few small wins, and hopefully a large collaboration that will get started as a result of it. And we’ll likely organize a follow-up in ~6 months, so please let me know if you’re working on GSAI and would like to participate.
Growth:
We’ve spun out Jason Gross early to pursue moonshot autoformalization projects. We’re excited to share more information soon on how to follow his new efforts!
We’re excited to have Alexandre Rademaker joining us part-time to help on the Formal Spec IDE. Shaowei Lin is also re-joining briefly, part time (now that he’s left Topos Institute) and will also be working on the SpecIDE project. This is now growing to include a collaboration with the Beneficial AI Foundation; we'll provide specification generation and validation (ensuring your spec is correct) for their verification (ensuring the code meets the spec) efforts.
Focus:
We’re going to be ramping up our formal specification validation work in partnership with an as-yet-unannounced collaborator. I’d recommend following blog.atlascomputing.org/ for more frequent updates than quarterly! We’ve also started writing monthly updates on the Specification IDE project for Schmidt Sciences here. And if you want to see a 4-slide explanation of the project, look here.
Travel updates
Upcoming events: catch us in person or let us know if we should meet anyone
We were previously looking into organizing an event next to ICSE to bring together people near the intersection of formal methods and AI. We ended up deciding to postpone it so we can organize something bigger; feel free to email me if you would like to know when we’ve set a date.
Anyway, thanks for reading!
- Evan