Two Graphs for Mathematical Discovery: What COMPOSE Gets Right

When we ask a language model to imagine the next theorem a research program might produce, we are really asking two different questions at once. The first is a question of direction: given where a field has been going, what comes next? The second is a question of legality: given the formal scaffolding of definitions, lemmas, and prior results, what can validly follow? These questions are not the same, and conflating them is the reason so much machine-generated mathematics reads as fluent but hollow. A recent paper, COMPOSE: Composing Future Theorems from Citations and Formal Structure by David Busbib and Michael Werman at the Hebrew University of Jerusalem, takes the position that these two questions deserve two separate representations, and that grounding requires both.

This is a quiet design decision with broad implications. Below I work through what the paper does, why the dual-graph framing matters, and where I think the idea travels beyond mathematics.

The task: grounded future mathematical generation

The authors define a task they call grounded future mathematical generation. Given an anchor paper, the goal is to generate a plausible future theorem-like claim that both extends the research trajectory of prior work and respects the logical dependencies of the underlying mathematics. The framing draws an explicit line between two failure modes in existing systems:

• Models trained on scientific text alone can identify plausible research directions but produce claims that float free of formal mathematical dependencies. They sound right but may not be derivable from anything.
• Theorem-proving systems reason carefully over formal structure but lack the surrounding scientific context to judge which directions are worth pursuing. They are valid but unmotivated.

The insight is that a plausible future claim sits at the intersection. It must satisfy what the authors implicitly treat as two constraints: follow the direction of prior work, and respect the formal dependencies that constrain what can validly follow. This is the cleanest articulation I have seen of the distinction between plausible and valid in the context of automated mathematical discovery.

The method: two graphs, encoded separately, fused for generation

COMPOSE represents the two sources as two complementary graphs.

The scientific graph is built from the anchor paper, a set of selected cited papers, and theorems extracted from those papers. In the architecture diagram, paper abstracts and extracted informal theorems form nodes, connected through the citation relations. This graph captures the trajectory of ideas: which results are building on which, and in what direction the literature is moving.

The formal graph is constructed by aligning each extracted informal theorem to its corresponding theorem in Lean's Mathlib, then importing the Lean dependency structure among those formal theorems. This graph captures the rigid logical scaffolding: what depends on what, what must already hold for a new result to be stated.

The bridge between the two is an informal-to-informal alignment strategy using a tool the authors call FrenzyMath, which matches each informal theorem from a paper to its Mathlib counterpart. This alignment step is the technical heart of the construction, because the same mathematical content appears very differently in a prose abstract and in a formal Lean statement. Getting this matching right is what makes the two graphs comparable at all.

Architecturally, the system uses:

• A dedicated graph neural network encoder for the scientific graph.
• A separate GNN encoder for the formal graph.
• A cross-attention fusion module that combines the two into a shared representation.
• A math-specialized LLM decoder conditioned on that fused representation, which generates the future research claim.

Training proceeds in two stages. The graph encoders and fusion module are first optimized with alignment objectives, then the decoder is fine-tuned for graph-conditioned generation. This staged approach is sensible: it forces the model to learn a coherent joint embedding of the two structures before asking it to write mathematics on top of that embedding.

The data and the evaluation

One of the more substantial contributions here is the dataset itself. The authors construct 108K paired scientific-formal graph examples from arXiv mathematics and Mathlib, using pre-2023 papers for training. They then build a benchmark of 47K future papers from late 2024 and 2025 for evaluation. The temporal split is the right move for a task about predicting the future: training on the past and testing against papers that genuinely appeared later is far more honest than a random split, because it prevents the model from simply interpolating within a fixed snapshot of the literature.

Evaluation runs along two axes. The first is retrieval to real future papers: does the generated claim resemble what actually came next, measured by retrieval against the held-out 2024 to 2025 corpus? The second is LLM-judge evaluation, where a model assesses the quality of generated claims. COMPOSE reports the strongest retrieval performance and the best overall performance under LLM-judge evaluation, producing outputs the authors describe as more grounded and mathematically richer. Ablations confirm that both graph sources contribute, which is the claim that matters most: removing either the scientific or the formal graph degrades performance, supporting the central thesis that direction and validity are genuinely separate signals.

My take: the plausible-versus-valid split generalizes

The dual-graph framing is more general than the paper's mathematical focus suggests. What COMPOSE really encodes is the difference between a soft preference graph of what people are pursuing and a hard constraint graph of what is admissible. Once you see the structure in those terms, you find it everywhere.

• Drug discovery has exactly this shape. There is a citation-like signal of promising chemical directions, the molecules and scaffolds the field is gravitating toward, and a hard constraint graph of chemical and physical validity, synthesizability, and known reaction dependencies. A generated candidate must be both fashionable and feasible.
• Code synthesis has it too. Trending APIs and common usage patterns form the direction graph, while type dependencies, import requirements, and compilation constraints form the validity graph. A plausible function call is not the same as a well-typed one.
• Even experimental science planning fits: the literature signals which experiments are worth running, while resource and methodological dependencies constrain which can actually be run.

The lesson I draw is that grounding is not a single property to be optimized. It decomposes into "what should come next" and "what can come next," and these are best modeled as distinct graphs with distinct encoders, fused late rather than merged early. Late fusion preserves the structural character of each source, which an early concatenation would blur.

There is also a deeper point about evaluation hiding inside this paper. Retrieval against real future papers is an elegant proxy, but it rewards claims that resemble what humans did publish, not necessarily claims that are correct or genuinely novel. A model could score well by producing safe, conventional extensions. The truly interesting future claims, the ones that redirect a field, would by construction score poorly on retrieval because nothing resembling them yet exists.

Limitations and open questions

The honest limitations follow from the construction. The whole pipeline depends on the informal-to-formal alignment step, and Mathlib, while large, covers only a fraction of published mathematics. Entire subfields have little or no formalized counterpart, which means the formal graph will be sparse or empty precisely where mathematics is most active and least settled. The system is therefore strongest in well-formalized areas and weakest at the frontier, which is somewhat in tension with the goal of anticipating future work.

A second open question concerns verification. COMPOSE generates theorem-like text, but it does not prove that text. The formal graph constrains what could plausibly follow, yet a generated claim is not checked against Lean. The natural next step is to close that loop: feed generated claims to a theorem prover and use provability as a filter or reward signal. That would turn plausible-and-valid-looking into plausible-and-actually-valid.

The broader question is whether this kind of system can ever propose directions rather than extrapolate them. For now, COMPOSE is a thoughtful answer to a well-posed problem: separating what should come next from what can come next, and insisting that real grounding needs both.