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

TL;DR

This paper introduces WARP, a neurosymbolic approach that enhances large language models' ability to analyze worst-case symbolic constraints in code, improving their capacity for symbolic reasoning and vulnerability detection.

Contribution

The paper presents WARP, a novel neurosymbolic framework combining program analysis and LLMs to generalize worst-case constraints to larger inputs, advancing symbolic reasoning in LLMs.

Findings

WARP improves worst-case constraint reasoning performance.

Reinforcement learning fine-tunes LLMs to better handle symbolic constraints.

WARP-1.0-3B outperforms larger baseline models.

Abstract

Large language models (LLMs) have demonstrated strong performance on coding tasks such as generation, completion and repair, but their ability to handle complex symbolic reasoning over code still remains underexplored. We introduce the task of worst-case symbolic constraints analysis, which requires inferring the symbolic constraints that characterise worst-case program executions; these constraints can be solved to obtain inputs that expose performance bottlenecks or denial-of-service vulnerabilities in software systems. We show that even state-of-the-art LLMs (e.g., GPT-5) struggle when applied directly on this task. To address this challenge, we propose WARP, an innovative neurosymbolic approach that computes worst-case constraints on smaller concrete input sizes using existing program analysis tools, and then leverages LLMs to generalise these constraints to larger input sizes. Concretely, WARP comprises: (1) an incremental strategy for LLM-based worst-case reasoning, (2) a solver-aligned neurosymbolic framework that integrates reinforcement learning with SMT (Satisfiability Modulo Theories) solving, and (3) a curated dataset of symbolic constraints. Experimental results show that WARP consistently improves performance on worst-case constraint reasoning. Leveraging the curated constraint dataset, we use reinforcement learning to fine-tune a model, WARP-1.0-3B, which significantly outperforms size-matched and even larger baselines. These results demonstrate that incremental constraint reasoning enhances LLMs' ability to handle symbolic reasoning and highlight the potential for deeper integration between neural learning and formal methods in rigorous program analysis.