TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow

TL;DR

The paper addresses the high cost and data scarcity in training formal-reasoning models by introducing TheoremForge, a modular, low-budget data synthesis pipeline that decomposes formalization into five sub-tasks and employs a Decoupled Extraction Strategy to salvage training signals from failed trajectories. By leveraging a mix of expert and general-purpose LLMs, targeted premise retrieval, and semantic verification, it achieves a favorable cost-per-success trajectory and a higher Verified Rate (VR) on a 2,000-problem benchmark ($$VR=12.6\%$$, $$\text{cost}=\$0.481\text{ per successful trajectory}$$) compared to a baseline. The work demonstrates a 1.6× data-yield boost for proof-generation via decoupled extraction and documents robust cross-domain performance with meaningful bottlenecks in proof sketching and correction. This approach provides a scalable data flywheel to train future expert models in formal mathematics and suggests practical benefits for building open-source corpora and downstream learning tasks.

Abstract

The high cost of agentic workflows in formal mathematics hinders large-scale data synthesis, exacerbating the scarcity of open-source corpora. To address this, we introduce \textbf{TheoremForge}, a cost-effective formal data synthesis pipeline that decomposes the formalization process into five sub-tasks, which are \textit{statement formalization}, \textit{proof generation}, \textit{premise selection}, \textit{proof correction} and \textit{proof sketching}. By implementing a \textit{Decoupled Extraction Strategy}, the workflow recovers valid training signals from globally failed trajectories, effectively utilizing wasted computation. Experiments on a 2,000-problem benchmark demonstrate that TheoremForge achieves a Verified Rate of 12.6\%, surpassing the 8.6\% baseline, at an average cost of only \textbf{\$0.481} per successful trajectory using Gemini-3-Flash. Crucially, our strategy increases data yield by \textbf{1.6$\times$} for proof generation compared to standard filtering. These results establish TheoremForge as a scalable framework for constructing a data flywheel to train future expert models. Our code is available \href{https://github.com/timechess/TheoremForge}{here}.

Figures (9)

• Figure 1: Schematic overview of the formalization workflow and its five sub-tasks.
• Figure 2: Statement Formalization Workflow. The pipeline consists of three phases: 1) Information Preprocessing for normalization and definition retrieval; 2) Expert Model Sampling for candidate generation and compilation checks; and 3) Statement Filtering for semantic verification via LLM-as-Judge and final selection.
• Figure 3: Proof Generation Workflow. The process comprises two phases. 1) Expert Model Sampling is where an expert model is invoked to generate a proof. A general-purpose LLM attempts to rectify the errors if all candidates fail. 2) Subgoal Decomposition is where a proof sketch is generated and the problem is decomposed into subgoals.
• Figure 4: (a) This figure illustrates the cost–performance comparison across different models, where models located in the upper-left region achieve a more favorable balance. The average cost is calculated by Total Cost / Number of Verified Problem. (b) This figure compares models by the cumulative number of verified problems as a function of per-problem token consumption, revealing their efficiency under limited computational budgets.
• Figure 5: Data collection statistics for the five sub-tasks. The stacked bars distinguish between samples derived from fully successful trajectories (bottom) and valid samples extracted from intermediate steps of failed trajectories (top). The latter reveals data yield improvements by decoupled extraction..