Synthetic Proofs with Tool-Integrated Reasoning: Contrastive Alignment for LLM Mathematics with Lean (2025)

Abstract: Modern mathematical reasoning benchmarks primarily focus on answer finding rather than proof verification, creating a gap in evaluating the proving capabilities of large language models (LLMs). We present a methodology for generating diverse mathematical proof tasks using formal tools. Our approach combines Lean-based synthetic problem generation with a Tool-Integrated Reasoning (TiR) framework for partial (sampling-based) proof validation, and it uses contrastive preference optimization to align the model’s proof outputs. Experiments on the Qwen-2.5 family of models demonstrate meaningful improvements in mathematical reasoning, particularly for smaller models. Our aligned models achieve up to a 57% higher success rate than baselines on the MiniF2F benchmark (across 0.5B, 1.5B, and 7B parameter models). These results highlight the potential of synthetic data and integrated validation for advancing LLM-based mathematical reasoning.

## introduction mathematical reasoning is a fundamental challenge for artificial intelligence. despite significant advances in large language models @xcite @xcite , achieving robust proof-solving capabilities comparable to human mathematicians remains elusive. a core difficulty lies in the vast search space of proofs: any given statement can spawn an enormous graph of conjectures and implications. exhaustive search in this space is infeasible -formal proof attempts like alphaproof @xcite ) can be computationally expensive at scale for complex problems. recent approaches using llms show promise in their flexibility and reasoning ability. however, even models that excel at answer-focused tasks (e.g., the math benchmark @xcite ) often struggle with formal proofs and higher-level mathematical reasoning @xcite . this gap calls for methodologies that combine the adaptability of llms with the rigor of structured verification. the contributions of this paper are as follows: in our pipeline, lean primarily serves as a generation and structuring environment: it provides statements, neighborhood relations, and hints that scaffold synthesis. model outputs are informal proofs. we rely on tir and an llm judge as probabilistic filters at scale; comprehensive formal checking in lean is used only in a limited way here and is left to future work. our experiments with qwen-2.5 models @xcite (0.5b-7b parameters) demonstrate significant improvements in mathematical reasoning, particularly for smaller models. these results highlight the potential of combining structured generation with flexible validation to advance mathematical reasoning in ai systems. ## background formal theorem proving has traditionally relied on search-based methods in proof assistants. tools like lean's aesop tactic @xcite and the hypertree proof search algorithm @xcite ) can systematically explore proofs but struggle with the combinatorial explosion of possibilities in complex problems. more recently, large language models have been applied to theorem proving @xcite , but purely data-driven approaches still face challenges unless guided by formal structure. synthetic data generation has shown promise: for instance, al-phageometry @xcite trained an llm on two million procedurally generated geometry problems, yielding impressive problem-solving performance. aligning llm outputs with desired solutions often requires learning from preferences. reinforcement learning from human feedback (rlhf) @xcite showed that human feedback can effectively steer model behavior, and direct preference optimization (dpo) @xcite achieved this without a separate reward model. recent contrastive approaches led to the simple preference optimization (simpo) @xcite framework, which introduces a margin γ to ensure the model scores a preferred output higher than a dispreferred one by at least a fixed gap. this margin-based criterion is wellsuited for mathematical proofs, where distinguishing correct reasoning from subtly flawed reasoning is essential; alternative preference objectives and recipes include kto @xcite , lmsi @xcite , orpo @xcite , and ppo @xcite . another complementary direction is integrating external tools into the reasoning loop. tool-integrated reasoning @xcite agents allow an llm to call formal solvers or checkers during problem solving. we build on this idea by using formal environment checks to partially verify generated conjectures and proofs without requiring complete formalization. self-improving systems represent another promising direction, with recent work focusing on agents that enhance their mathematical capabilities by autonomously generating and filtering their own proofs @xcite @xcite , complemented by intrinsic motivation algorithms like minimo @xcite for exploring infinite action spaces without predefined goals. current evaluation methodologies present significant limitations; standard benchmarks @xcite typically rely on answer-matching approaches that fail to validate reasoning steps, while formal proof benchmarks such as putnambench and minif2f @xcite offer more rigorous assessment environments with varying difficulty distributions -putnambench featuring exceptionally challenging problems and minif2f providing a broader range suitable for evaluating models across different skill levels -though they still require bridging the gap between natural language reasoning and formal representations. ## training framework using the synthetic data and validation techniques above, we construct training pairs for contrastive alignment. for each problem x, we obtain a correct proof y w (verified by tir) and a corresponding incorrect proof y l (generated via the strategies in section 3.3). we then fine-tune the model using a simpo-based objective, which encourages the model to assign higher probability to y w over y l . the training loss follows the simpo formula-tion: ## scope and external validity our empirical scope is intentionally narrow (qwen-2.5, minif2f) to isolate pipeline effects. the components of our method (problem synthesis, tir filtering, contrastive alignment) are model-agnostic; we expect transfer across families with two practical considerations: (i) evaluation -complementing the llm judge with selective formal checking on representative subsets; (ii) domain coverageextending e and validators beyond algebra/number theory (e.g., geometry and graphs require domainspecific generators and metamorphic tests). ## conclusion our study demonstrates that combining synthetic proof generation with partial formal validation can substantially bolster an llm's mathematical reasoning abilities. in particular, training on generated conjecture-proof pairs (with contrastive alignment) enabled even relatively small models to solve significantly more formal problems. this work represents a step toward ai systems that can not only generate and verify mathematical proofs but also gradually improve their own reasoning strategies. to support reproducibility and accelerate progress in mathematical reasoning research, we will release our complete synthetic dataset of 30,000 problems and the tool-integrated reasoning framework under open-source licenses. this includes the tree-based generation algorithms, validation mechanisms, and alignment methodology described in this paper. in future work, we plan to enhance the synthetic generation process with chain-of-thought prompting to further improve conjecture quality, extend our framework to other domains such as geometry (which may require specialized validation techniques), strengthen the integration between llm reasoning and formal verification (improving the tir framework), and investigate more efficient training strategies to scale to larger models.