TLDR: PuzzleClone is a new framework that uses Satisfiability Modulo Theories (SMT) to automatically generate large, diverse, and verifiable datasets of logical and mathematical puzzles. It addresses the limitations of current LLM-generated data by encoding seed puzzles into structured specifications, randomizing variables and constraints, and ensuring validity through a reproduction mechanism. Training LLMs on the 83K+ puzzles generated by PuzzleClone significantly improves their logical and mathematical reasoning abilities on various benchmarks.
Large language models (LLMs) have shown impressive abilities in various tasks, but consistently strong logical reasoning remains a significant challenge. To improve this, researchers have created specialized benchmarks with difficult mathematical and formal logic problems. However, manually creating and validating these problems is time-consuming, leading to small and often similar datasets, which limits further progress.
A promising solution is data augmentation, where new problems are generated by modifying existing “seed” instances. Current methods often rely on LLMs to create, solve, and verify new problems. This approach, however, can lead to issues with data reliability, diversity, and scalability, as LLMs might produce flawed data, explore only a narrow range of variations, and incur high computational costs.
To address these challenges, a new framework called PuzzleClone has been introduced by Kai Xiong, Yanwei Huang, Rongjunchen Zhang, Kun Chen, and Haipang Wu. This formal framework uses Satisfiability Modulo Theories (SMT) to synthesize verifiable data on a large scale. PuzzleClone incorporates three main innovations:
Key Innovations of PuzzleClone
- Encoding seed puzzles into structured logical specifications.
- Generating numerous variations through systematic randomization of variables and constraints.
- Ensuring the validity of generated puzzles via a reproduction mechanism.
Using PuzzleClone, the researchers constructed a comprehensive benchmark dataset containing over 83,000 diverse and programmatically validated puzzles. These puzzles cover a wide range of difficulty levels and formats, presenting a substantial challenge for current state-of-the-art LLMs. The framework primarily focuses on SMT problems, which are a class of complex computational problems that many mathematical challenges can be reduced to.
How PuzzleClone Works
The data synthesis process in PuzzleClone involves three main stages:
1. Puzzle Encoding: Each original “seed” puzzle is manually translated into a structured problem specification using a specially designed Domain-Specific Language (DSL) and a configuration file. This DSL not only captures the core logic but also includes constraints specific to data augmentation, such as variable value ranges and the number of constraints.
2. Puzzle Generation: A puzzle generator then uses this specification to create new puzzles. It generates a Python script that randomly determines variables, conditions, and queries. Crucially, it leverages a symbolic SMT solver, Z3, to automatically derive the correct answers for each newly generated puzzle instance.
3. Config-based Answer Validation: To ensure the accuracy of the encoding process, PuzzleClone includes a validation step. A script is generated that can reproduce the original seed puzzle using its configuration, allowing for a deterministic reference answer to be computed and compared against the known ground-truth solution.
Dataset Construction and Evaluation
The PuzzleClone dataset was built through a multi-stage process to ensure quality, diversity, and verifiability. Seed puzzles were collected from various sources, including mathematics competitions and logical reasoning books. An LLM (Qwen2.5-72B-Instruct) was initially used to filter potential seeds based on their suitability for randomization and solvability by SMT solvers. Human experts then reviewed and enhanced these puzzles, adding complexity and diversity.
From 86 high-quality seed puzzles, PuzzleClone generated 1,000 variants for each, totaling 86,000 instances. A deduplication process was applied, comparing puzzle configurations rather than just surface-level text, resulting in 83,657 unique puzzles. The difficulty of each puzzle was assessed using a composite score based on factors like the number of logical symbols, constraints, description length, and the impact of variable domains.
Experiments showed that even advanced LLMs like ChatGPT-4o and DeepSeek-R1 found the PuzzleClone test set challenging. However, models like DeepSeek-R1-0528 and ChatGPT-o3 demonstrated strong performance. The research also highlighted that post-training (Supervised Fine-Tuning and Reinforcement Learning) on the PuzzleClone dataset significantly improved the logical reasoning capabilities of smaller LLMs, such as Qwen2.5-7B-Instruct. This model’s average score on PuzzleClone increased from 14.4 to 56.2 after SFT, and it showed consistent improvements across other logic and mathematical benchmarks.
Also Read:
- Unifying AI Reasoning: How a New Framework Enhances LLM Problem-Solving
- Crafting Consistent Physics Problems with AI: A New Approach
Future Directions
The creators of PuzzleClone envision several future enhancements, including automating puzzle enrichment by prompting LLMs to rephrase descriptions or propose new variables and constraints. Another goal is to enable LLMs to automatically construct formal specifications from puzzle texts, significantly reducing manual effort. Ultimately, the aim is to achieve seed-free puzzle generation, where puzzles are composed directly from a library of logical operators, potentially with human assistance for validation.
For more technical details and to access the code and data, you can visit the PuzzleClone research paper.
