COMPOSE: Predicting Future Math by Combining Citation Networks and Formal Proofs

Paper: 2605.30333 Authors: David Busbib, Michael Werman Categories: cs.CL

The Gap

Existing approaches to generating future mathematical claims face a fundamental split: citation-based methods produce claims that follow research trends but lack formal rigor, while formal theorem provers generate logically valid statements that feel disconnected from actual research directions. Neither alone captures what makes a mathematical claim both plausible and interesting—it must extend current research momentum while respecting the logical constraints of what can actually be proven next.

Problem: Generate plausible future math theorems
         |
         v
Prior approaches split the task:
         |
    +----+----+
    |         |
Citation    Formal
context     structure
    |         |
    v         v
Motivated   Valid but
but weak    unmotivated
    |         |
    +----+----+
         |
         v
Gap: Need BOTH sources simultaneously
         |
         v
Method: Dual-graph conditioning (COMPOSE)
         |
         v
Evidence: 108K paired examples, 47K future papers
         |
         v
Conclusion: Combined grounding > either alone

The Increment

One sentence: Before this paper, you could generate mathematically motivated claims OR formally valid claims; after, you can generate claims that are both grounded in research context and respect formal dependencies.

Core Mechanism

COMPOSE operates on two parallel graph structures. The first is a scientific citation graph where nodes are papers and edges represent citations—this captures research momentum and thematic evolution. The second is a formal theorem dependency graph from Mathlib where nodes are formalized theorems and edges represent logical dependencies—this captures what can validly follow from what.

The framework encodes both graphs using separate graph neural networks, then fuses their representations before feeding them to a language model. For a given anchor paper, COMPOSE retrieves relevant neighbors from both graphs: cited papers that establish research context, and formal theorems that the anchor’s formalized counterparts depend on. These dual contexts condition the generation process, constraining the output to respect both scientific plausibility and formal structure.

The key architectural choice is late fusion: graph encodings remain separate until the final conditioning stage, allowing each graph to preserve its distinct signal. The scientific graph provides topical coherence and research direction; the formal graph provides structural constraints and logical scaffolding. The language model then generates theorem-like claims that satisfy both sources of grounding.

Input: Anchor paper P
         |
    +----+----+
    |         |
    v         v
Citation    Formal
 graph      graph
    |         |
    v         v
  GNN       GNN
encoding  encoding
    |         |
    +----+----+
         |
         v
    Late fusion
         |
         v
Condition LM on
dual context
         |
         v
Generate future
theorem claim

Think of COMPOSE as a research advisor with two complementary knowledge sources. The citation graph is like reading recent papers in your subfield—you understand what problems people care about, what techniques are gaining traction, what open questions remain. The formal graph is like checking a proof assistant—you know exactly what lemmas are available, what dependencies must be satisfied, what logical steps are valid. A good advisor consults both: they suggest research directions that are both interesting to the community (citation context) and technically feasible given existing foundations (formal structure). COMPOSE mechanizes this dual consultation by encoding both knowledge sources and using them jointly to guide generation.

Key Concepts

• Grounded generation: Standard language models generate text by predicting likely continuations based on training data patterns. Grounded generation adds external constraints—the model must produce outputs consistent with specific retrieved context. Here, “grounded” means the generated theorem must be plausible given both the scientific papers that cite or are cited by the anchor, and the formal theorems that logically precede it. It’s the difference between free-form creative writing and writing a sequel that respects established canon from two different source materials simultaneously.

• Dual-graph conditioning: Most graph-conditioned generation uses a single graph structure. COMPOSE conditions on two heterogeneous graphs with different semantics. The citation graph is dense and thematic (papers cite many related works); the formal graph is sparse and logical (theorems depend on specific prior results). Conditioning on both means the model receives two distinct signals: “this is the research direction” from citations, and “these are the available building blocks” from formal dependencies. The challenge is preserving both signals without one drowning out the other—hence separate encoders and late fusion.

• Scientific-formal alignment: The dataset pairs arXiv papers with their Mathlib formalizations. Not all math papers have formal counterparts, and not all formal theorems correspond to published papers. Alignment means establishing correspondence: when paper P discusses theorem T, and Mathlib contains a formalization F of T, we link P to F. This creates a bridge between informal mathematical discourse (papers) and formal mathematical objects (proof assistant code). The alignment enables training on paired examples where both graphs are available, teaching the model to respect both modalities.

Framework Shift

Before (mainstream approach):        After (this paper):

Citation graph only:                 Dual-graph fusion:
                                     
Paper -> [GNN] -> LM -> Output       Paper -> [Citation GNN] -+
                                                               |
  Motivated but                                                v
  formally weak                                           [Fusion] -> LM
                                                               ^
OR                                                             |
                                            [Formal GNN] ------+
Formal graph only:                                |
                                            Formal graph
Theorem -> [GNN] -> LM -> Output       
                                          Motivated AND
  Valid but                               formally grounded
  unmotivated

One sentence: From single-source conditioning (either research context or formal structure) to dual-source conditioning, the core shift is treating scientific plausibility and formal validity as complementary constraints rather than alternative approaches.

Expert Assessment

Problem choice: This is a real gap. The split between citation-based and formal methods reflects a genuine tension in mathematical AI: informal math (papers, intuition, research directions) versus formal math (proof assistants, verified theorems). The problem sits at the intersection of two active research areas—scientific document understanding and automated theorem proving—and addresses a practical need: helping mathematicians identify promising research directions that are both interesting and technically feasible.

Method maturity: The approach is straightforward—dual GNN encoders with late fusion. No architectural novelty, but that’s appropriate here. The insight is problem formulation, not algorithmic innovation. The choice of late fusion over early fusion or cross-attention is under-justified; ablations show it helps, but the paper doesn’t deeply explore why. A simpler baseline would be concatenating citation abstracts and formal theorem statements as text, bypassing graph encoding entirely—this isn’t tested.

Experimental integrity: The benchmark is solid: 47K real future papers from 2024-2025 provide ground truth for retrieval evaluation. Baselines are reasonable (citation-only, formal-only, text-only). The LLM-judge evaluation is standard but has known limitations—GPT-4 preferences don’t always align with human expert judgment, especially for mathematical content. The paper acknowledges this but doesn’t include human evaluation, which would strengthen claims. Retrieval metrics (recall@k) are clean; generation metrics (LLM-judge scores) are softer. Numbers are plausible and consistent across experiments.

Writing quality: The related work section is thorough but dense—it lists many prior systems without clearly positioning COMPOSE’s unique contribution until late. The method section is clear, but the dataset construction details are scattered across main text and appendix, making it hard to assess data quality. The results section front-loads tables without sufficient narrative guidance. Rewriting the introduction to lead with a concrete example (showing a generated theorem and explaining why it needs both graphs) would make the motivation immediately tangible.

Verdict: weak accept — Solid problem formulation and clean execution, but limited architectural novelty and reliance on LLM-judge evaluation without human validation. The contribution is primarily in dataset construction and demonstrating that dual grounding helps, not in methodological innovation.

Takeaways

For practitioners building grounded generation systems: The late fusion architecture is worth stealing. When you have multiple heterogeneous context sources (structured data, unstructured text, knowledge graphs), encoding them separately and fusing late preserves distinct signals better than early concatenation. Test this against simpler baselines (text-only, early fusion) to verify the graph structure actually helps.

For researchers in scientific document understanding: The scientific-formal alignment pipeline (matching arXiv papers to Mathlib formalizations) is reusable infrastructure. If you’re working on math-heavy domains, this paired dataset enables training models that bridge informal and formal representations. The alignment heuristics (matching by theorem names, author overlap, temporal proximity) are domain-specific but the general approach transfers.

For anyone doing retrieval-augmented generation: The paper’s evaluation setup—using real future documents as ground truth for retrieval—is a cleaner benchmark than synthetic or held-out test sets. If your domain has temporal structure (papers, patents, code commits), consider constructing similar future-prediction benchmarks to evaluate whether your retrieval actually captures forward-looking relevance.

Honest assessment: The core idea (combine citation context with formal structure) is simple and the execution is competent, but there’s no single technique here that fundamentally changes how you’d approach other problems. The value is in demonstrating that dual grounding works for this specific task and providing the dataset to enable follow-up work.