Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Force GitHub README to respect dark mode (function() { var style = document.createElement('style'); style.textContent = ' .markdown-body { color-scheme: dark light; } .markdown-body pre { background: #161b22 !important; } .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; } .markdown-body table th, .markdown-body table td { border-color: #30363d !important; } .markdown-body img { background: #0d1117; } .markdown-body blockquote { border-left-color: #8b949e; } .markdown-body hr { border-color: #30363d; } '; document.head.appendChild(style); })(); } } catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Highlight search terms from Google/DuckDuckGo/Bing referrer (function() { var ref = document.referrer; var terms = []; if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) { var url = new URL(ref); var q = url.searchParams.get('q') || url.searchParams.get('p'); if (q) { terms = q.split(/\s+/).filter(function(t) { return t.length > 2; }); } } if (terms.length === 0) return; var style = document.createElement('style'); style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }'; document.head.appendChild(style); function highlight(node) { if (node.nodeType === 3) { // text node var text = node.textContent; var found = false; terms.forEach(function(term) { var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi'); if (regex.test(text)) { found = true; var frag = document.createDocumentFragment(); var parts = text.split(regex); parts.forEach(function(part, i) { if (i % 2 === 0) { frag.appendChild(document.createTextNode(part)); } else { var span = document.createElement('span'); span.className = 'userscript-highlight'; span.textContent = part; frag.appendChild(span); } }); node.parentNode.replaceChild(frag, node); } }); } else if (node.nodeType === 1 && node.childNodes) { // element var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT']; if (!skipTags.includes(node.tagName)) { Array.from(node.childNodes).forEach(highlight); } } } highlight(document.body); // Re-highlight on dynamic content var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1 || node.nodeType === 3) highlight(node); }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Strip utm_, fbclid, gclid, etc. from all links on page (function() { var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content', 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid', 'ref', 'ref_src', 'source', 'medium', 'campaign']; function cleanUrl(url) { try { var u = new URL(url, window.location.origin); var changed = false; trackingParams.forEach(function(p) { if (u.searchParams.has(p)) { u.searchParams.delete(p); changed = true; } }); return changed ? u.toString() : url; } catch (e) { return url; } } function cleanLinks() { document.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } cleanLinks(); var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1) { if (node.tagName === 'A') cleanLinks(); node.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); } })(); (function(){ try { var __m = "youtube.com"; var __re = new RegExp('^' + "youtube\\.com" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Auto-enable theater mode on YouTube (function() { function tryTheater() { var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]'); if (btn && !btn.classList.contains('activated')) { btn.click(); } } // Try immediately tryTheater(); // Try after navigation (SPA) var lastUrl = location.href; setInterval(function() { if (location.href !== lastUrl) { lastUrl = location.href; setTimeout(tryTheater, 500); } }, 1000); // Also try on player load var observer = new MutationObserver(tryTheater); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Remove or un-stick sticky/fixed headers that block content (function() { function unstick() { document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) { if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') { el.style.position = 'static'; el.style.top = 'auto'; el.style.zIndex = 'auto'; } }); } unstick(); var observer = new MutationObserver(unstick); observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] }); })(); } } catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + '
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Universal Dark Mode - works on any site (function() { var enabled = true; function applyDarkMode() { if (!enabled) return; // Create style element if it doesn't exist var style = document.getElementById('universal-dark-mode-style'); if (!style) { style = document.createElement('style'); style.id = 'universal-dark-mode-style'; document.head.appendChild(style); } // Dark mode CSS - inverts colors but preserves images/video style.textContent = ' /* Invert everything except media */ html { filter: invert(1) hue-rotate(180deg) !important; background: #1a1a2e !important; } /* Restore images, videos, iframes, canvas */ img, video, iframe, canvas, svg, picture, [style*="background-image"] { filter: invert(1) hue-rotate(180deg) !important; } /* Preserve specific elements that should not be inverted */ .no-dark-mode, .no-dark-mode *, [data-theme="light"], [data-theme="light"], .ace_editor, .ace_editor *, .CodeMirror, .CodeMirror *, .monaco-editor, .monaco-editor *, .markdown-body pre, .markdown-body pre *, .highlight, .highlight *, pre code, pre code * { filter: none !important; } /* Fix common UI elements */ .modal, .popup, .dropdown-menu, .tooltip, .popover { filter: invert(1) hue-rotate(180deg) !important; background: #2d2d44 !important; border-color: #444 !important; } /* Scrollbars */ ::-webkit-scrollbar { background: #1a1a2e !important; } ::-webkit-scrollbar-thumb { background: #444 !important; } ::-webkit-scrollbar-thumb:hover { background: #555 !important; } /* Selection */ ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; } ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; } '; } function removeDarkMode() { var style = document.getElementById('universal-dark-mode-style'); if (style) style.remove(); } // Toggle with Alt+Shift+D document.addEventListener('keydown', function(e) { if (e.altKey && e.shiftKey && e.key === 'D') { e.preventDefault(); enabled = !enabled; if (enabled) { applyDarkMode(); console.log('[Universal Dark Mode] Enabled'); } else { removeDarkMode(); console.log('[Universal Dark Mode] Disabled'); } } }); // Apply on load applyDarkMode(); // Re-apply on dynamic content var observer = new MutationObserver(function(mutations) { if (enabled && !document.getElementById('universal-dark-mode-style')) { applyDarkMode(); } }); observer.observe(document.head, { childList: true }); console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle'); })(); } } catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); } })(); })();
Skip to content

Repository files navigation

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

Kai Xiong1*, Yanwei Huang2*, Rongjunchen Zhang1♠, Kun Chen1, Haipang Wu1, Yingcai Wu3

1HiThink Research 2HKUST 3Zhejiang University
*Equal Contribution Corresponding Author

ACL 2026 Findings

[API Docs] | [Tutorials] | [Benchmark] | [Evaluation Toolkit]

LicensePython VersionGitHub stars


Overview of the PuzzleClone framework

Overview of the PuzzleClone framework.


Table of Contents


🧭 Overview

PuzzleClone is a data synthesis framework and comprehensive dataset for logical reasoning problems. It features:

  • Guaranteed Verifiability: Every problem is generated with a ground-truth solution and is formally verifiable via a symbolic solver or deterministic program execution, ensuring correctness.
  • 🎯 Granular Control: Offers fine-grained control over problem attributes like scale, structure, and difficulty through a set of adjustable parameters, enabling large-scale batch generation.
  • Flexible Adaptation: Facilitates the easy customization of problem scenarios and translation into different languages or domains.
  • 📊 Expansive and Diverse Coverage: Based on PuzzleClone, we have curated a benchmark including 83,657 unique logical reasoning puzzles procedurally generated from 86 seed questions. The dataset spans:
    • Various applications of Satisfiability Modulo Theories (SMT) and SMT-like puzzles,
    • Classic logical puzzles like Sudoku, the Knapsack problem, and linear optimization (LP).
    • Diverse mathematical problems of varying difficulties.
  • 🚀 State-of-the-Art Performance: Achieves SOTA results among open-source datasets, outperforming the public dataset by 18.4 points on SATBench (from 51.6 to 70.0).

📦 PC-83K Benchmark

Applying PuzzleClone, we construct PC-83K, a benchmark covering 83,657 unique logical reasoning puzzles. The generated puzzles span Satisfiability Modulo Theories (SMT), SMT-like reasoning tasks, classic puzzles such as Sudoku and knapsack, linear optimization, and diverse mathematical problems.

SplitSFTRL-TrainRL-ValTotal TrainTest
Normal2,16150,73843051,1685,730
Hard2,13923,61643024,0462,713
Sum4,30074,35486075,2148,443

Puzzle difficulty distribution

Puzzle difficulty distribution before and after deduplication.


📊 Benchmark Results

Current LLMs still show large gaps on complex logical reasoning. On PC-83K, stronger reasoning models achieve substantially higher accuracy, while post-training on PC-83K improves Qwen2.5-7B-Instruct from 14.5 to 66.0 average accuracy.

Baseline Performance on PC-83K (Click to Expand)
ModelNormalHardAvg.
ChatGPT-4o31.724.628.2
ChatGPT-o387.183.485.3
ChatGPT-591.186.388.7
Gemini-2.0-flash42.031.636.8
Gemini-2.5-pro75.867.271.5
Gemini-3-pro86.583.084.8
Claude-3.5-sonnet37.627.432.5
Claude-4-sonnet62.747.855.3
Seed1.687.882.485.1
GLM-Z1-9B-041463.653.558.6
GLM-Z1-32B-041471.160.966.0
Qwen2.5-7B-Instruct16.812.114.5
Qwen2.5-14B-Instruct24.317.921.1
Qwen2.5-32B-Instruct31.423.527.4
Qwen2.5-72B-Instruct32.825.329.0
Qwen3-8B71.659.465.5
Qwen3-14B78.667.072.8
Qwen3-32B77.068.172.5
Qwen3-235B-A22B82.973.878.3
DeepSeek-R1-Distill-Qwen-14B47.938.443.1
DeepSeek-R1-Distill-Qwen-32B53.343.248.3
DeepSeek-R1-0528-Qwen3-8B76.066.871.4
DeepSeek-R1-052888.782.685.6
Post-Training Results (Click to Expand)
ModelPC-83K NormalPC-83K HardPC-SL-35KSATBenchBBEH-miniAIME24AIME25AMC2023MATH500OlympiadBench
Qwen2.5-7B-Instruct16.812.19.651.611.313.36.752.575.241.0
SFT61.948.014.770.09.820.013.367.580.843.4
RL (PC-83K)71.061.015.262.017.016.713.365.080.044.4
SynLogic-7B----8.010.0-55.071.8-
RL (PC-SL-35K)22.014.355.358.416.523.310.062.579.842.4
RL (PC-83K+PC-SL-35K)64.854.154.257.217.016.716.760.080.452.2

Average accuracy grouped by seed puzzles

Average accuracy of evaluated models on the PuzzleClone test set, grouped by seed puzzle.


🔄 Data Synthesis Pipeline

PuzzleClone synthesizes data through three stages: puzzle encoding, puzzle generation, and config-based validation. Each seed puzzle is manually encoded into a DSL specification and a config file. The generator then produces randomized configs, renders new puzzle instances, computes reference answers, and validates correctness through deterministic reproduction.

PuzzleClone data synthesis pipeline

The data synthesis pipeline of PuzzleClone.


🛠️ Quick Start

Environment Setup

git clone https://github.com/HiThink-Research/PuzzleClone.git
cd PuzzleClone
pip install -r requirements.txt

Generate a Single Test Case

Run the translator in test mode to generate a sample question from a specification file:

python translator.py -t path/to/spec.yaml

The generated data ({spec_name}_data.jsonl) and debugging files such as {spec_name}_synthesizer.py are written to temp/.

Generate a Full Dataset

Run the translator in deployment mode to generate many puzzle instances:

python translator.py -d path/to/spec.yaml -o data.jsonl

If -o is omitted, the output is saved to output/{spec_name}_data.jsonl.

Apply a New Template

Use -g to load existing puzzle configs and render them with a new specification:

python translator.py -d path/to/new_spec.yaml -g old_data.jsonl -o new_data.jsonl

Data Transformation

Scripts in data_processing_scripts/ transform generated data into standard benchmark formats. See data_processing_scripts/README.md for details.

Evaluation

Use PolyhedronEvaluator for benchmark evaluation.


📚 Documentation


⚖️ License

Code License

This project is licensed under the Apache 2.0 License. See LICENSE for details.


📚 Citation

If you find PuzzleClone useful, please cite:

@inproceedings{xiong2026puzzleclone,
title = {PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
author = {Xiong, Kai and Huang, Yanwei and Zhang, Rongjunchen and Chen, Kun and Wu, Haipang and Wu, Yingcai},
booktitle = {ACL 2026 Findings},
year = {2026},
url = {https://github.com/HiThink-Research/PuzzleClone}
}

About

[ACL 2026] PuzzleClone: An SMT-Powered Framework for Synthesizing Verified Mathematical Reasoning Data

Topics

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages