PuzzleClone: An SMT-Powered Framework for Synthesizing Verifiable Data

TL;DR

PuzzleClone introduces a scalable SMT-based framework for generating large, diverse, and verifiable logical puzzles to enhance the reasoning abilities of large language models, significantly improving their performance on related benchmarks.

Contribution

It presents a novel formal framework for synthesizing verifiable puzzles at scale using SMT, including encoding, randomization, and validation techniques, and demonstrates its effectiveness in improving LLM reasoning.

Findings

Generated over 83K validated puzzles with diverse formats and difficulty levels.

Training on PuzzleClone data significantly improves LLM performance on logic benchmarks.

Post training increases PuzzleClone scores from 14.4 to 56.2 and boosts other benchmarks by up to 12.5 points.

Abstract

High-quality mathematical and logical datasets with verifiable answers are essential for strengthening the reasoning capabilities of large language models (LLMs). While recent data augmentation techniques have facilitated the creation of large-scale benchmarks, existing LLM-generated datasets often suffer from limited reliability, diversity, and scalability. To address these challenges, we introduce PuzzleClone, a formal framework for synthesizing verifiable data at scale using Satisfiability Modulo Theories (SMT). Our approach features three key innovations: (1) encoding seed puzzles into structured logical specifications, (2) generating scalable variants through systematic variable and constraint randomization, and (3) ensuring validity via a reproduction mechanism. Applying PuzzleClone, we construct a curated benchmark comprising over 83K diverse and programmatically validated puzzles. The generated puzzles span a wide spectrum of difficulty and formats, posing significant challenges to current state-of-the-art models. We conduct post training (SFT and RL) on PuzzleClone datasets. Experimental results show that training on PuzzleClone yields substantial improvements not only on PuzzleClone testset but also on logic and mathematical benchmarks. Post training raises PuzzleClone average from 14.4 to 56.2 and delivers consistent improvements across 7 logic and mathematical benchmarks up to 12.5 absolute percentage points (AMC2023 from 52.5 to 65.0). Our code and data are available at https://github.com/HiThink-Research/PuzzleClone.