Atlas Computing updates

[Evan Miyazono]

Hello Atlas community!

At some point in the last few months, you asked me for updates of some form. Here's a pretty distilled update.  Feel free to reply to me with questions or book time to chat.

What we've been up to:

Mostly fundraising, planning, writing, and building a network of relevant contacts (which now includes you!)

• We're popularizing "provable safety properties" as a new+complementary approach to AI risk
  
• Overall message is: AI can have quantitative safety guarantees in scoped domains like other types of engineering; if we show those products are easy and rewarding to build, we can direct R&D attention on asymmetrically defensive capabilities rather than risky ones.
  
• Then we can fill in the gap between domains, rather than aiming for alignment in one fell swoop.
  
• We've made a few documents to explain this to different audiences
  
• pitch deck (for potential donors)
  
• 2-pager on overall strategy (general public)
  
• domain 1: draft 2-pager on AI for scaling formal verification (for policymakers)
  
• milestones doc (for experts and policy advisors) of indicators that would unlock more interest in using AI for formal verification
  
• domain 2: FRO proposal on AI for toxicity forecasting (for Convergent Research) - this one is pretty much on the back burner for another month or two
  
• We've found individuals at SRI, AWS, DHS, DOE, NSA, and DARPA who support using AI to scale formal verification - main limit sounds like a talent bottleneck, so we're working to figure out how to widen that
  
• We've organized small workshops on boundaries & provable safety properties
  
• We set up an email list that's been delightfully active in connecting AI news with verifiable safety guarantees. Messages are public, but we require approval to post in order to limit spam, but it's pretty rubber-stamp approval.
  

Intended impact:

• We've got clear plans (annual & quarterly OKRs and a gantt chart)
  
• Our top goals for the year are:
  
• organize a 200 person conference on AI architectures with provable safety properties
  
• convince ≥1 relevant gov official to grow the talent pipeline of researchers in AI x formal verification
  
• convince NIST that provable safety properties are an important architecture to add to the portfolio of approaches
  
• secure funding & recruit a lead for the toxicity forecasting competition
  

Fundraising: 

• $800k in-flight in speculation grants from SFF
  
• that covers through Eo2024 with growth, or Eo2025 without growth (forecasted budget, org chart)
  
• I'd like to raise $1.7-2.7M more to cover Eo2025 with growth
  
• The next S-Process round hasn't been announced yet (though there'll be a separate funding effort)
  
• Banyan Collective contributed a combined $15k
  
• I'm in conversations with endowed foundations, but most will be funding through grant programs, so I'm applying to lots of grants
  
• ACX grants contributed $40k to the boundaries workshop I co-organized for regranting
  

Desired help:

• I'd really like to grow the team, and that means I'd love intros to potential donors.
  
• We're on Open Collective, but please reach out directly if you or someone you know would like to make larger contributions (feel free to forward this email if helpful)
  
• Let me know if you can intro me to people working on AI at NIST or formal verification NSF
  

Get involved (recap of the above):

• join the discussion mailing list here
  
• email Daniel (cc'd) and me if
  
• you'd like to take on an independent hobby project (like building a thing, or volunteering to organize a community call)
  
• there are things you think I/we should be doing (engaging communities, speaking to people)
  
• there are people you think we should be talking to

Hope you're doing well; thanks for making it this far.

To the future!

   - Evan

p.s. definitely considered starting this email pretending to be SupremecyAGI before deciding that was a horrible note to start on

P.p.s. What I've been reading: Finally got to and quickly finished the Jean le Flambeur series - very compelling world-building in a future where most human upload is common with a delightful amount of physics and game theory wrapped in a fun series of heist stories.  The main character's womanizer-y inclination led to a few eye-rolls though.  Definitely between Accelerando (Stross) and Diaspora (Egan) on that scale, though.  Multiple scales, in fact