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

Ch. 15. P. 195–202.

Obozov M., Diskin M., Beznosikov A., Alexander Gasnikov, Barannikov S.

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.

Keywords: formal verification, few-shot learning, Contrastive learning, synthetic data generation, mathematical nlp, tool integration

In book

Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025)

Suzhou: Association for Computational Linguistics, 2025.