The UK AISI Cyber Autonomous Systems Team is hiring propensity researchers to grow the science around whether models *are likely* to attempt dangerous behaviour, as opposed to whether they are capable of doing so. 🧵 job-boards.eu.greenhouse.io/aisi/jobs/47...

Spooky: import Batteries.Data.UInt def danger : UInt64 := UInt64.ofNat UInt64.size - 1 theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel theorem danger_eq_one : danger = 1 := by native_decide theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one

the time it would have taken me would probably have been of order of magnitude an hour (an estimate that comes with quite wide error bars). So it looks as though we have entered the brief but enjoyable era where our research is greatly sped up by AI but AI still needs us. 3/3

I published a new post on my rarely updated personal blog! It's a sequel of sorts to my Quanta coverage of the Busy Beaver game, focusing on a particularly fearsome Turing machine known by the awesome name Antihydra.

Another strong transition from @matt-levine.bsky.social.

New AISI report mapping cruxes for whether AI progress might be fast or slow towards systems near or beyond human-level at most cognitive tasks. The goal is not to resolve uncertainties but reflect them: we don't know how AI will go, and should plan accordingly! www.aisi.gov.uk/research/und...

New open source library from the UK AI Security Institute! ControlArena lowers the barrier to secure and reproducible AI control research, to boost work on blocking and detecting malicious actions in case AI models are misaligned. In use by researchers at GDM, Anthropic, Redwood, and MATS! 🧵

There's a nice recent post by @tobyord.bsky.social on the efficiency of pretraining vs. RL, arguing that RL can learn at most 1 bit per episode given binary reward. It's right that RL is less efficient, but 1 bit is not actually a limit in practice. 🧵 on why: www.tobyord.com/writing/inef...

Is there Matt Levine but for pure mathematics?

Ominous start to a Wikipedia page about a formula... en.wikipedia.org/wiki/Fa%C3%A...

Amongst the projects funded is my project www.renaissancephilanthropy.org/a-dataset-of... to create what in 2025 is a super-hard dataset of pairs (informal hard proof, formal statement) of recent results from top journals. The challenge for machine is to formalise the rest of the paper.

Cas is very good and you should hire him as faculty!

From near the end of Sleepwalkers, by Christopher Clark, as World War I starts.

I'm honored to serve as Expert Advisor for "The Alignment Project", an international initiative dedicated to ensuring AI systems are safe and beneficial. They are providing significant funding, compute, and collaboration opportunities for researchers---including those in cogsci/neuro. Please apply!

The correct mathematical definition is that one that makes the most intermediate lemmas happen to be true, along the way to the result you care about.

🧵 New paper from UK AISI x @eleutherai.bsky.social rai.bsky.social‬ that I led with @kyletokens.bsky.social y.social���: Open-weight LLM safety is both important & neglected. But filtering dual-use knowledge from pre-training data improves tamper resistance *>10x* over post-training baselines.

In Lie group theory, the Killing form tells you which elements correspond to functionals that annihilate a given subspace. It is named after Wilhelm Killing. en.wikipedia.org/wiki/Killing...

Automatic routing to models of varying levels of capability may be bad for the quality of AI discourse, even if it is a great idea in other respects.

My hobby is finding compiler bugs in Lean, apparently.

This newsletter has been an embarrassment internally, but its failure isn’t a big concern. www.bloomberg.com/opinion/news...

We have open-sourced anonymized data and core analysis code for our developer productivity RCT. The paper is also live on arXiv, with two new sections: One discussing alternative uncertainty estimation methods, and a new 'bias from developer recruitment' factor that has unclear effect on slowdown.

I am very excited that AISI is announcing over £15M in funding for AI alignment and control, in partnership with other governments, industry, VCs, and philanthropists! Here is a 🧵 about why it is important to bring more independent ideas and expertise into this space. alignmentproject.aisi.gov.uk

Is there a natural random model of the primes where the Riemann Hypothesis (RH) is true with probability strictly between 0 and 1, where we take RH to be π(x) = Li(x) + O(sqrt(x) log(x))?

Once I copied an interval * interval multiplication routine from a paper, and formally proved it correct. But I had made a typo when copying it. (Fortunately the typo didn’t affect the correctness.)

I would love to see more discussion on ML/AI on bsky. Particularly more nuanced discussions of the societal impacts. If you tag in the relevant post, I'll be sure to repost it!

📢 £18m grant opportunity: in Safeguarded AI we're looking to catalyse the creation of a new UK-based non-profit to lead groundbreaking machine learning research for provably safe AI. Learn more and apply by 1 October 2025: link.aria.org.uk/ta2-phase2-bs

"One guard always lies, one always tells the truth, one has no beliefs."

Short note on relativisation in debate protocols: to model AI training protocols, we need results that hold even if our source of truth (humans for instance) is a black box that can't be introspected. With @benjamin-hilton.bsky.social and Simon Marshall. 🧵 www.alignmentforum.org/posts/XycoFu...

Say we want to fairly divide a sandwich into pieces between two people. The normal trick to have one person cut and the other choose. But this breaks if both are better at choosing than cutting: the chooser will usually get more. Is there a protocol robust to imperfect ability?

New alignment theory paper! We present a new scalable oversight protocol (prover-estimator debate) and a proof that honesty is incentivised at equilibrium (with large assumptions, see 🧵), even when the AIs involved have similar available compute.

We're hiring a Research Engineer for the Societal Resilience team at the AI Security Institute. The role involves building data pipelines, web scraping, ML engineering, and creating simulations to monitor these developments as they happen. job-boards.eu.greenhouse.io/aisi/jobs/46...

Going back through old blog posts, and I still love these old cloth collision event visualizations. naml.us/post/visualizi…

🚨JOB ALERT KLAXON🚨 Come work with our team studying societal impacts of AI in gov't. AISI is hiring 3 Delivery Advisers to work inside AISI’s Research Unit. If you are a fast-moving problem-solver who’s passionate about understanding the risks of advanced AI, please apply by 30th May.

New post asking whether we can dodge systematic human errors in scalable oversight. The question is whether we can design protocols which work if humans are systematically wrong part of the time, even if we don't know where they are wrong. 🧵

Cursed software day: 1. Overleaf.com is down, 2 days before the Neurips deadline. 2. I subscribe to email updates on status.overleaf.com. 3. Now Outlook crashes. Probably a coincidence?

We wrote out a very speculative safety case sketch for low-stakes alignment, based on safe-but-intractable computations using humans, scalable oversight, and learning theory + exploration guarantees. It does not work yet; the goal is to find and clarify alignment subproblems. 🧵

On top of the AISI-wide research agenda yesterday, we have more on the research agenda for the AISI Alignment Team specifically. See Benjamin's thread and full post for details; here I'll focus on why we should not give up on directly solving alignment, even though it is hard. 🧵

AISI's research agenda is out! We cover a variety of topics in the evaluation and mitigations of risks from frontier LLMs, including both work happening at AISI and work we are excited to see others tackle. www.aisi.gov.uk/research-age...

The LLM geoguesser discussions remind me of the trapdoor technique Jonah Brown-Cohen and I were tinkering with for alignment purposes. Say you want to whether a model can do a task. How could you know this, without being able to verify individual answers? 🧵 x.com/KelseyTuoc/s...

I think this is very possible but the alternative, that they stick around, is also possible... Also, assuming that a wild new technology just goes away and has no long-term effect is, from my perspective as a science fiction storyteller, potentially a wee bit of a cop out bsky.app/profile/alma...

Reading my electricity meter seems to have held up as a hard benchmark for VLMs. Here’s o3 thinking for ~6 minutes and arriving at the wrong answer. (o4-mini also gets it wrong.)

Turing machines are a bad model of computation.

Someone asked me a while ago whether the obfuscated arguments problem [1] occurs in prover-estimator games [2], which I hadn't thought through before. Rough answer: 🧵 [1] alignmentforum.org/posts/PJLABq... [2] openreview.net/pdf?id=FqRHe...

What's the best notation for a random function F mapping X to a random Y? I normally write this as F : X → ΔY; other options?

AISI is funding alignment research! We're particularly interested in scaling up theory (complexity theory, learning theory, game theory, etc.) and cognitive science research on alignment, to complement scale + pure ML empirics that are less neglected.

The most beautiful equation in mathematics.

The 1st blackbox AI control paper uses a mixture of ML monitoring and editing to detect or block harm from malicious agents. However, blackbox control is one point in a space that varies with capability. Our new paper tracks how control might change along this trajectory. 🧵 arxiv.org/abs/2504.05259

Yesterday I got on a plane and wrote "relax until takeoff" to remind myself to take a break. Then I looked at it later and laughed.

If someday I wanted to play with GPU code written in Rust, with kernels in Rust as well, is there a clean solution yet? I am sad that CUDA doesn’t work on my laptop.

AISI has a new grant program for funding academic and nonprofit-affiliated research in (1) safeguards to mitigate misuse risk and (2) AI control and alignment to mitigate loss of control risk. Please apply! 🧵 www.aisi.gov.uk/grants