Self-Play for LLMs, AI for Biology, Formal Verification, and More

Yaso explains how ESM Cambrian learns from amino acid sequences using masked-token prediction, without being given protein structures. Its long-range contact performance follows a smooth scaling curve, and unlike the earlier ESM-2 models, it keeps improving as model size and compute increase. The researchers expanded training data from about 50 million sequences to 2.8 billion, much of it from metagenomic sources.

The paper compares ESMFold 2, which uses a single protein sequence, with AlphaFold 3, which uses multiple sequence alignments. ESMFold 2 comes within about three points of AlphaFold 3 on general protein complexes and scores about 50% versus 47% on the antibody task described. Yaso notes that alignments can be slow to build and may be less useful for antibody design, where available sequence diversity is limited.

Sparse autoencoder analysis finds model features associated with amino acids, structural motifs, protein domains, and functions, despite the model receiving no such labels during pretraining. One feature identifies the nucleophilic elbow motif across structurally different proteins. The researchers also use model representations to build a large protein atlas, including maps of families such as CRISPR-Cas enzymes.

Luke Bailey presents self-guided self-play for language models, using Lean math problems as a test case. In baseline self-play, the model learns to generate difficult problems, but it produces convoluted statements that do not help the solver; performance matches regular reinforcement learning. The proposed method grounds generated problems in unsolved targets and uses a guide model to judge relevance and complexity. With eight times the compute, a 7B model reaches the pass@ performance of a 670B model on the reported evaluation.

Robert George describes Lean as a programming language and proof checker for formal mathematics, then discusses applying verification to programs and neural networks. In the final presentation, Luke Orthwein of Channel AI compares agent-assisted software work to real-time strategy games: run parallel tasks, monitor them, and correct mistakes early. His team reports 3.5 times as many PRs per engineer per month, with a further 60% increase after broader adoption of its workflow.