Counterexample Guided Learning in the Large using Reasoning Agents

This paper studies a simple but powerful idea: instead of asking a language model to produce an answer in one shot, pair it with a verifier that points out exactly where the answer is wrong. The authors frame the task as regular-expression induction - infer a regex that matches a target language from examples - because it is a clean setting where a checker can produce a concrete counterexample (a string the proposed regex gets wrong) rather than just a pass or fail signal.

The loop works like this: the LLM proposes a candidate regex, the verifier returns a counterexample showing a difference between the proposal and the target, and the model revises. The authors add refinement strategies including regularization and symbolic clustering, plus agentic techniques like reflection loops. The verifier feedback dramatically improves sample efficiency. On the hardest task groups, success rates climb from 3.2 percent to 38.1 percent, and on other regex domains from 38.9 percent to 74.1 percent - in cases where plain prompting essentially failed to learn complex target expressions at all.

The broader significance is methodological. It is more evidence that the bottleneck for LLM problem-solving is often not raw generation but the quality of the feedback signal. A verifier that explains the mistake teaches far more per attempt than a yes-or-no grade, which is why counterexample-guided and verification-driven approaches keep outperforming naive sampling on structured reasoning tasks. The work is authored by a group including Thomas Reps and Frederic Sala, drawing on the counterexample-guided synthesis tradition from formal methods.

Sources

Last verified June 15, 2026