Skip to content
AI.info

Research

A Solver-in-the-Loop Framework for Improving LLMs on Answer Set Programming for Logic Puzzle Solving

Overview Research area: Neuro-symbolic AI at the intersection of large language models and symbolic reasoning, specifically LLM code generation for the domain-specific language Answer Set Programming

A Solver-in-the-Loop Framework for Improving LLMs on Answer Set Programming for Logic Puzzle Solving
arXiv
2512.17093
Published
2025-12-18
Authors
Timo Pierre Schrader, Lukas Lange, Tobias Kaminski, Simon Razniewski, Annemarie Friedrich

AI summary

Overview

  • Research area: Neuro-symbolic AI at the intersection of large language models and symbolic reasoning, specifically LLM code generation for the domain-specific language Answer Set Programming (ASP).
  • Technical level: Intermediate. The paper introduces ASP concepts (rules, constraints, choice rules, answer sets) from scratch, but assumes familiarity with LLM fine-tuning, supervised fine-tuning (SFT), LoRA adapters, and best-of-N sampling.
  • Scope (one sentence): The paper proposes a solver-in-the-loop framework in which an ASP solver both filters LLM-generated partial ASP encodings into silver-standard training data and ranks candidate encodings at inference time, evaluated on grid-based logic puzzles in two prompting settings.

What This Paper Is About

LLMs are strong coding assistants for general-purpose languages such as Python, C++ and JavaScript, but they perform poorly on domain-specific languages, including ASP, largely because they saw few ASP examples during pre-training. This matters because ASP is an effective declarative approach for combinatorial search problems such as assignment, scheduling and configuration tasks, and domain experts who can describe such problems in natural language often cannot write ASP themselves.

The paper's goal is to make open-weight LLMs better at turning natural-language problem descriptions and hints into correct ASP encodings, using only problem specifications in natural language and their solutions, without any additional human annotations. The authors use grid-based logic puzzles as a proxy task because these reflect assignment problems, one of the main use cases of ASP.

Key Contributions

  1. Evidence that current open-weight LLMs struggle with ASP coding, even under a heavily prompt-engineered pipeline, while showing that a detailed prompt pipeline is not sufficient on its own.
  2. A fully automated method for creating silver-standard ASP training data: partial ASP encodings are sampled from an LLM and filtered by an ASP solver that checks for errors and for whether the ground-truth answer can still be derived; passing encodings are labelled "chosen" and failing ones "rejected".
  3. Supervised fine-tuning on the chosen instances improves open-weight LLMs of different sizes (8B to 70B) at generating ASP encodings for grid puzzles, especially on problems of higher complexity, in both a few-shot (two-shot) setting and a prompt-engineered pipeline setting.
  4. A solver-guided test-time procedure with a novel reward function and fallback mechanisms (regeneration and backtracking) that steers generation during inference and improves both trained open-weight models and the untrained closed-source GPT-4.1-mini.

Main Findings

  • Fine-tuning helps every model tested. All SFT-trained models outperform their untrained counterparts on ASP generation, which the authors attribute to the need for fine-tuning on underrepresented programming languages such as ASP.
  • The 70B model gains most. Llama-3.3 70B benefits heavily from training, with two-digit improvements in all settings; in the ablation on LogicPuzzles it moves from 31.0 (base) to 55.4 with SFT, a starting point for further test-time gains.
  • Small models can acquire ASP skills. The 8B models, which initially have essentially no usable ASP skills, improve by approximately 20pp–25pp on LogicPuzzles and 10pp on average on GridPuzzles after SFT on data automatically drawn from Llama-3.3 70B. Sampling ASP encodings from the 8B models themselves did not yield sufficient results.
  • Gains transfer to harder, unseen puzzle sizes. Similar increases appear on GridPuzzles, which the models were not specifically trained on and which contains puzzle sizes 3×4, 3×5, 4×4, 4×5 and 4×6 across easy, medium and hard difficulty levels.
  • Test-time search adds large gains. On LogicPuzzles with Llama-3.3 70B, best-of-N with regeneration and backtracking ("+Both (TT)") reaches 66.8 (Δ +11.4 over SFT), 65.1 at N=10 (Δ +9.7) and 69.2 at N=25 (Δ +13.8) across five runs.
  • Both fallback mechanisms are needed. Regeneration shows slight improvements of 2pp over basic best-of-5 sampling, while the combination of regeneration and backtracking yields a robust improvement of over 3pp.
  • More samples help, with a cost trade-off. Accuracy rises with N up to 69% at N=25, and the number of generated output tokens scales linearly with N; the authors conclude N=5 offers a good trade-off between cost efficiency and task performance in their setup.
  • Closed-source models benefit without training. GPT-4.1-mini (version

Authors’ abstract

The rise of large language models (LLMs) has sparked interest in coding assistants. While general-purpose programming languages are well supported, generating code for domain-specific languages remains a challenging problem for LLMs. In this paper, we focus on the LLM-based generation of code for Answer Set Programming (ASP), a particularly effective approach for finding solutions to combinatorial search problems. The effectiveness of LLMs in ASP code generation is currently hindered by the limited number of examples seen during their initial pre-training phase. In this paper, we introduce a novel ASP-solver-in-the-loop approach for solver-guided instruction-tuning of LLMs to addressing the highly complex semantic parsing task inherent in ASP code generation. Our method only requires problem specifications in natural language and their solutions. Specifically, we sample ASP statements for program continuations from LLMs for unriddling logic puzzles. Leveraging the special property of declarative ASP programming that partial encodings increasingly narrow down the solution space, we categorize them into chosen and rejected instances based on solver feedback. We then apply supervised fine-tuning to train LLMs on the curated data and further improve robustness using a solver-guided search that includes best-of-N sampling. Our experiments demonstrate consistent improvements in two distinct prompting settings on two datasets.

Read the original paper