This repository supports research on solving KenKen puzzles with both vision-language models (VLMs) and a custom neuro-symbolic pipeline. The project creates a synthetic KenKen board dataset, renders puzzle images from symbolic puzzle definitions, solves board images with a vision model plus constraint satisfaction, and evaluates VLMs on the same puzzle set.
The work is organized around three goals:
- Generate valid KenKen puzzles and store their mathematical representations.
- Convert those symbolic puzzles into board images for visual reasoning experiments.
- Compare direct VLM puzzle-solving performance against a neuro-symbolic solver that combines image understanding with a Z3 constraint solver.
Paper link, Co-authored with Ben Wooding: https://link.springer.com/chapter/10.1007/978-3-032-32357-6_9
.
├── SymbolicPuzzleGenerator.ipynb # Generates valid KenKen puzzles and symbolic cage definitions
├── BoardImageGeneration.ipynb # Renders puzzle images from symbolic puzzle data
├── NeuroSymbolicSolver.ipynb # Vision + constraint-satisfaction solver pipeline
├── GPTEvaluation.ipynb # GPT VLM evaluation
├── GeminiEvaluation.ipynb # Gemini VLM evaluation
├── ClaudeEvaluation.ipynb # Claude VLM evaluation
├── QwenEvaluation.ipynb # Qwen VLM evaluation
├── AnalyzingResults.ipynb # Aggregates and visualizes model results
├── board_images/ # 430 synthetic generated KenKen boards of sizes n = 3-7
├── puzzles/
│ └── puzzles_dict.json # Symbolic mathematical representations of generated puzzles
├── symbols/
│ ├── TMNIST_NotoSans.csv # Digit glyph data used when rendering puzzle clues
│ └── operators/ # Operation symbols used in generated board images
├── models/ # Model weights for the custom solver, tracked with Git LFS when present
└── results/ # Evaluation CSVs, one per model or solver
Some large artifacts are expected to be present locally but may not be tracked in Git. In particular, models/ should contain trained model weights such as character-recognition and grid-detection weights. The repository is configured to track .pth files with Git LFS.
SymbolicPuzzleGenerator.ipynb builds a dataset of valid KenKen puzzles using symbolic constraints. Each puzzle is represented as cages with cell coordinates, a target value, and an operation such as addition, subtraction, multiplication, or division. These representations are saved in puzzles/puzzles_dict.json and serve as the ground truth for both rendering and evaluation.
BoardImageGeneration.ipynb turns the symbolic puzzle data into rendered board images. It draws grid lines and cage borders, inserts target numbers from the TMNIST digit data, and inserts operator symbols from symbols/operators/.
NeuroSymbolicSolver.ipynb implements the custom solver. It uses vision models to detect the grid size and classify rendered clue characters, reconstructs the symbolic puzzle representation from the image, and solves the resulting constraints with Z3.
The VLM evaluation notebooks prompt models directly with puzzle board images and ask for a completed grid. Candidate solutions are parsed from model responses and validated against the ground-truth symbolic puzzle constraints with Z3.
The results/ folder should contain one CSV per evaluated model or solver, for example:
results/
├── claude_evaluation.csv
├── gemini_evaluation.csv
├── gpt_evaluation.csv
├── qwen_evaluation.csv
└── neurosymbolic_solver.csv
Each CSV records performance by puzzle size, including accuracy and average response or solve time. AnalyzingResults.ipynb loads these files to compare VLM performance against the custom neuro-symbolic solver.
- Puzzle sizes in the notebooks are primarily 3x3 through 7x7.
- API-backed VLM notebooks require the corresponding provider credentials in the local environment.
- Large model weights should live in
models/and be managed through Git LFS rather than committed directly.