Neurosymbolic Generation of Valid Cryptic Crosswords with Proof-Guided Clue Generation and Constraint Solver Driven Grid Construction

Cryptic crosswords are crossword puzzles where each clue contains both a semantic definition for the solution and a wordplay from which the solver should construct the solution, for instance, using anagrams, homophones or hidden words. As in a regular crossword, the solutions are also connected together in an interlinking grid. Generating puzzles that satisfy this complex set of linguistic and combinatorial constraints presents an interesting challenge for natural language processing. In this work, we evaluate the ability of LLMs to generate valid cryptic crosswords. We break this problem down into two tasks: clue generation, and grid construction and demonstrate both tasks are still beyond the current abilities of state-of-the-art LLMs. However, whilst LLMs alone cannot solve this problem, we show that by combining LLMs with a domain-specific proof language, a set of deterministic validation tools and a satisfiability solver, we can generate cryptic crossword puzzles that are both syntactically and semantically valid.