Grantmaking.ai link: https://app.grantmaking.ai/projects/0bf05c8a-676a-4702-b14d-c4d4a209a12b

Project summary

In this project, we aim to produce theoretical and foundational results in mechanistic interpretability by leveraging the recent advances in the mathematical abilities of frontier models. To make sure that the theorems provided by the frontier models do not contain logical flaws, we formally verify them in Lean 4. Preliminary analyses hint at a mathematical abstraction (imagine Feynman diagrams for particle physics and more recently, twistors for cosmological correlators) for multihead attention that can unlock progress in knowledge discovery for foundational mechanistic interpretability. Such an abstraction would help with tracking features across the layers of a transformer and hence provide theoretical foundations to build tools for feature discovery in transformers.

What are this project's goals? How will you achieve them?

We start with a simple pilot question: how many attention heads are required to represent a Boolean function? We first treat multihead attention as a basic building block and then extend this analysis by including feed forward networks. By doing so, we are eventually working towards the goal of composing these component level theorems to understand the expressivity of the multilayer transformers. This question is not a purely abstract one: it grew out of my MATS work on understanding alignment pretraining, where I study how features are represented after an attention update. This connection gives some evidence that studying expressivity of multihead attention can be relevant to empirical mech interp, not just to formal expressivity theory.

The pilot question also serves as a feasibility test for the whole program. The setting is simple enough for frontier models to make progress while requiring a human expert to ask the high level questions. Initial autoresearch runs have produced impressive results that have provided us with some good intuitions that the next phase can build on.

Method

We plan to use an autoresearch pipeline, consisting of multiple frontier models collaborating to generate theorems and formally verify them. Our implementation adapts and extends the harness proposed in Numina Lean Agent, tailoring it to the problem at hand. During the course of the project, we hope to identify the "secret sauce" of multiagent orchestration, i.e., the optimal harness can make progress in foundational mech interp.

Concrete outputs

This phase is expected to run for four months, and I have requested the budget accordingly. By the end, we aim to deliver the following outputs:

1. A mechanistic interpretability dojo: an open source modular library in Lean 4 that formally verifies the mathematical results obtained during this project. The goal is also for this to serve as a reusable codebase for other researchers to formally verify mathematical statements in mech interp.
2. An open source multi agent orchestration harness: A system for coordinating frontier models for conjecture generation, proof search and Lean verification.
3. LessWrong posts containing the theoretical progress made during the pilot, and a retrospective on what this project reveals about LLM-automated knowledge discovery for mechanistic interpretability.

Theory of impact

Mechanistic interpretability is an important component of a broader toolkit for AI safety and oversight. Theoretical mech interp works (Elhage et al., 2021; Elhage et al., 2022) has shaped empirical interpretability by providing useful abstractions, and principled starting points for experimentation. However, developing this kind of theory has been demanding, requiring sustained expert effort to work through the underlying mathematics. Yet recent advances in language models for mathematical reasoning and formal theorem proving may make it possible to produce rigorous results at a lower cost. This project aims to produce foundational results for empirical interpretability by leveraging the growing mathematical abilities of frontier models, while identifying multi agent harnesses that make such theoretical research faster and more reliable.

Precedent for foundational theory shaping empirical mech interp research

There is precedent for foundational theory shaping mechanistic interpretability. "A Mathematical Framework for Transformer Circuits" (Elhage et al., 2021) worked out the mathematics of attention from first principles, and many later mechanistic interpretability ideas (for example, induction heads) build on that framework. Our aim is more modest than that of Elhage et al. but similar in spirit: a growing library of kernel-checked theorems that applied researchers can use as reference points, and a workflow for producing them faster than hand-derivation alone.

Why formally verified autoresearch for foundational theory?

1. Need for autoresearch: foundational theory is hard to scale with human effort alone. Hand-derivation is slow and expertise-intensive, and frontier models can now carry much of this load, and the field is already beginning to automate alignment research itself.

2. Need for formal verification: unverified automation can fail quietly. Frontier models make mistakes, long derivations accumulate subtle errors, and human evaluation alone cannot reliably catch either, so automated research tends to produce results that look compelling but are quietly wrong. Requiring every proof to pass the Lean kernel removes this failure mode for mathematical claims. Resolution's launch note makes a similar case: theory unlocks higher automation because proofs give automated research a source of ground truth that empirical metric-climbing lacks. A four-month open pilot that shows where kernel-verified autoresearch works, and where it breaks, is low-cost evidence for those far larger bets on automated alignment research.

How will this funding be used?

Full budget with the split for the minimum and ideal: budget spreadsheet

The grant funds a four-month project (August to November 2026) with the following splits:

• Project lead stipend (part-time). I coordinate the project, adapt the proving agent to the head-complexity problem, supervise the mentees, and do the mathematics alongside the agents.

• Two paid mentees, a research scientist (mech interp theory) and a research engineer (multi-agent orchestration), who run the autoresearch experiments and the orchestration ablations. Paying them secures reliable commitment to the project's core deliverables.

• Claude, OpenAI, and Google AI subscriptions for the two paid mentees, since the multi-agent proving pipeline runs on frontier-model subscriptions.

• GPU compute for the empirical experiments (RunPod, roughly 10 hours per day across the project).

• CPU compute for the multi-agent orchestration runs and Lean proof checking (RunPod CPU pods, one each for me and the two paid mentees)

Who is on your team? What's your track record on similar projects?

The current team consists of 5 researchers with expertise in mechanistic interpretability and Lean formalization. We plan to onboard two additional researchers over the coming months to help with the multi agent orchestration and mech interp aspects of this project.

• Karthik: I set the direction, do the mathematics alongside the agents, and run the autoresearch pipeline. I am responsible for setting the research direction and coordinating the autoresearch pipeline among other things. I have been a part of MARS 3.0 and MATS 9, and have published papers on interpretability in ICML and TMLR.

• Collaborators from Berkeley Research Academy who maintain the repository with the formally verified proofs in Lean 4. They also guide the autoresearch pipeline by suggesting the mathematical abstractions that can be used to characterize multihead attention.

• Two paid mentees to be recruited:

  • A research engineer to build the multi agent orchestration framework

  • A research scientist to help with the mech interp aspects and guide the autoresearch framework

What are the most likely causes and outcomes if this project fails?

The most likely cause of failure is that this research problem is simply too hard for current autoresearch systems. The agents may require so much expert steering that the pipeline does not outperform a conventional human research workflow. Even if they solve isolated head-complexity problems, those results may not compose cleanly when we add feed forward networks and multiple layers. In that case, we would produce some verified partial results but not a useful general theory, providing evidence that current frontier models are not yet capable of automating this kind of foundational mechanistic interpretability research.

Outcomes if this project fails:

1. Multi-agent framework for mech interp researchers. The project also studies which multi-agent workflows produce verified knowledge discovery, which fail, and why. We will measure this on a live research problem and report the harness via an open source contribution. This also derisks the project: even if the head-complexity mathematics advances more slowly than hoped, the funded work still leaves behind an open, reusable multi-agent system for formalized interpretability theory.

2. Field-building. On the field building side, the project trains six early-career researchers (four dojo mentees already onboarded, two paid orchestration mentees to be recruited) at the intersection of interpretability, formal verification, and AI-assisted research, building a small talent pipeline for verified interpretability work.

How much money have you raised in the last 12 months, and from where?

We have received $17,800 from the launch round of grantmaking.ai. Please refer to the grantmaking.ai page for more details.

We have also received a $1,920 BlueDot Rapid Grant, which covers AI tool subscriptions for our Berkeley Research Academy collaborators. While the BlueDot Rapid Grant is a part of this project, it is separate from this request and does not overlap with this budget.