What We Think We Know

Noisy synthetic data can improve pretraining. Tiny models can outperform much larger systems on difficult reasoning tasks. Formally verified software can still leave room for ambiguity. Models that appear to retrieve facts may instead organize knowledge geometrically. Even some of the most widely used architectural components of modern language models reveal unexpected limitations when pushed to larger scales.

These findings are a reminder that scientific progress is rarely a straight path from theory to understanding. More often, it involves discovering that our assumptions were incomplete, our explanations insufficient, or our intuitions wrong. Fortunately, those moments are often the most informative.

Pick: LeanBET: Formally-verified surface area calculations in Lean

Software is driving many parts of science. Last month, our Corral paper, but also our newsletter, focused on the importance of the process for producing knowledge: In many cases, we must have trust that the process that we use to derive an answer is correct.

Using code, this might seem easy, but it is surprisingly difficult to write correct code. And everyone who writes code for a living knows what I speak about.

Practices such as tests and test-driven development help to increase the trust in the code we have. However, even if we have covered 100% of the lines of code with tests, tests (even fuzz tests) only cover the behavior for the specific examples we test and do not guarantee correctness in any circumstance.

As more code is being written by autonomous systems such as LLM-based agents, the interest in having guarantees for the code that the agents produce is increasing. The practical reason for that is the fact that it is hard to manually review code and tests at the pace that the systems produce them.

One way to have guarantees is to prove correctness. This is something one can achieve with special programming languages such as Lean. Lean has conventionally been used to prove theorems. But it can also be used to define the implementations and definitions in code and then prove the correctness, and then use the implementation one proved to be correct for execution.

Tyler Josephson’s group has been pushing the formalization of the chemical sciences in Lean for a while and has just been publishing the Lean implementation of a very practical tool for doing BET fits. BET fits of adsorption isotherms are often used (e.g., for metal-organic frameworks, MOFs) to determine surface areas. BET relies on a series of approximations for multilayer adsorption, and it is typically possible to do the same BET fit in many different ways. This is the fact because one performs a fit only on a range of the full isotherm (that fulfills a set of consistency criteria), and there are typically multiple ranges that one could choose. Prior work has shown that, for these reasons, practitioners might fit results that differ by four orders of magnitude when fitting the same experimental data. As a step toward removing some of the ambiguity, researchers proposed a code —-BETSI—- that removes the ambiguity by considering all possible fitting windows.

As this code is implemented with the general-purpose programming language Python, we have no guarantees for correctness, and the code actually implements what it claims to implement. The authors of LeanBET changed this by implementing the code in Lean. This is a tremendous amount of work, but it might nowadays be a bit easier thanks to LLMs also having the ability to write Lean. The main outcome of this work is an implementation where one has more guarantees of correctness. But the more interesting point to me is one statement from the conclusion: “even with a suite of theorems specifying the derivation of the theory and numerous constraints the implementation must satisfy, there exist multiple variations of the software that would satisfy the proofs”.

It turns out that even with the best efforts, there is still ambiguity. There are still “Rashomon sets” of programs that are equivalent within the tests we do, but might still behave differently in edge cases. This is very humbling as there is a lot of effort invested in comparing different implementations of DFT codes, or implementing machine learning pipelines in formalized ways — but there might always be some ambiguity remaining. Even if it is only the floating point number artifacts.

Picks: Probabilistic Tiny Recursive Model

TRM (the simpler single-network successor to HRM) is deterministic at inference: one input, one trajectory, one answer. The authors show that many of TRM’s failures aren’t really “wrong reasoning,” but trajectories stuck in bad basins in latent space with no escape mechanism. The proposed method is straightforward: inject Gaussian noise into the latent state at every deep recursion step, run K parallel rollouts so each settles into a different basin, and use TRM’s existing Q head to pick the best candidate. The Q head is interesting here because it was explicitly trained as a correctness classifier (its loss is binary cross-entropy against 1[ŷ = y_true]) but had only been used to decide when to halt during training. PTRM repurposes it as the verifier it was always trained to be. Think of it as rolling 100 marbles with random kicks down a bumpy hill instead of one, then using a learned eye to spot which one actually reached the bottom. The results are strong for a tiny model (5M for Sudoku, 7M for the rest): Sudoku-Extreme 87.4% to 98.75%, Pencil Puzzle Bench 62.6% to 91.2%, beating an ensemble of 7 frontier LLMs (55.1%) that is even granted a perfect verifier, at roughly 1/40,000th the cost per correct answer.

I find this paper interesting less for the benchmark numbers and more for what it generally implies about deterministic inference. The gap between pass@K and the deterministic baseline suggests TRM was already capable of solving these puzzles, but couldn’t access that capability because inference forced it down a single path. It also reframes what auxiliary heads can do: the Q head was trained to predict correctness all along, the field just used it for halting and threw the signal away at inference. This raises the question of how many existing checkpoints contain trained-but-unused verification capacity. The conceptual bridge to LLMs is also narrower than it first appeared. PTRM is essentially best-of-N with a learned verifier, the same recipe behind LLM test-time scaling, just applied in latent space rather than token space. The caveat is that all of this works because puzzles have clean correctness signals to train the Q head against. For fuzzier tasks, there is nothing to anchor the verifier to, and the verifier problem becomes the actual bottleneck rather than the exploration mechanism PTRM provides.

Pick: Synthetic Pre-Pre-Training Improves Language Model Robustness to Noisy Pre-Training Data

While the LLM research is more focused on the post-training side, especially after the o1 and R1 models, pre-training still has a significant impact on the final performance of the models. However, pre-training is still very challenging because of the scale; leveraging the right data and the right training techniques is crucial to achieve good performance. In this regard, I found the article from Guo et al. very interesting, as it provides a counterintuitive way of enhancing pre-training by starting with a small stage of synthetic data from randomly initialized RNNs. The authors argue that this approach helps the model to better learn what noise is and what the signal is in the data, which ultimately leads to better performance. In the results, the authors show that the method that they propose notably improves the performance of the baseline pre-training (no early stage), random-generated text pre-training, and a strong formal-language baseline (Dyck, which slightly improves the random and baseline pre-training). In the attention ablation that is carried out in the work, the authors show that the model does not learn to downweight the attention to noise tokens during the early stage, but learns faster how to do it at the beginning of the web-based pre-training stage. This is a very interesting finding, as it suggests that the model is able to learn how to filter out noise from the data more effectively when it is exposed to randomly generated text during the early stage of pre-training.

I mention it is counterintuitive because one would expect that starting with very noisy generated text would not provide any useful information to the model, and could even potentially harm the learning process. Rather, I would expect that the model would struggle to learn meaningful patterns from such noisy data. However, the authors show that this is not the case, and that it actually helps the model to learn better representations of the data. But the internal discussion that I have is that it would not be better to clean all the pre-training data to remove all the noise. Obviously, this is perhaps not feasible because of the scale, and using LLMs would result in the data losing all the diversity and richness that is needed for good pre-training. In these lines, a recent article from Mohri et al. showed that my intuition is wrong again, as they show that the best data filtering that you can do for pre-training is none, especially as the model size and training steps increase.

Pick: ATLAS: Agentic or Latent Visual Reasoning? One Word is Enough for Both

ATLAS (Agentic or Latent Visual Reasoning) is a visual reasoning framework that addresses a fundamental limitation of current Vision-Language Models (VLMs), their ability to dynamically manipulate or annotate visual inputs during reasoning. Prior approaches each had drawbacks: unified models that generate intermediate images are computationally expensive; agentic methods that write code or call external tools suffer from high latency and verbose output; and latent methods that reason in a hidden embedding space break standard parallel training and generalize poorly. The authors resolve this by introducing “functional tokens”, five discrete vocabulary tokens (<|Manip|>, <|Shape|>, <|Line|>, <|Arrow|>, <|Text|>), each of which represents an internalized visual operation. Generated like ordinary words through next-token prediction, these tokens allow the model to reason about visual manipulations without actually generating images or invoking external tools, preserving full compatibility with autoregressive training pipelines.

The authors train ATLAS in two stages. First, they curate ATLAS-178K, a dataset of 178K supervised training trajectories built by parsing visual operation code from an existing dataset, mapping those operations to functional tokens, and using Gemini-2.5-Pro to rewrite the resulting trajectories into natural, fluent reasoning text. This Supervised Fine-Tuning (SFT) stage gives the model a reliable foundation for knowing when and how to invoke functional tokens. In the second stage, the authors apply reinforcement learning (RL) via GRPO (Group Relative Policy Optimization), refining performance further through a composite reward that balances answer correctness, meaningful functional token usage, output formatting, and penalties for verbosity and token spamming. Crucially, no custom training modifications are needed, since functional tokens are standard vocabulary entries, and the entire RL pipeline works off-the-shelf.

A key technical challenge identified in the paper is “gradient dilution”; functional tokens make up only about 2.3% of generated tokens on average, so their learning signal gets diluted by the much larger population of ordinary text tokens during RL. To address this, the authors propose Latent-Anchored GRPO (LA-GRPO), which adds a lightweight auxiliary loss anchored specifically at functional token positions in each rollout, reusing the same group-level advantage from GRPO without introducing any new reward signal. This targeted intervention produces stronger, more stable gradient updates on exactly the tokens that matter most for visual reasoning, without disrupting the global optimization.

The results validate the approach convincingly. On the BLINK benchmark, ATLAS improves the base model’s accuracy from 22.8% to 51.3%, with LA-GRPO achieving the most balanced performance across subtasks. Compared to the agentic baseline V-Thinker, the framework reduces inference latency by 5x, cuts peak memory usage by 1.78x, and eliminates verbose code generation entirely, while improving accuracy by 15.7 points. Attention map visualizations further confirm that functional tokens are not mere syntactic placeholders; they genuinely attend to task-relevant visual regions like geometric lines or object boundaries. What makes this work particularly compelling is how it reframes the problem entirely, rather than building heavier architectures or more complex execution pipelines, the authors show that thoughtful vocabulary design alone can substitute for significant architectural complexity.

Pick: RoPE Distinguishes Neither Positions Nor Tokens in Long Contexts, Provably

Scaling the context window of LLMs has become as much a necessity as a trend in recent years. Current models exhibit higher levels of hallucinations and inconsistencies at larger context windows. The authors of “RoPE Distinguishes Neither Positions Nor Tokens in Long Contexts, Provably” analyze these issues from the positional tokenization point of view.

RoPE is responsible for encoding token positions so that transformers can learn about order and relationships within text. The authors show both theoretically and empirically that as context length grows, RoPE progressively loses its ability to distinguish positions. At sufficiently large contexts, attention mechanisms can exhibit position aliasing, where different token positions become indistinguishable, and even token aliasing, where distinct tokens produce effectively identical attention behavior. Rather than treating long-context degradation as merely an optimization or scaling issue, the paper frames it as an architectural problem. The authors prove that RoPE-based attention loses locality properties at long ranges, causing models to struggle with even simple positional retrieval tasks. Experimental results on real-world LLMs confirm these findings: models with very large advertised context windows degrade substantially earlier than expected when asked to retrieve information from long sequences.

I always find works like these very interesting to read. We often take different models for granted and try to apply them to different fields and scale them indefinitely, without looking deep within them to understand how different components work in different conditions. Considering the quality of current benchmarks (or the lack thereof) works like these become a real measurement of models capabilities and limitations.

Pick: SmileyLlama: modifying large language models for directed chemical space exploration

They take Llama-3.1-8B-Instruct and apply SFT and DPO to generate drug-like SMILES with required properties (LoRA with rank 32, ~ 2M parameters, for both the SFT and the DPO parts). They use ChEMBL as the source of molecules and rdkit-derived properties. They compare this with zero-shot and twenty-shot Llama base model, as well as other Chemical Language Models:

Interestingly, (they also mention this in the paper), the twenty-shot model’s validity score is lower!

They apply the same training on other LLMS: 1B and 3B version of Llama-3.1, and also Qwen2.5-7B. There differences are negligible. The only relatively significant change is that larger models have better validity scores.

They show that the distribution of generated SMILES by the model closely resembles the ChEMBL distribution. They also compare the performance of the model on satisfying the required properties. They compare SFT-only, SFT+DPO, and SFT with no properties in the prompt (”prompt-ablation”). The general trend is DPO > SFT > prompt-ablation. The effect of DPO is negligible for tasks with an already high score, but for tasks with a low SFT-only scores, DPO significantly improves the score. The authors claim that these results show that including the properties in the prompts during SFT is necessary, which seems plausible, but… something the authors do not mention and I find super interesting is that the “prompt-ablation” scores are already very high (+80%) for some of the tasks and moderate (~50-60%) for others. Among the scores they show, only 3 tasks have very low score (<2%), and those are the ones for which the SFT and DPO can only achieve moderate scores. This means that a General Purpose Model (GPM), fine-tuned only to generate drug-like molecules with no conditioning on properties, can already understand properties and generate valid molecules that satisfy those properties!

The more interesting (and maybe more useful) part of the paper, shows a closed-loop RL to find protein inhibitors: They sample some molecules —> score them using AutoDock on a specific protein —> update the weights using DPO —> sample again. They show that this approach is more efficient than the iMiner approach (using an LSTM) they compare it too: achieving the same scores on fewer iterations. The resulting molecules have good docking scores but do not have very good drug-likeness. To achieve better drug-likeness, they tried another training loop but this time, they included a few property-requirements in the prompt. This simple approach did enhance the drug-likeness of the resulting molecules at the cost of slightly lowering the docking score.

What I think:

I would draw attention to the surprisingly good performance of the “ablation-prompt” model mentioned above. The authors only use this ablation to say “look, the predictions improve when the model is trained on the properties” which is, to be honest, not surprising. This, combined with the fact that they show the base model has a negligible effect on the performance, makes me want more ablation studies on the effects of the base model. Are the LoRA adapters doing almost all of the heavy-lifting? Probably not, but how responsible is the base model vs the adapters? I would’ve liked an ablation of the size of LoRA adapters, and also one where they randomly corrupt more and more of the weights in the base models to investigate this effect.

What I find very interesting is where they combined prompt-engineering with DPO to do multi-property optimization: DPO is used for the harder part of the problem (docking scores), while the other requirements are delegated to the model itself through prompt-engineering.

Pick: Deep sequence models tend to memorize geometrically; it is unclear why.

The authors use a synthetic path-star graph task. The model first memorizes local graph edges in its weights, then is asked to recover paths for held-out leaf nodes. Crucially, the test paths are never seen end-to-end during training; only their component edges are seen individually. This is designed to isolate in-weights reasoning: the model must reason over knowledge stored in weights, not over a graph supplied in-context. The original in-context version of this task is known to be hard for next-token models, because the first path token requires implicit multi-hop planning.

The paper argues that neural sequence models do not always memorize “facts” as lookup tables. Instead, they can memorize facts geometrically: learned embeddings arrange entities so that distances or dot products encode global relationships, even between entities that never co-occurred in training. This turns some apparently hard multi-step reasoning problems into easier geometric navigation problems.

Transformers and Mamba models succeed on the in-weights version, even when trained only on the hardest first-token decision and without step-by-step supervision from the later path tokens. The authors argue this is surprising because a pure associative-memory view would require learning a difficult multi-hop composition.

Their explanation is that the models learn structured embeddings: nodes on the same path cluster in embedding space, so the first-token prediction can be treated more like a one-step geometric decision than a brute-force chain of local lookups.

One of the natural explanation for this behavior would be: “These settings suggest that representations arise due to pressures from either the supervision or the architecture or the optimizer; such pressures forbid a lookup.” The authors argue against several simple versions of that explanation, on four fronts:

1. Supervision pressure does not explain it: geometry appears even when models are trained only on local edge memorization, with no path-finding objective.

2. Capacity pressure does not explain it: the models can represent associative lookup, and associative memory can even be learned when embeddings are frozen.

3. Optimization pressure does not straightforwardly explain it: in their tiny-graph experiments, associative memory appears easier and faster to find than geometric memory, yet training later organizes memory geometrically.

4. Succinctness does not fully explain it: for sparse graphs like path-stars or cycles, they argue associative and geometric memory can have comparable bit/norm complexity.

Mechanism investigation:

To understand the geometry, they reduce the setup to a simpler weight-tied Node2Vec-like model trained only on local edges with cross-entropy loss. In this simplified case, associative memory is architecturally ruled out, letting them study the geometry itself.

They find that the learned embeddings align with top eigenvectors of the negative graph Laplacian. (The idea being that eigenvector corresponding to the second smallest eigenvalue of a graph Laplacian (adj matrix - degree matrix) is a good descriptor for a graph connectivity).

The paper suggests that common intuitions about language-model memory may be incomplete. If facts are stored geometrically, then models may naturally infer relationships not explicitly trained, which could help with discovery and implicit reasoning. But it also complicates knowledge editing, unlearning, factual retrieval, and hallucination, because facts may be entangled through the embedding geometry.

The authors are careful that their strongest evidence is on symbolic graph tasks, especially path-star and related graph topologies. They do not show that the same mechanism fully explains natural-language factual memory. They also use small to mid-sized from-scratch Transformers rather than large pretrained LLMs, and many of the arguments remain empirical or informal rather than fully theoretically characterized.

Pick: ResearchBench: Benchmarking LLMs in Scientific Discovery via Inspiration-Based Task Decomposition

In the AI4Science field, one of the hot topics is if LLMs can do novel discovery and evaluate this capabilities. This paper introduces ResearchBench, a benchmark that first decomposes scientific discovery into three components: inspiration retrieval, hypothesis composition, and hypothesis ranking. To construct the dataset, the authors adopt a reverse engineering approach based on real scientific papers. They select representative “discovery papers” with a clear research goal, a subset of prior works, and treat the original contribution as the ground truth. This decomposition makes an otherwise open-ended problem more structured and measurable.

The design is thoughtful in several aspects. In particular, the use of controlled inspiration pools with distractors and varying difficulty levels helps prevent trivial retrieval and encourages more meaningful reasoning. Grounding the benchmark in real scientific literature is also a strength.

However, mimicking the complete real scientific process is still challenging. Current work reduces the discovery to a one-shot pipeline, which does not reflect the diversity, iteration, and uncertainty inherent in real research. So it is still hard to say whether models can reconstruct known discoveries rather than genuinely generate new ones.

Moreover, potential biases are also introduced when constructing the dataset. Models may be guided toward the intended solution. More fundamentally, using a fixed ground truth hypothesis overlooks the possibility of multiple valid or even superior alternative solutions.

• Reducing cross-sample prediction churn in scientific machine learning

  When we build models, current best practice is to report the accuracy across different random seeds. However, for many practical applications it is not only enough that the overall accuracy is stable across seeds. We would also like to know that the individual predictions are stable. This is, for instance, relevant in the case of Bayesian Optimization where the individual predictions are experiments one should do — and we would not like them to change with retrainings. In this paper, we show that surprisingly many predictions might change with retrainings. But we also give options to fix this based on a special version of the bootstrap.

• Agentic AI Scientists Are Not Built For Autonomous Scientific Discovery

  A position paper led by Anoop Krishnan’s group in which we argue that current agentic systems, while useful, still have some fundamental limitations that prevent fundamental scientific discovery.

• Condition-aware prediction of copolymer architecture

  One of the big challenges of chemistry is that outcomes for many processes are not only determined by the ingredients of the process but also by the processing conditions. This is especially the case for copolymerizations. Here, two or more monomers react to form a copolymer. Depending on the conditions, different copolymer architectures form. And all these architectures have different application properties. To enable rational design, one would hence need to be able to predict the impact of the conditions on the reaction outcome.

  This has been prohibitive because of the lack of corresponding models, theory, and data. We address this with a dataset we mined from the literature. On this dataset, we train a classifier to predict the conditions. We not only test the classifier on a test set but also retrospectively test on studies that report condition-induced architecture changes, as well as prospectively for new reactions we carried out in-house.

  The data and an interactive prediction tool are available at polycarp.cheminfo.org.

About this newsletter: The paragraphs about the papers are written by group members individually and reflect their own opinions. The newsletter has been reviewed by other group members for factual correctness and edited by Gordan Prastalo and Kevin Jablonka. The editorial is written by Gordan Prastalo.