Technical Summary: Counterexample Guided Learning in the Large using Reasoning Agents

Problem Statement

The paper addresses the challenge of enabling Large Language Models (LLMs) and agents to effectively learn and adapt from feedback. While feedback is critical for coding agents, tool users, and personalized assistants, measuring and improving a model's ability to utilize feedback is difficult due to the heterogeneity, domain-specificity, and lack of controllability in typical feedback mechanisms.

To create a controllable testbed for this capability, the authors focus on regular-expression (regex) induction. This is a classical symbolic learning problem where the goal is to infer a regular expression (the target language $L^\star$) from a set of labeled strings (positive and negative examples). The task is inherently challenging because many candidate expressions can fit a small set of examples, leading to overfitting on superficial patterns. The authors frame this as an oracle-guided symbolic generation problem, where an LLM (the learner) iteratively refines its hypothesis based on feedback from a verifier (the teacher) in the form of counterexamples.

Methodology

The proposed framework integrates LLMs with a teacher-learner loop, enhanced by agentic workflows. The system operates through the following components:

1. Teacher-Learner Iterative Framework

• Learner: An LLM proposes a candidate regular expression based on the current set of labeled examples.
• Teacher: A verifier checks the candidate against the target language. Since regular language equivalence is decidable, the teacher constructs the symmetric difference $L(\hat{r}) \triangle L^\star$ between the candidate and the target.
• Feedback: If the candidate is incorrect, the teacher returns counterexamples (strings that should be in the target but are not, or vice versa). These are added to the training set for the next round.

2. Counterexample Synthesis and Clustering

To manage the potentially infinite number of counterexamples (especially those arising from Kleene stars/loops), the authors introduce Clustered Counterexamples:

• Instead of returning individual strings, the teacher analyzes the minimized difference automaton.
• It groups outgoing symbols from a state that lead to the same destination state into "super-characters" (e.g., representing $\{A, \dots, Z, a, \dots, z\}$ as $[A-Za-z]$).
• A clustered counterexample is a path in this automaton using these super-characters, representing a set of concrete strings that share the same failure mode. This provides a more systematic and less redundant view of the error region.

3. Agentic Workflow

The framework lifts the standard teacher-learner loop into an agentic workflow comprising two loops:

• Outer Loop (Reflection): The LLM is prompted to reflect on previous attempts. It receives the previous hypothesis, its reasoning trace, and new counterexamples. The model is instructed to explain what failed and how to revise the hypothesis.
• Inner Loop (Repair): To ensure consistency, the system employs a repair loop. It repeatedly queries the LLM to generate candidates that satisfy:
  1. Syntax Check: The regex must be syntactically valid.
  2. Satisfaction Check: The regex must correctly label all accumulated counterexamples.
  • A RepairScore function evaluates candidates based on compilation success and the fraction of misclassified examples, selecting the best candidate from multiple retries.

4. Regularization

To prevent the LLM from generating overly specific or complex expressions that fit the current sample set but fail generally, the system employs prompt-level regularization. This includes constraints on maximum expression length, nesting depth of operators, and a bias toward simpler hypotheses.

Key Contributions

1. Oracle-Guided Formulation: The paper formulates LLM-based regex induction as an iterative symbolic learning problem where hypotheses are refined via counterexample feedback, bridging the gap between traditional program synthesis (CEGIS) and modern LLM inference.
2. Active Learning Methodology: It introduces techniques for building effective LLM-based active learners, specifically symbolic counterexample clustering and regularization to prioritize simpler, more plausible hypotheses.
3. Agentic Workflow: The authors develop a novel agentic framework utilizing reflection (to extract structural implications of errors) and iterative repair loops to revise failed hypotheses, moving beyond simple prompt-driven generation.
4. Rigorous Evaluation: The study provides a comprehensive evaluation across two datasets (Simple and Extended Regex) and multiple backbone models, analyzing performance dynamics, sample efficiency, and the impact of specific components.

Results

The authors evaluated their framework on two datasets: Simple Regex (standard operators over $\{a, b, c\}$) and Extended Regex (supporting intersection, negation, and complex quantifiers).

• Performance Gains: On the most difficult tasks (high StarDepth), the counterexample-guided framework significantly outperformed standard prompting.
  • On Simple Regex (StarDepth 4), success rates improved from 3.2% (Standard) to 38.1% (Agentic).
  • On Extended Regex (StarDepth 2), success rates improved from 38.9% (Standard) to 74.1% (Agentic).
• Sample Efficiency: Counterexample-guided learning substantially reduced the number of labeled examples required to reach a target accuracy compared to methods using randomly sampled examples.
• Component Analysis:
  • Clustered Counterexamples: Consistently outperformed non-clustered (individual string) counterexamples, indicating that the quality and systematic coverage of feedback matter more than just the volume.
  • Agentic vs. Single: The full agentic workflow (with reflection and repair) consistently outperformed single-inference approaches using the same counterexamples, though at a higher token cost.
  • Model Agnosticism: The improvements were observed across various backbone models (Qwen3, GPT-5.4 variants, GPT-oss), suggesting the framework is robust to model choice.
  • Ablation: While regularization helped prevent early overfitting, the repair loop provided the largest performance gains. Reflection contributed to success but was less critical than the repair mechanism.

Significance and Claims

The paper claims that LLMs can benefit from rich feedback beyond treating it as additional data. By treating feedback as a structured, iterative signal (counterexamples) rather than static training data, LLMs can engage in robust, verifier-guided refinement.

The authors position this work as a step toward robust verifier-guided methods for LLM-based program synthesis and formal reasoning. They argue that in domains where informative failures can be synthesized (verifiable domains), agents can move beyond merely fitting examples to performing reliable iterative refinement. The study suggests that the combination of symbolic verification (counterexamples) and agentic reasoning (reflection/repair) creates a synergy that allows LLMs to solve complex symbolic induction tasks that standard prompting fails to address.