PuzzleClone: An SMT-Powered Framework for Synthesizing Verifiable Data

• URL: http://arxiv.org/abs/2508.15180v2
• Date: Mon, 25 Aug 2025 17:16:00 GMT
• Title: PuzzleClone: An SMT-Powered Framework for Synthesizing Verifiable Data
• Abstract summary: We introduce PuzzleClone, a framework for verifiable data at scale using Satisfiabilityo synthesizing (SMT)<n>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.
• Score: 7.63617172069015
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Recurrent Reasoning on Symbolic Puzzles with Sequence Models [3.900695166480356]
  We introduce RecurrReason, a difficulty-controlled benchmark of four recurrent logic puzzles.<n>We benchmark two Transformer families, an encoder-decoder model (T5-style) and a decoder-only model (GPT-2-style)<n>Fine-tuned pre-trained T5 achieves 97.27% validation and 81.00% OOD accuracy on Block World; all models score 0.00% on River Crossing under all conditions.
  arXiv  Detail & Related papers  (2026-04-19T15:48:32Z)
• S3-CoT: Self-Sampled Succinct Reasoning Enables Efficient Chain-of-Thought LLMs [48.80914119283909]
  Large language models equipped with chain-of-thought (CoT) achieve strong performance and offer a window into behavior.<n>Recent evidence suggests that improvements in CoT capabilities often come with redundant reasoning processes.<n>Our study presents a self-sampling framework based on activation steering for efficient CoT learning.
  arXiv  Detail & Related papers  (2026-02-02T11:37:36Z)
• Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training [24.74642687780046]
  We introduce Spark-Prover-X1, a 7B parameter model trained via a three-stage framework to unlock the reasoning potential of moderately-sized LLMs.<n>Key innovation is a "CoT-augmented state prediction" task to achieve fine-grained reasoning.<n>We also introduce ExamFormal-Bench, a new benchmark dataset of 402 formal problems.
  arXiv  Detail & Related papers  (2025-11-17T06:44:02Z)
• Staying in the Sweet Spot: Responsive Reasoning Evolution via Capability-Adaptive Hint Scaffolding [59.60915947702282]
  Reinforcement learning with verifiable rewards (RLVR) has achieved remarkable success in enhancing the reasoning capabilities of large language models (LLMs)<n>Existing RLVR methods often suffer from exploration inefficiency due to mismatches between the training data's difficulty and the model's capability.<n>We propose SEELE, a novel supervision-aided RLVR framework that dynamically adjusts problem difficulty to stay within the high-efficiency region.
  arXiv  Detail & Related papers  (2025-09-08T17:36:21Z)
• Teaching LLM to Reason: Reinforcement Learning from Algorithmic Problems without Code [76.80306464249217]
  We propose TeaR, which aims at teaching LLMs to reason better.<n>TeaR leverages careful data curation and reinforcement learning to guide models in discovering optimal reasoning paths through code-related tasks.<n>We conduct extensive experiments using two base models and three long-CoT distillation models, with model sizes ranging from 1.5 billion to 32 billion parameters, and across 17 benchmarks spanning Math, Knowledge, Code, and Logical Reasoning.
  arXiv  Detail & Related papers  (2025-07-10T07:34:05Z)
• PuzzleWorld: A Benchmark for Multimodal, Open-Ended Reasoning in Puzzlehunts [47.92619068073141]
  We introduce PuzzleWorld, a large-scale benchmark of 667 puzzlehunt-style problems designed to assess step-by-step, open-ended, and creative multimodal reasoning.<n>Most state-of-the-art models achieve only 1-2% final answer accuracy, with the best model solving only 14% of puzzles and reaching 40% stepwise accuracy.<n>Our error analysis reveals that current models exhibit myopic reasoning, are bottlenecked by the limitations of language-based inference, and lack sketching capabilities crucial for visual and spatial reasoning.
  arXiv  Detail & Related papers  (2025-06-06T16:17:09Z)
• SPaRC: A Spatial Pathfinding Reasoning Challenge [7.140449861888235]
  SPaRC is a dataset of 1,000 2D grid pathfinding puzzles to evaluate spatial and symbolic reasoning.<n>Humans achieve near-perfect accuracy (98.0%; 94.5% on hard puzzles), while the best reasoning models, such as o4-mini, struggle (15.8%; 1.1% on hard puzzles)
  arXiv  Detail & Related papers  (2025-05-22T13:53:50Z)
• Mind the Gap: Bridging Thought Leap for Improved Chain-of-Thought Tuning [54.65050470296886]
  We propose the CoT Thought Leap Bridge Task, which aims to automatically detect leaps and generate missing intermediate reasoning steps.<n>We demonstrate that models fine-tuned on bridged datasets consistently outperform those trained on original datasets.<n>Our approach effectively enhances distilled data and provides better starting points for reinforcement learning.
  arXiv  Detail & Related papers  (2025-05-20T17:59:31Z)
• Nemotron-CrossThink: Scaling Self-Learning beyond Math Reasoning [66.43194385702297]
  Large Language Models (LLMs) have shown strong reasoning capabilities, particularly when enhanced through Reinforcement Learning (RL)<n>We propose NEMOTRON-CROSSTHINK, a framework that systematically incorporates multi-domain corpora, including both synthetic and real-world question-answer pairs, into RL training to improve generalization across diverse reasoning tasks.
  arXiv  Detail & Related papers  (2025-04-15T21:37:13Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  Recent advances in large language models (LLMs) have improved their performance on coding benchmarks.<n>However, improvement is plateauing due to the exhaustion of readily available high-quality data.<n>We propose Sol-Ver, a self-play solver-verifier framework that jointly improves a single model's code and test generation capacity.
  arXiv  Detail & Related papers  (2025-02-20T18:32:19Z)
• Navigating the Labyrinth: Evaluating LLMs' Ability to Reason About Search Problems [62.76627483915117]
  Large Language Models (LLMs) have recently achieved impressive performance in math and reasoning benchmarks.<n>We introduce a new benchmark, SearchBench, which contains 11 unique search problems inspired by intuitive puzzles.<n>We show that using step-by-step, language-only reasoning, even the most advanced LLMs fail to solve SearchBench.
  arXiv  Detail & Related papers  (2024-06-18T00:44:58Z)
• Exploring Mathematical Extrapolation of Large Language Models with Synthetic Data [7.52830790706506]
  We show that the model can perform well on multi-step reasoning tasks via fine-tuning on high-quality synthetic data. Experimental results with the open-llama-3B model on three different test datasets show that the model can reach a zero-shot pass@1 at 0.44.
  arXiv  Detail & Related papers  (2024-06-04T08:30:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.