Research map / Graph learning / Knowledge and temporal graphs
COMPOSE: Composing Future Theorems from Citations and Formal Structure
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces grounded future mathematical generation and COMPOSE, a dual-graph (citation graph + Mathlib dependency graph) conditioned LLM that generates plausible future theorem-like claims, evaluated by future-paper retrieval and LLM-judge scores.
Problem
Generating plausible future mathematical claims for an anchor paper requires both the research direction from citation context and the formal dependency constraints of mathematics, which existing methods model only partially.
Approach
A dual-GNN encoder over a scientific citation graph and an aligned formal Mathlib dependency graph, fused by bidirectional cross-attention and fed as conditioning into a LoRA-adapted math LLM decoder, trained in two stages with link-prediction, alignment, cross-modal, and graph-margin losses.
Key results
- COMPOSE (DeepSeek-Math 7B) reaches Gap 0.240 and H@10 0.508 on future retrieval, versus 0.176 and 0.369 for Text-only (LoRA).
- Under LLM-judge evaluation COMPOSE (DeepSeek) achieves the highest overall score of 3.36/5, ahead of Prompt-only (3.10) and GIANTS (2.75).
- Removing the scientific graph drops H@10 to 0.135 in the formal-graph-only ablation, and the paper-graph-only variant reaches H@10 0.390 vs 0.508 for the full model.
Surprising findings
- Text-only and Prompt-only baselines capture the right topic but have high Neg-Sim, so their retrieval gap is smaller than COMPOSE's despite similar Tgt-Sim.
- GIANTS and FutureGen score higher on Novelty in the LLM judge than COMPOSE, which trades novelty for mathematical content.
Limitations
- Informal-to-formal alignment is approximate and introduces noise into the formal graph encoder.
- Generated claims are not verified by a proof assistant, so evaluation relies on proxy retrieval and LLM-judge signals.
- Main-claim extraction from future papers may be noisy for papers with multiple results.
Experimental setup
Datasets: S2ORC arXiv mathematics papers (2000-2023) Mathlib FrenzyMath
Benchmarks: future-paper retrieval benchmark (47K pool, 2K test) NMCP
Metrics: Tgt-Sim Neg-Sim Gap H@10 H@100 Exp-Sim NMCP Precision NMCP Match LLM-judge scores BERTScore
Baselines: GIANTS GoAI FutureGen CoI ResearchAgent Fixed NN Text-only (LoRA) Prompt-only Paper-graph-only Bag-of-Papers
Builds on: LoRA FrenzyMath LeanDojo S2ORC E5
Closest papers by meaning
- Semantic Search over 9 Million Mathematical Theorems (NeurIPS 2026 · similarity 0.84)
- RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.84)
- HLM-Cite: Hybrid Language Model Workflow for Text-based Scientific Citation Prediction (NeurIPS 2024 · similarity 0.83)
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.83)
- OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text (ICLR 2024 · similarity 0.83)
- Foundation Models for Scientific Discovery: From Paradigm Enhancement to Paradigm Transition (NeurIPS 2025 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.