Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
The paper introduces grounded future mathematical generation, a task that aims to generate plausible future theorem-like claims for a given anchor paper using both its citation graph and aligned formal theorem dependency graph. To tackle this, they propose COMPOSE, a dual-graph framework that conditions a language model on both scientific citation context and formal theorem structure. Experiments on a new dataset of 108K paired scientific-formal graph examples demonstrate that COMPOSE outperforms strong baselines in retrieving real future papers and generates more grounded and mathematically richer outputs as judged by LLMs.
Generating plausible future mathematical claims is now possible by jointly modeling scientific citations and formal theorem dependencies, leading to more grounded and mathematically rich outputs.
A plausible future mathematical claim must satisfy two constraints: it should follow the direction of prior work and respect the formal dependencies that constrain what can validly follow. Existing approaches typically model only one of these sources, producing claims that are either weakly grounded or insufficiently motivated. We introduce grounded future mathematical generation, where the goal is to generate a plausible future theorem-like claim for an anchor paper using two complementary sources of context: its scientific citation graph and aligned formal theorem dependency graph. To address this setting, we propose COMPOSE, a dual-graph framework that conditions a language model on both scientific citation context and formal theorem structure. To support this setting, we construct a dataset of 108K paired scientific-formal graph examples from arXiv and Mathlib, together with a benchmark of 47K future papers from 2024--2025. Experiments show that COMPOSE outperforms strong baselines on retrieval to real future papers and achieves the best overall performance under LLM-judge evaluation, producing more grounded and mathematically richer outputs. These results show that future mathematical generation benefits from combining scientific context with formal structure. Project page is available at https://david-busbib.github.io/COMPOSE-page/.