Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means

Welcome to Import AI, a newsletter about AI research. Import AI runs on arXiv, cappuccinos, and feedback from readers. If you’d like to support this, please subscribe. Subscribe now How math could help alignment: ...What the “industrialization of mathematics” means for safety... AI safety startup Resolution (formerly known as Sequent, Import AI 461 ) has published work on how it has automatically formalized some mathematical statements related to statistical learning theory. Specifically, the team has autoformalized the resolution of singularities, which they believe “lays the groundwork for further automated research into the relationship between loss landscape geometry and generalization.” How they did it: I’ll skip over the math and concentrate on how they did it, which gives us some broader lessons for how people are using AI systems to push on the frontier of knowledge. A Resolution researcher “started by working with agents to develop two plans: a high-level, human-interpretable version and a detailed (112-page) plan divided into atomic steps that closely followed the existing literature,” they write. The researcher “then deputized an orchestrator agent to carry out the plan, spinning up agents to do pen-and-paper math, write Lean, and handle support functions like checking that things were staying on track... the execution phase required little scaffolding beyond the initial plan and some agent skills distilled from earlier internal autoformalization efforts.” $135k for math formalization: The work took about a week, taking “on the order of 100B input tokens (90% cache reads) and about 300 million output tokens (totaling an estimated $135,000 in token spend), and produced about 600k lines of Lean.” Now that they’ve done this, they’ve been able to accelerate some other aspects of their research: “We have already seen both benefits from autoformalization in using this library to extend parts of singular learning theory. Formalizing resolution of singularities lets us automate more of the theory, for example, to better understand sampling, and that understanding is what lets us shape how models learn, which is the goal of what we call patterning”. Why this matters – perhaps the math boom will help us make safe AI: Though frontier mathematics often seems disconnected from immediate advances in other fields, posts like this highlight how the two might converge. The key point here is that AI is making it possible to do things that were previously so unbelievably expensive and human-time-intensive that very few people did them and you couldn’t easily integrate them into the research roadmap of a startup – but that has now changed. “We expect the coming industrialization of mathematics to make possible a new, rigorous science of research automation,” Resolution writes. Read more: Formalizing Hironaka’s Resolution of Singularities (Resolution) . *** Agents can build programs from scratch: ...ProgramBench goes from 0% to 18.5% performance in a few months... In a reminder of the blistering pace of AI progress, Claude Opus 5.5 (xhigh) has got a score of 18.5% on ProgramBench, a very hard benchmark that came out in May of this year – and when it came out, every tested model scored 0%. What ProgramBench is: ProgramBench tests out how well AI systems can rebuild software programs based on being given a compiled program and its documentation. Tasks include building things like language interpreters (PHP, Lua, tinycc), databases (DuckDB, SQLite), media and compression utilities (FFmpeg, zstd, xz), and developer tools (ripgrep, fzf, jq). It was very hard until it wasn’t: When it came out, the best scoring system was Claude Opus 4.7 with 0% resolved (fraction of the 200 tasks where all tests passed), and 3% almost (fraction of the 200 tasks where >95% of tests pass). Compare that to today, when Claude Opus 5.5 gets 18.5% resolved and 70.5% (!!!) almost. Why this matters – the era of ephemeral software cometh: In 2027, huge amounts of software will be built via AI systems end-to-end autonomously developing whatever they need to do for whatever tasks they’re being put to. Evals like ProgramBench give us a sense of how rapid the pace of progress is here, given we went from 0% earlier this year to 20% now. My expectation is ProgramBench is saturated by the end of 2027 (where I define saturated as some very high score on resolved, though as with most benchmarks it’s likely there’s some kind of noise ceiling here, so it might not strictly be 100%). Read more: ProgramBench: Can Language Models Rebuild Programs From Scratch? (arXiv) . *** OpenAI illustrates why locking down AI systems is harder than you think: ...Securing smart agents is like catching greased pigs... Here’s a nice post from OpenAI going over some of the things they discovered when they recently used their AI systems to ‘red team’ their own internal controls. The post goes over a number of the escapes and vulnerabilities that OpenAI’s agents found. There’s one particular example about communicating which is worth studying in detail because it tells us something about the wild cunning complexity of these systems. What they did and what they found: OpenAI “asked agents in separate microVMs, created and managed by OpenAI’s sandboxing software on shared host machines, to exchange synthetic secrets without the use of network connections or shared writable files—something that our systems are meant to prevent,” the company wrote. “The agents found a way to communicate using the processor’s cache: a small, fast memory that holds copies of data that applications have recently accessed. Reading data from the cache is faster than retrieving it from main memory, and the agents used this timing difference to communicate. One agent encoded information by evicting selected data from the cache. Another timed how long it took to reload that data, using the difference between fast and slow reads to recover the message. Once the agents agreed on a protocol for encoding and decoding these signals, they could exchange the synthetic secrets without changing a shared file or opening a network connection”. In a related attack, an agent “alternated between continuous writes and inactivity, while another measured the resulting timing differences and used those differences to decode the signal”. During this attack the agent’s chain of thought read as: “Could create acoustic modem-like signal ... using continuous writes vs idle.” Why this matters – fighting agents is very difficult : AI systems are increasingly creative, very fast, and have the ability to stay focused on a task and keep trying things. Fighting AI systems is akin to ensuring no leaks in a pipe with water flowing through it; at some point if you increase the pressure of the water (e.g., the intelligence and volume of the AI system), then the water will burst through the pipe. Read more : Securing our frontier model training environment (OpenAI blog) . *** What RSI looks like – one person pretrains a decent model from scratch: ...Mirendil reveals what AI R&D optimization can do... In a sign of how massively augmented AI research is getting, a single researcher at AI R&D startup Mirendil has trained a decent coding model by themselves. The announcement of Mirendil-Base is the first major output from the startup and is less a technical breakthrough and more a proof-of-concept for how AI development could work in the future – a single human working in partnership with AI can build systems that would have taken teams of ten or more people to do a year ago. What they did: Mirendill-Base is a pretrained LLM “built by one researcher in 3.5 months, with less than $10m in compute,” Mirendil writes. “This includes all the research and small-scale experiments it took to get there, as well as the final training run.” All the code was written from scratch on top of libraries like PyTorch and JAX, and the model learned only from publicly available data. Decent scaling: Mirendil-