Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models

• URL: http://arxiv.org/abs/2506.08171v1
• Date: Mon, 09 Jun 2025 19:33:30 GMT
• Title: Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models
• Authors: Daniel Koh, Yannic Noller, Corina S. Pasareanu, Adrians Skapars, Youcheng Sun,
• Abstract summary: Large language models (LLMs) have been successfully applied to a variety of coding tasks, including code generation, completion, and repair.<n>This paper investigates the capacity of LLMs to reason about worst-case executions in programs through symbolic constraints analysis.
• Score: 11.612762531670212
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have been successfully applied to a variety of coding tasks, including code generation, completion, and repair. However, more complex symbolic reasoning tasks remain largely unexplored by LLMs. This paper investigates the capacity of LLMs to reason about worst-case executions in programs through symbolic constraints analysis, aiming to connect LLMs and symbolic reasoning approaches. Specifically, we define and address the problem of worst-case symbolic constraints analysis as a measure to assess the comprehension of LLMs. We evaluate the performance of existing LLMs on this novel task and further improve their capabilities through symbolic reasoning-guided fine-tuning, grounded in SMT (Satisfiability Modulo Theories) constraint solving and supported by a specially designed dataset of symbolic constraints. Experimental results show that our solver-aligned model, WARP-1.0-3B, consistently surpasses size-matched and even much larger baselines, demonstrating that a 3B LLM can recover the very constraints that pin down an algorithm's worst-case behaviour through reinforcement learning methods. These findings suggest that LLMs are capable of engaging in deeper symbolic reasoning, supporting a closer integration between neural network-based learning and formal methods for rigorous program analysis.

Related papers

• Discrete Tokenization for Multimodal LLMs: A Comprehensive Survey [69.45421620616486]
  This work presents the first structured taxonomy and analysis of discrete tokenization methods designed for large language models (LLMs)<n>We categorize 8 representative VQ variants that span classical and modern paradigms and analyze their algorithmic principles, training dynamics, and integration challenges with LLM pipelines.<n>We identify key challenges including codebook collapse, unstable gradient estimation, and modality-specific encoding constraints.
  arXiv  Detail & Related papers  (2025-07-21T10:52:14Z)
• Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
  Large Language Models (LLMs) have rapidly transformed the landscape of artificial intelligence.<n>Their reliance on probabilistic inference limits their effectiveness in domains requiring strict logical reasoning.<n>This paper proposes a neurosymbolic approach that augments LLMs with logic-based reasoning modules.
  arXiv  Detail & Related papers  (2025-06-29T22:03:01Z)
• LogicPuzzleRL: Cultivating Robust Mathematical Reasoning in LLMs via Reinforcement Learning [29.047063129464494]
  Large language models (LLMs) excel at many supervised tasks but often struggle with structured reasoning unfamiliar settings.<n>This discrepancy suggests that standard fine-tuning pipelines may instill narrow, domain-specifics rather than fostering general-purpose thinking strategies.<n>We propose a "play to learn" framework that fine-tunes LLMs through reinforcement learning on a suite of seven custom logic puzzles.
  arXiv  Detail & Related papers  (2025-06-05T09:40:47Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  Computational Thinking Model (CTM) is a novel framework that incorporates computational thinking paradigms into large language models (LLMs)<n>Live code execution is seamlessly integrated into the reasoning process, allowing CTM to think by computing.<n>CTM outperforms conventional reasoning models and tool-augmented baselines in terms of accuracy, interpretability, and generalizability.
  arXiv  Detail & Related papers  (2025-06-03T09:11:15Z)
• CrossWordBench: Evaluating the Reasoning Capabilities of LLMs and LVLMs with Controllable Puzzle Generation [53.452699232071495]
  CrossWordBench is a benchmark designed to evaluate the reasoning capabilities of Large Language Models (LLMs) and Large Vision-Language Models (LVLMs) through the medium of crossword puzzles.<n>Our evaluation reveals that reasoning LLMs outperform non-reasoning models substantially by effectively leveraging crossing-letter constraints.<n>Our findings offer insights into the limitations of the reasoning capabilities of current LLMs and LVLMs, and provide an effective approach for creating multimodal constrained tasks for future evaluations.
  arXiv  Detail & Related papers  (2025-03-30T20:03:36Z)
• ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning [92.76959707441954]
  We introduce ZebraLogic, a comprehensive evaluation framework for assessing LLM reasoning performance.<n>ZebraLogic enables the generation of puzzles with controllable and quantifiable complexity.<n>Our results reveal a significant decline in accuracy as problem complexity grows.
  arXiv  Detail & Related papers  (2025-02-03T06:44:49Z)
• Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis [9.865771016218549]
  This work presents a novel systematic methodology to analyse the capabilities and limitations of Large Language Models (LLMs)<n>The analysis is complexity-graded w.r.t. rule dependency structure, allowing quantification of specific inference challenges on LLM performance.
  arXiv  Detail & Related papers  (2024-08-15T16:41:00Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  Large Language Models (LLMs) have demonstrated impressive capability in many natural language tasks. LLMs are prone to produce errors, hallucinations and inconsistent statements when performing multi-step reasoning. We introduce Q*, a framework for guiding LLMs decoding process with deliberative planning.
  arXiv  Detail & Related papers  (2024-06-20T13:08:09Z)
• Investigating Symbolic Capabilities of Large Language Models [16.88906206735967]
  This study aims to bridge the gap by rigorously evaluating Large Language Models (LLMs) on a series of symbolic tasks. Our analysis encompasses eight LLMs, including four enterprise-grade and four open-source models, of which three have been pre-trained on mathematical tasks. The findings reveal a significant decline in LLMs' performance on context-free and context-sensitive symbolic tasks as the complexity, represented by the number of symbols, increases.
  arXiv  Detail & Related papers  (2024-05-21T21:24:34Z)
• Characterization of Large Language Model Development in the Datacenter [55.9909258342639]
  Large Language Models (LLMs) have presented impressive performance across several transformative tasks. However, it is non-trivial to efficiently utilize large-scale cluster resources to develop LLMs. We present an in-depth characterization study of a six-month LLM development workload trace collected from our GPU datacenter Acme.
  arXiv  Detail & Related papers  (2024-03-12T13:31:14Z)
• DiLA: Enhancing LLM Tool Learning with Differential Logic Layer [11.810200077863172]
  We propose a novel differential logic layer-aided language modeling (DiLA) approach, where logical constraints are integrated into the forward and backward passes of a network layer. We evaluate the performance of DiLA on two classic reasoning problems and empirically demonstrate its consistent outperformance against existing prompt-based and solver-aided approaches.
  arXiv  Detail & Related papers  (2024-02-19T07:38:57Z)
• Evaluating LLMs' Mathematical and Coding Competency through Ontology-guided Interventions [47.83142414018448]
  We focus on two popular reasoning tasks: arithmetic reasoning and code generation. We introduce (i) a general ontology of perturbations for math and coding questions, (ii) a semi-automatic method to apply these perturbations, and (iii) two datasets. We show a significant performance drop across all the models against perturbed questions.
  arXiv  Detail & Related papers  (2024-01-17T18:13:07Z)

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.