Can Language Models Falsify? Evaluating Algorithmic Reasoning with Counterexample Creation
Authors: Shiven Sinha
Shashwat Goel
Ponnurangam Kumaraguru
Jonas Geiping
Matthias Bethge
Ameya Prabhu
Venue: COLM 2025 (2025)
Keywords: code; self-repair; falsification
TL;DR: We test the abilities of models to find counterexamples automatically using code-execution, and this can be hard for reasoning models.

Abstract: There is growing excitement about the potential of Language Models (LMs) to accelerate scientific discovery. *Falsifying* hypotheses is key to scientific progress, as it allows claims to be iteratively refined over time. This process requires significant researcher effort, reasoning, and ingenuity. Yet current benchmarks for LMs predominantly assess their ability to generate solutions rather than challenge them. We advocate for developing benchmarks that evaluate this inverse capability — creating counterexamples for subtly incorrect solutions. To demonstrate this approach, we start with the domain of algorithmic problem solving, where counterexamples can be evaluated automatically using code execution. Specifically, we introduce REFUTE, a dynamically updating benchmark that includes recent problems and incorrect submissions from programming competitions, where human experts successfully identified counterexamples. Our analysis finds that the best reasoning agents, even OpenAI o3-mini (high) with code execution feedback, can create counterexamples for only $<9$% of incorrect solutions in REFUTE, even though ratings indicate its ability to solve up to $48$% of these problems from scratch. We hope our work spurs progress in evaluating and enhancing LMs' ability to falsify incorrect solutions — a capability that is crucial for both accelerating research and making models self-improve through reliable reflective reasoning.

Published as a conference paper at COLM 2025
Can Language Models Falsify? Evaluating Algorithmic Reasoning with Counterexample Creation
Shiven Sinha? Shashwat Goel 2,3
Ponnurangam Kumaraguru'
Jonas Geiping 2,3,1 Matthias Bethge
Ameya Prabhu 4,50
MIT Hyderabad ELLIS Institute Tübingen
3 Max Planck Institute for Intelligent Systems
4 Tübingen Al Center
UUiveesityy of Tübingen
Abstract
There is growing excitement about the potential of Language Models (LMs) to accelerate scientific discovery. Falsifying hypotheses is key to scientific progress, as it allows claims to be iteratively refined over time. This process requires significant researcher effort, reasoning, and ingenuity. Yet current benchmarks for LMs predominantly assess their ability generate solu- tions rather than challenge them. We advocate for developing benchmarks that evaluate this inverse capability - creating counterexample for subtly incorrect solutions. To demonstrate this approach, we start with the domain algorithmic problem solving, where counterexamples can be evaluated automatically using code execution. Specifically, we introduce REFUTE, a dynamically updating benchmark that includes recent problems and incor- rect submissions from programming competitions, where human experts successfully identified counterexamples. Our analysis finds that the best reasoning agents, even OpenAl o3-mini (high) with code execution feed- back, can create counterexamples for only < 9% of incorrect solutions in REFUTE, even though ratings indicate its ability to solve up to 48% of these problems from scratch. We hope our work spurs progress in evaluating and enhancing LMs' ability to falsify incorrect solutions capability that is crucial for both accelerating research and making models self-improve through reliable reflective reasoning.
1 Introduction
Empirical science has evolved through an iterative process of new claims, falsification and subsequent refinement of these claims. Mathematicians too follow similar approach they propose conjectures and then invest substantial effort in search of counterexamples before attempting a proof. There has been growing interest in using language models (LMs) to accelerate research (Jumper et al., 2021; Lu et al., 2024), which is considered the next frontier for Al progress. Yet, most existing LM benchmarks focus on a model's ability to generale solutions to problems (Jimenez et al., 2024; Wijk et al., 2024; Phan et al., 2025). In this work, we highlight the need for benchmarks that test the inverse capability fulsification. Scientific hypotheses are considered falsified when concrete contrary evidence is presented (Popper, 2005). Researchers create counterexamples to claims by inspecting every step of argumentation and evidence, leveraging domain knowledge, epistemic uncertainty, reasoning and creative intuition. This process requires deep understanding of the problem, and is both challenging and time intensive. Thus, benchmarking counterexample creation can not only accelerate scientific discovery, but also rigorously test LM reasoning abilities.
However, a key challenge with creating such benchmarks is to verify whether a model's output is valíd counterexample to the claim. Traditional benchmarking by comparison with ground-truth reference solutions is insufficient - there could be many valid counterex- amples to a claim (Lakatos, 2015). In this paper, make initial progress in this direction,

---

Published as a conference paper at COLM 2025
Traditional Benchmark
Inverse Benchmark
Counterexample Generator
Counterexample
0-1 Knapsack
Given values weigghts, exceeding weight cop'.
ordedry picas highes value-censtty ttems ignore spacee utllionia
petence,
S8
neipht
ender
peteet 7
Imput constralidie L-.]
op Sky
J
knsprack(ttemss, cap) 8
correct knapsaakkfttsssss
Validation
maae st91 /x1t),
format t inpur constraints
incorrect output
Ne cap
valid countersxemilo
petam S9t.
Figure 1: While standard benchmarks for algorithmic reasoning require models to generate solutions, we propose an inverse benchmark to evaluate reasoning about correctness by falsifying incorrect solutions. To allow expressivity, we let the model output code that generates the counterexample input, and validate it by comparing the output of the incorrect solution with a held out correct solution.
by focusing on unstructured algorithmic problem solving, where counterexamples can be verified formally through code execution. Language models have already shown promise in solving algorithmic problems an expert level (Jain al., 2024; OpenAI, 2025). So we ask:
Can LMs create counterexamples for incorrect solutions to algorithmic problems?
To investigate this, we design a novel benchmark: REFUTE (Refuting Erroneous Findings Using Targeted Examples). Each sample in REFUTE contains: (i) detailed problem descrip- tion (including input constraints) and (ii) an incorrect solution. The task for LMs to create inputs satisfying the constraints, such that the given solution fails. The LM must generate program that prints such an input, and is allowed to use arbitrary programmatic constructs to this end (Figure 1).
We automatically source samples of incorrect submissions from Codeforces' contests in 2024 and 2025. These samples are search and contamination free Codeforces does not reveal non-trivial failure cases. We regularly update our benchmark to prevent indirect leakage due to potential overlap with training data, similar to LiveCodeBench (Jain et al., 2024). An automated pipeline to extensively filter samples ensures that counterexample discovery requires reasoning about the incorrect solution beyond random search. REFUTE contains 324 samples spanning diverse algorithmic topics with rich metadata annotations (Section 4).
We benchmark the current best models from five different model developers, ranked based on their accuracy at generating solutions to these problems on LiveCodeBench (Jain et al,, 2024). These include Ap o3-mini (high) and DeepSeek R1, which can generate cor- rect solutions for up to 50% of the problems in our benchmark based on reported Elo ratings. Yet, even with few-shot prompting with chain of thought and a ReAct agent scaffold (Yao et al., 2022) with code execution feedback, these models can only find counterexamples to < 9% of problems our dataset. Our results additionally demonstrate a prior hypothesis that LMs' ability to repair their own incorrect code is bottlenecked by their inability to find mistakes in their code (Gu et al., 2024; Olausson al., 2024). More broadly, our results demonstrate that verification, which includes falsification of subtly incorrect solutions, can sometimes be harder for models than solving the problem correctly. This indicates limitations in the potential for self-improvement using the generator- verifier gap (Song et al., 2024). As models progress towards solving novel problems where humans cannot provide ground-truth, it will be crucial that they can reflect about their
"httss//codeforees.com
2

---

Published as a conference paper at COLM 2025
own mistakes (DeepSeek-AI, 2025) to produce more reliable outputs. Our work takes first steps in evaluating a model's ability to falsify-in the limited domain of algorithmic problem solving, which is form of deductive reasoning. We hope our work spurs interest in the community to create such "inverse benchmarks" that test the ability of models at invalidating incorrect solutions claims in broader domains, including ones which involve inductive reasoning (Hume, 2000).
2 Related Work
Formal verification Programmatic search methods have long assisted researchers by enu- merating and validating cases ranging from symbolic execution tools like higher-order logic systems (Blanchette & Nipkow, 2010), SMT solvers (De Moura & Bjørner, 2008), sym- bolic execution tools like KLEE (Cadar et al., 2008) and randomized testing frameworks like QuickCheck (Claessen & Hughes, 2000) (for details see eloquent survey by Baldoni et al. (2018)), Automatic test case generation has widely been studied in software eegieeeninnnei engineering (see surveys (Anand et al., 2013; Zhu et al., 1997; Runeson et al., 2006)). Existing work on LM based test generation (Li & Yuan, 2024) focuses creating valid inputs and desired outputs for a given task specification. However, counterexamples may reside in non-obvious regions of combinatorially large input spaces, making cearch-based methods infeasible (Holzmann, 2002), especially in algorithmic reasoning settings (Forišek, 2006). While formal verification tools have made lot of progress (Alur et al., 2013; Polgreen et al., 2020), their expressivity still remains limited (Ammons et al., 2002; Bjorner & Havelund, 2014; Rozier, 2016). More- over, most claims are unstructured, and complete formalization of the whole system is not possible for most claims. We focus on the task of hard-to-find, targeted test cases that invalidate subtly incorrect solutions.
Fact Verification as Refuting False Information. At first glance, fact checking (and misinfor- mation detection) literature also aims to refute incorrect claims by verifying facts (Thorne et al., 2018; Guo et al., 2022; Press et al., 2024; Nakov et al., 2021), such as on social media platforms (Aïmeur et al., 2023; Chen & Shu, 2024) using sourced evidence (Nakano et al., 2021; Chen et al., 2023; De et al., 2024). Yet, fact checking is challenging due to unclear epis- temological grounding of truth in a complex social world (Uscinski & Butler, 2013; Vinhas Bastos, 2022). In contrast, we focus on domains with clear truth semantics (Davidson, 1967), requiring the model to produce a counterexample that verifiably refutes given claim.
Cybersecurity. Cybersecurity has traditionally focused on vulnerability detection with CTF style contests (Agency, 2023; AIxCC, 2016), with recent interest in LLM Agent sys- tems (Abramovich et al., 2024; Deng et al., 2023) (refer to (Motlagh et al., 2024) for a survey). Similarly, fuzzing (Huang et al., 2024b) involves finding security vulnerabilities in software codebases by providing invalid or unexpected random data and monitoring for crashes, failing pre-defined assertions, memory leaks. On the surface, CTF and fuzzing do require finding worst-case inputs that cause code to misbehave. Our work focuses on creating counterexamples using valid inputs for subtly wrong algorithmic solutions, with an eye towards subtly incorrect scientific claims.
Code Self-Repair. Existing work on code self repair (Chen et al., 2024) focuses on the follow- ing task: the LM is given access to code execution environment (Wang et al., 2024) along with predefined test cases, and iteratively improves its own solution using compilation and correctness feedback till it passes all test cases (Khattab et al., 2023). Instead, our work focuses on the ability of the LM to generate worst-case test cases where a given incorrect solution would fail. Gu et al. (2024) show that LMs struggle to classify their own generations as incorrect. Improving counterexample creation could thus help LMS self-repair their own code when solving novel problems with unknown ground-truth
Language Models for Scientific Discovery. FunSearch (Romera-Pareedes et al., 2024) demon- strated the use of LMs to generate novel solutions to an open problem in Mathematics, given access to a programmatic evaluator. We ask, can LMs falsify subtly incorrect solutions or claims, including domains where programmatic evaluation might not be possible? Lu et al. (2024); Si et al. (2024) proposed writing research papers end-to-end using an LM, an agentic pipeline where feedback is obtained from LM generated review scores. Instead of
3

---

Published as a conference paper at COLM 2025
depending papers and review scores arbitrary units of science, we focus research progress through precise claims and counterexamples.
Scalable Oversight. In the limit, improving at counterexample creation can help models red-team (Perez et al., 2022) another model's reasoning (Tyen et al., 2024; Huang et al., 2024a), thus acting better judges (Zheng et al., 2023), Allowing self-improvement through critique (Wang et al., 2025) and debate (Kenton et al., 2024). Finding mistakes and avoiding sycophantic behavior (Sharma et al., 2024) is crucial for emerging safety paradigms where models assist humans in overseeing other models (Bowman et al., 2022).
3 Problem Formulation
Most current benchmarks for language models involve choosing or generating a correct solution to given problem. We now formalize inverse benchmarks, which test model's ability to falsify incorrect solutions.
3.1 Falsification by Providing Counterexamples
To falsify a claim means to find counterexample that shows the claim is not always true.
Clain: A claim C has two parts: set of conditions H. and proposition P. The claim is true when: Given any input that meets the conditions (H(x) is true), then it must also make the proposition true (P (x) is true). We write this as H(x) = P(x).
Counterexample: counterexample to a claim is an input x that shows the claim is wrong. This means that x* follows all the rules (H(x*) is true) but does not make the statement true (P(x*) is false).
Task. Given a claim C (which might be stated in natural language), the model must find counterexample x".
3.2 Finding Counterexamples for Algorithms
How to check whether proposed counterexample x* truly invalidates the claim? This requires verifying: (i) The conditions H are met and, (ii) The claim P does not hold for the given input. As first step, we focus on a setting where counterexamples can be automatically verified: algorithmic problem solving. Here, solution is to be generated for problem statement which specifies the computational task, input constraints and input-output formats, and example cases for reference. The conditions Ht and claim P are:
H The input format and constraints included in the given problem statement are satisfied. The given code A solves the problem described the statement.
Task. The goal of the model is to find an input x" where A produces an incorrect output. A validator script verifies whether satisfies the input constraints H. Then, the claim can be checked by comparing the output of A to a ground-truth solution (AA*), i.e, A(x*) * A' (x*).
4 REFUTE Benchmark
Having formalized counterexample creation in algorithmic problem solving, we now de- scribe the data collection process and features of RÉFUTE.
4.1 Data Collection
We first discuss how we collect problems and corresponding incorrect codes that form the samples in REFUTE. The overall pipeline is described in Figure 2.
Sourcing Problem Statements. We first source 647 problems from Codeforces Division 1 and Division contests held between January 2024 and January 2025, reflecting latest,
4

---

Published as a conference paper at COLM 2025
greedy
data streetine
implerantinn Taton
seatch
Codedorces problems Jan 25
647
des and
grapha
constructive algotishig
495
Easy to evaluaae
bil hiluus ko
tWo pointess
divido and tonquer
403
Non trivial solutions
string
shorted
345
Unilikely to at random imputs
proba
matriess
hushing
Dows
Aren't baiting for hackss
grapp mistchinge
324
string suffix strudjuzee
mice--in-then he--thh--iddlll
chinese remainder Thegrem
terpary
2-pa
schedu
50
100
150
Number of Problems
Figure 2: (Left) Sample Filtering Pipeline. We curated (problem, incorrect solution) pairs from Codeforces (Jan 2024-Jan 2025) where counterexamples are easy to verify but non- trivial to generate, using 4-step filtering process (dynamically expandable over time). (Right) Dataset Topic Coverage. The dataset covers 35+ algorithmic topics, including many niche ones. Problems are multi-tagged-e,, e.g.. the high number of "ggredy" problems indicates it's one of the key concepts, not the only one.
competition-level programming tasks. We apply two filters on the problems: (i) We remove 152 (23%) problems that require a non-trivial grading environment for any given input. Such problems are explicitly marked as involving interaction between the program and a grader, allowing multiple correct outputs for given input. (ii) Then, remove 92 (18% of the remaining) problems which are rated below 1200. The incorrect solutions here are more likely to have trivial implementation bugs as these problems do not require much algorithmic reasoning. We also obtain the correct solution for each problem as these are released officially by the problem authors in an editorial.
Picking Incorrect Solutions. Next, we select incorrect submissions for each the shortlisted problems, optimizing for ones where creating counterexamples might be more challenging and interesting. As we wish to test falsification and not implementation inefficiences, we filter to submissions marked as providing wrong answers, rather than those that violated time or memory constraints. For these incorrect submissions, we prioritize them using the following scoring function: score(s) hss) M + f(s) + 10 b(s). Here, h(s) indicates whether the submission was "hacked" post-contest after passing all test-cases designed by the problem authors. We strictly prioritize such submissions by adding a large constant = = 10 to their score, as they form interesting instances of subtle incorrect solutions that slipped through initial tests, but human experts could create counterexamples for them under time-constraints. Next, (s)) is the number of test cases the submission passed before giving wrong answer. Finally, b(s) takes a binary value that indicates whether the author is rated 2 2000, acting as bonus for expert written incorrect submissions.
Filtering Trivial Samples. Finally, we remove samples for which finding counterexamples is trivial in two ways. First, we wish to ensure that randomly generating test cases without reasoning about the incorrect code is not enough to find counterexample. We provide Gemini 2.0 Flash Thinking just the problem statement, without the incorrect code, and prompt it to output random test case generation code. We run this test case generator for up to one minute to check whether it can find any inputs where the incorrect code doesn't t match the ground-truth solution. This is true for 58 (14%) of the 403 problems. We filter these incorrect submissions.
Second, we found that 21 (6%) submissions contain deliberately inserted code that produces incorrect outputs only when a specific, unlikely constant appears in the input. This is done perhaps way to maliciously bait for hacks in the contest, as hackers are rewarded with extra scores. For the results in our paper, an expert human evaluator went through the submissions and removed such samples. It is easy to automate this step the malicious
5

---

Published as a conference paper at COLM 2025
0,35
Max 13
039%
Melia 2013
Sau
6:122
617%
Tex. Coes Poseed Rosrroe Salurbekkes
Prokica Builnng
Auttor Rislls
The median test cases passed is 17, making the mistakes non-trivial. (Center) Distribution of Problem Ratings: The benchmark spans a range of difficulty levels. (Right) Distribution of Incorrect Solution Author Ratings: Preference was given to expert authors, rated above 2000, resulting in noticeable peak.
Figure 3: (Left) Distribution of Test Cases Passed by Incorrect Solutions:
parts of such code are quite overt. We plan to utilise a language model by providing it the expert identified samples as demos, along with a rubric.
Final Dataset. The REFUTE dataset contains 324 samples authored by 304 different pro- grammers. The incorrect submission in 317 samples written in C++. The remaining are in Python, as C++ is far more popular in programming competitions due to its efficiency. Each sample consists of a unique problem statement with an incorrect code solution, and the correct solution along with an input validation script is available for evaluation. The corresponding lengths are summarized Table
4.2 Benchmark Features
Our benchmark is constructed to have desirable features highlighted below.
Allows arbitrary algorithmic generation of novel counterexamples. We provide the lan- guage model a problem statement and incorrect solution, and ask it to output a code Aout that, when executed, outputs a counterexample input The code Aout must complete its execution within minute, and the LM is informed of this time limit in its prompt. Allowing the LM to output code allows it to generate counterexamples with varying complexity, ranging from a hard-coded input to complex functions that create the counterexample input. We score the counterexample from the correct one, while matching constraints specified in the problem.
success if the incorrect solution has different output
Avoids Search and Training Data Leakage. Codeforces does not publically reveal the full test cases that broke an incorrect submission on non-trivial cases, so models cannot directly find counterexamples on the internet. Further, to prevent indirect leakage from user discussions, we will dynamically update the claims as more contests on Codeforces occur, similar LiveCodeBench (Jain et al., 2024). This allows model comparisons by filtering to the subset of claims collected after the latest knowledge cutoff date among the models.
Diversity and Metadata. Our benchmark spans 34 fundamental topics in algorithms as tagged by Codeforces (e.g. Greedy, Dynamic Programming, Graphs, etc.), shown in Figure 2. The problems range in difficulty from an Elo rating of 1200 to 3500, while the incorrect submissions are authored by programmers with expertise ranging from Elo 700 to 3800. Figure 3 shows the distribution over problem rating, solver rating, and the test case number where the submission failed on CodeForces. We provide all these meta-data annotations for each sample in our benchmark, which may be helpful for future research.
5
Experiments
We first report frontier reasoning and non-reasoning models' performance at creating counterexamples on our benchmark and then analyze the results.
5.1 Models struggle at creating counterexamples
Based on LiveCodeBench (leaderboard in Figure 5), we select the three best reasoning models from unique developers: 03-mini-high-0131, DeepSeek R1, Gemini 2.0 Flash Thinking-0121 and the two best chat models, Claude-3.5-Sonme 2024ee22224022 and DeepSeek V3. We also test Claude Sonnet 3.7, enabling thinking in the zero-shot setting.

---

Published as a conference paper at COLM 2025
Table 1: Performance Comparison of LLMs. We test 4 strategies across 324 problems in our benchmark. While top reasoning models can generate correct solutions for nearly half of the problems, their ability to find counterexamples for subtly incorrect solutions lags significantly, even with agentic code execution feedback. Providing models with the correct solution does not substantially improve counterexample generation, highlighting fundamental gap between solving and falsifying.
Solution Generation
Counterexample Creation
Model
Rating
Solved%
Cost (S)
Prompting
ReAct Agent
Zero-shot
Few-shot
w/ Correct
w/o Demo
w/ Demo
DeepSeek-V3 Sonnet:3 3.5
1134
10.8
5
2.4
2.7-188
3.7=21
3.7220
3.1:1.7
71
4.6+1.9
3.7-20
2.2+1.6
3.0+1.9
Sonnet
383
8.0+22.4
3.4=1.4
7.5+233
Flash 2.0 (Thinking)
0.9+-1.0
2.1-1.6
2.5+1.7
1.8+1.4
2.5+1.7
DeepSeek-RI
2029
44.0
104
5.8:2..5
52-24
4.-2.1
6.5226
03-mini (high)
2130
48.7
76
8.6:22.8
8.9-2.9
9.3-288
6,842.66
8,6
We compare two strategies: Prompting and Agentic Code Execution.
Prompting. We prompt each model with the problem statement, input constraints, example input-output pairs, and the incorrect code. The model must produce a script to print failing test case, along with concise reasoning. In the few-shot setup, we also present three sample problems and incorrect code illustrating diverse issues with expert-annotated rationales.
Agentic Interaction with Code Execution Feedback. A typical human workflow of finding bugs involves tinkering with the code and observing its behaviour various inputs. Inspired by this, we allow the model to interact with a code execution environment. The model can make upto ten attempts to execute any code with arbitrary inputs it wishes to test. It receives the output in return. In case of errors, it receives the corresponding feedback instead (e.g. compiler messages). For example, the model can add print statements to the incorrect code and observe intermediate behaviour (Hu et al., 2024). It can also write its versions of subroutines in the code and observe any differences from how the buggy code handles the same scenario, effectively avoiding the need to "dry run" computations itself. To prevent exhausting the context, we truncate the outputs upto 2000 characters before revealing them to the model. Each code execution is limited to 30 seconds. After this interactive phase, similar to the standard prompting setup, the model must submit script to print failing test-case. If this submission fails validation checks, we provide this feedback the agent and allow to resubmit upto five times.
Can models solve these problems? We include the code generation performance of models on our benchmark's problems by estimating the number of problems solved. This is computed by first finding the per-problem success probability, which is derived from the problem's rating and the model's reported Elo (DeepSeek-Al. 2025) following standard Codeforces
rating calculations. If the model rated r, we define: (rlved Ep
Here, p is sampled from the problem ratings in our benchmark.
What if models have access to the ground-truth solution? We also evaluate the impact of providing models with access to the correct code. This decouples the ad advantage of models with better solution generation abilities. We augment the earlier zero-shot prompting setup to additionally reveal the correct solution and report results in Table 1 (w/ Correct).
Discussion and Error Analysis. Table 1 shows that counterexample creation lags signifi- cantly behind solution generation and does not scale proportionally. Models also struggle to leverage code execution feedback-a key component of human debugging workflows-wiit only DeepSeek R1 exhibiting modest improvements. On the other hand, our analysis shows that execution feedback greatly reduces test-case validation failures. For instance, DeepSeek R1 and V3 both eliminate validation issues completely, compared to 45 and 36 failures in the zero-shot setting. Additionally, while few-shot prompting with expert rationale improves Gemini's performance over zero-shot, other models show minimal gains even degrade.
7

---

Published as a conference paper at COLM 2025
Table 2: Prompting Models to use Search to find Counterexamples. Without the correct solution (RandSearch), models often generate invalid counterexamples where the incorrect solution gives the right output. The counterexample success rate increases with access to the correct solution (RandSearch Oracle), but significant room for improvement remains.
Model
DeepSeek-V3
Flash 2.0 (Thinking)
DeepSeek-R1
o3-mini (high)
RandSearch
4.0
3.7
4.0
8.3
RandSearch Oracle
15.1
7.7
9.9
The oracle (Table 1 (w/ Correct)) simulates a hypothetical where o3 (currently unreleased) matches the reported Codeforces rating of 2727, or a future model is able to solve most Code- forces problems: would they automatically be able to find counterexamples for incorrect solutions? While counterexample creation abilities could also improve, knowing the correct solution alone is insufficient even for the best current reasoning model, 03-mini (high).
5.2 Does explicit prompting for search help?
Manual inspection of model outputs revealed that models rarely used a search based strategy to find counterexamples, In contrast, humans often generate randomized inputs guided by structural intuition which they expect to yield valid counterexamples. To address this, we explicitly prompt models to generate counterexamples using a search-based strategy with controlled randomization. Note that a key difference from our initial filtering step (where we filtered trivial samples that can be broken through search without reasoning, described in Section 4.1) is that there the model was not given access to the incorrect solution, so it by definition did not reason about it, whereas here it can. Specifically, we test two strategies and report these numbers in Table 2:
RandSearch. The model constructs a randomized input generator and a brute-force solution. We use the generator to search for tests and compare the outputs of the brute-force solution against the incorrect code. The search terminates when it encounters differing outputs. We limit this search to 2 minutes. We provide few-shot examples with rationale only to non-reasoning models, as reasoning models performed better without them.
RandSearch Oracle. The previous step requires the model to generate a brute-force solution. solutions for these algorithmic prob-
While it is often easy to find apponential-copleen lems, models could still produce wrong ones. To alleviate this, we simulate a hypothetical scenario where the model has access to the correct solution and then writes a randomized search strategy to find an input where the incorrect solution's output strategy doesn't 't match. In other words, the model can use our ground-truth verification environment, so any input produced at the end is likely to be correct as long as it passes validation checks.
We provide detailed description of the motivation and nuances of these methods in Appendix A.
Discussion and Error Analysis. Performance of reasoning models deteriorates when ex- plicitly prompted to use randomized search. It offers marginal gains for chat models. For 03-mini, the successful samples are interestingly quite disjoint when using this strategy. The counterexamples created invalidate 6% distinct submissions that the previous prompting and agentic strategies could not, in contrast to 3% new submissions invalidated when the model was provided correct solutions. This shows that models learning to leverage programmatic search when appropriate can significantly boost performance.
Further analysis of RandSearch's 's failure modes reveals that, average, 35% of all samples terminate with an incorrect counterexample. Among these, 14% fail due to test-case vali- dation errors, while the remaining 86% result from incorrect brute-force code. This trend remains remarkably consistent across models - differences in code generation benchmarks do not appear to significantly impact their ability to write trivial brute-force code.
Gemini Flash 2.0 (Thinking), the worst performer, and o3-mini (high), the best, are similarly bottlenecked by incorrect brute-force code (28% vs. 32% of all samples). However, 03-mini (high) still manages to double its overall success rate, suggesting that more intelligent search strategies can outperform unguided attempts.
8

---

Published as a conference paper at COLM 2025
misuae
me
Figure 4: Analysis of R1, 03-mini (high) success rate at creating counterexamples, com bining success across strategies like prompting, agent and programmatic search. We find that model successes are not predictable based on problem difficulty, or attributes of the incorrect submission like author expertise and number of test cases passed before giving wrong answer. Success rate on the hacked subset, where counterexamples were found despite passing all initial tests is 4% 1%.
5.3 When can models create counterexamples?
As counterexample creation abilities are particularly relevant for model reflection and reliability in model outputs, it is important to characterize in what types of situations they can and cannot create valid counterexamples, We analyze counterexample creation success across three attributes which are highly predictive of solution generation correctness problem difficulty, number of tests the incorrect submission passed before failing, and incorrect submission author expertise. For each attribute, we divide samples into five percentile buckets and measure average success at creating counterexamples of the best two models, R1 and o3-mini (high), across prompting (Zero-shot, Few-shot), agentic (with and without demos) and search strategies.
Surprisingly, we find no clear trends in Figure between these three attributes and coun- terexample creation success. We also find limited insight based on problem statement and incorrect solution length as shown in Appendix Figure This demonstrates that model counterexample capabilities can be non-trivial to predict using attributes that are predictive of solution generation capabilities. This further highlights the complementary nature of fal- sification. We believe that better understanding of what attributes contribute to its difficulty an important direction for further investigation.
5.4 Where do the models fail?
To better understand the failure modes of the models, conducted a detailed error analysis. A domain expert (Codeforces Grandmaster) manually annotated the underlying bugs in the incorrect code and compared them against the models' attempts at generating counterexamples.
5.4.1 Analysis of Bug Misclassification
In our analysis of 25 random tasks, we observed the following tendencies in how models classified the nature of the bug.
For 48% of the tasks, the model incorrectly assumed the bug was with the underlying logical approach, completely missing that it was a minor implementation error.
Conversely, for only 8% of the samples, the model mistakenly identified an issue an
implementation bug when the core logic was flawed.
The model correctly identified the bug as logical issue 20% of the cases and as an implementation bug in 24% of the tasks.
For 20% of the tasks, the model had a nearly correct understanding of the bug but was unable to generate a test case to exploit it.
For these same incorrect submissions, we examined the performance of the original human contestants in the programming competition. We found that the contestants took median time of minutes to identify the bug, correct it, and resubmit an accepted solution, indicating that for humans, these were often not conceptually difficult bugs resolve.

---

Published as a conference paper at COLM 2025
Distribution of successfully identified bug types compared to their overall distribu- Table 3:
tion in random sample of the dataset.
Bug Type
Successful Tasks
% in Dataset (Sampled)
Initialization and bounds errors
56%
32%
Incorrect approach
28%
28%
Implementation errors Edge case handling errors
12%
20%
3%
20%
5.4.2 Qualitative Analysis of Failures
We performed qualitative analysis of the failed attempts to identify recurring patterns of incorrect reasoning.
Misallocated Attention. Models frequently misdirect their attention to parts of the code less likely to contain bugs, such as I/O code or standardized data structure templates. This contrasts with expert human programmers who typically begin by critiquing the high-level algorithmic logic before focusing on lower-level implementation details. This suggests that models may lack effective abstraction for evaluating the structural correct- ness of program.
Boundary Condition Analysis. Models frequently fail to find bugs related to edge cases. Human debuggers often test extremal values within the given input constraints to find such bugs. Despite many instances in our benchmark being susceptible to these types of errors, the models often failed to generate the corresponding counterexamples.
Failure to Follow Search-Based Instructions. When prompted for randomized search code, reasoning models often ignored the instruction, instead outputting a single de- terministic test case after long chain of reasoning. In contrast, chat models such as DeepSeek V3 consistently followed the instructions, leading to better performance.
Impact of Feedback on Validation Errors. significant number of counterexamples, particularly from DeepSeek R1, were invalid due to format or constraint violations (almost 15% in zero-shot and few-shot settings). Providing explicit feedback (agentic setting) on why test case failed proved highly effective and nearly eliminated these errors, whereas simple failure notifications were insufficient.
5.4.3 Distribution of Correctly Identified Bugs
We further analyzed all the successfully generated counterexamples across models and strategies to understand which types of bugs are more easily identified (Table 3). This distribution is notably skewed when compared to the underlying distribution of bug types in random sample of 50 problems from our dataset, which is more balanced. Models are significantly better at finding simpler issues like off-by-one errors or the use of incorrect constants. Conversely, they are less likely to identify instances where the fundamental algorithmic approach flawed, and they perform even worse when the logic is incorrect only in specific, corner cases that could be handled separately.
6 Conclusion
In this work, we take the first steps toward benchmarking the ability of language models to create counterexamples for incorrect solutions. Focusing on algorithmic problem solving, we found that models often fail to detect errors in failed Codeforces submissions - even when given the correct solutions as guidance. We hope hillclimbing on our benchmark spurs effective methods for creating counterexamples using LMs, and deepens our under- standing of how this capability relates to a models capacity for reasoning, reflection, and rel--improveeent. We hope there will be more benchmarks for counterexample creation, such as for research-level mathematics (Bengio Malkin, 2024; Davies et al., 2021; Wagner, 2021). We excited about methods that integrate formal tools such SMT solvers to lever- age their complementary strengths. While our work focuses on claims and counterexamples verifiable through code execution many scientific hypotheses are not easily formalized in this way. Designing evaluations that test a model's 's ability to propose counterexamples based solely natural language claims presents exciting direction for future research.
10

---

Published as a conference paper at COLM 2025
Impact Statement
Al generated solutions, such entire research papers eL al., 2024), risk overwhelming our infrastructure to refute them, following Brandolini's law (Williamson, 2016). Our paper highlights the need for inverse benchmarks, that evaluate the ability of models to falsify sub- tly incorrect solutions, instead of the traditional paradigm of solving problems. Improved ability to falsify can help make AI outputs more reliable through reflection, which is impor- tant as edge-cases have long been the Achilles heel of deep learning driven deployments like self-driving. To emphasise that falsification we create REFÚTE, which we will release publically. Progress on REFUTE could also help language models' ability to audit codebases for mistakes, improving software reliability in an increasingly digitized economy.
sometimes be harder than generation,
Author Contributions
Shiven and Ameya conceived the project. Shiven led the experiments, and Shashwat helped design the benchmark. Shashwat and Shiven co-led the writing of the paper, with help from Ameya. PK provided helpful feedback throughout the project. Jonas, Matthias and Ameya advised the design of all experiments.
Acknowledgements
Special thanks to Siddharth Bhat and Siddhartha Gadgil for inspiration about this direction and specifically for introducing us to formal verification and counterexample creation. The authors would like to thank (in alphabetical order): Nikhil Chandak, Hari Aakash K, Shyamgopal Karthik, Srija Mukhopadhyay, Alexander Panfilov, Vishaal Udandarao, Saujas Vaduguru. AP and MB acknowledge financial support by the Federal Ministry of Education and Research (BMBF), FKZ.011S24083B and Open Philanthropy Foundation funded by the Good Ventures Foundation.
References
Talor Abramovich, Meet Udeshi, Minghao Shao, Kilian Lieret, Haoran Xi, Kimberly Milner, Sofija Jancheska, John Yang, Carlos É Jimenez, Farshad Khorrami, et al. Enigma: Enhanced interactive generative model agent for ctf challenges. arXiv preprint ar 1616: 2024.
Defense Advanced Research Projects Agency. AI Cyber Challenge, 2023. URL https: cyaer whweeeeghallleeeeeeeeeeeee com about/. Accessed: 2025-02-11.
Esma Aïmeur, Sabrine Amri, and Gilles Brassard. Fake news, disinformation and misinfor- mation in social media: review. Social Network Analysis and Mining, 13(1):30, 2023.
AIxCC. DARPA Cyber Grand Challenge, 2016. URL https: http://wwwaaaa wwww..arra..o mi -ham:/yyyerrrradchhaaa chann-chhaleen Accessed: 2025-02-11.
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guider synthesis. IEEE, 2013.
Glenn Ammons, Rastislav Bodík, and James Larus. Mining specifications. ACM Sigplan Notices, 37(1):4-16, 2002.
Saswat Anand, Edmund K Burke, Tsong Yueh Chen, John Clark, Myra B Cohen, Wolfgang Grieskamp, Mark Harman, Mary Jean Harrold, Phil McMinn, Antonia Bertolino, et al. An orchestrated survey of methodologies for automated software test case generation. Journal of systems and software, 8688) 2013.
11

---

Published as a conference paper at COLM 2025
Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1-39 2018.
Yoshua Bengio and Nikolay Malkin. Machine learning and information theory concepts towards an mathematician. Bulletin of the American Mathematical Society, 61(3):457-469, 2024.
Dines Bjorner and Klaus Havelund. 40 years of formal methods: Some obstacles and some possibilities? In International Symposium on Formal Methods, pp. 42-61. Springer, 2014.
Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on relational model finder. In International conference on interactive theorem prozing, pp. 131-146. Springer, 2010.
Samuel R Bowman, Jeeyoon Hyun, Ethan Perez, Edwin Chen, Craig Pettit, Scott Heiner, Kamilé Lukošiūtē, Amanda Askell, Andy Jones, Anna Chen, et al. Measuring progress on scalable oversight for large language models. arXiv preprint arXiv:2211.03544/ 2022.
Cristian Cadar, Daniel Dunbar, Dawson R Engler, al. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume 8, pp. 209-224, 2008
Canyu Chen and Kai Shu. Combating misinformation in the age of Ilms: Opportunities and challenges. Al Magazine, 45(3):354-368, 2024.
Jifan Chen, Grace Kim, Aniruddh Sriram, Greg Durrett, and Eunsol Choi. Complex claim verification with evidence retrieved in the wild. arXiv preprint ar Xtt:2305.11859, 2023.
Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. In The Twelfth International Conference on Learning Representations, 2024. URL https: http///pppeeeee.eeeeeeeee net/ forum? www.:mmmmduuiiiiapppooo
Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of haskell programs. In Proceedings of the fifth ACM SIGPLAN international conference on 2000.
Functional programminng pp.
Donald Davidson. Truth and meaning. In Philosophy, Language, and Artificial Intelligence: Resources for Processing Natural Language, pp. 93-111. Springer, 1967.
Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, et al. Advancing mathematics by guiding human intuition with ai. Nature, 600(7887):70-74, 2021.
Soham De, Michiel A Bakker, Jay Baxter, and Martin Saveski. Supernotes: Driving consensus in crowd-sourced fact-checking. arXiv preprint arXio:2411.06111 2024.
Leonardo De Moura and Nikolaj Bjorner. Z3: An efficient smt solver. In International
conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, 2008
DeepSeek-Al AI. Deepseek-r1: Inceniiiiig learning, 2025. URL https://arxiv.orr abs/2501. 22911.2948..
reasoniing reasoning capability in llms via reinforcement
Gelei Deng, Yi Liu, Victor Mayoral-Vilches, Peng Liu, Yuekang Li, Yuan Xu, Tianwei Zhang, Yang Liu, Martin Pinzger, and Stefan Rass. Pentestgpt: An llm-empowered automatic penetration testing tool. arXiv preprint ar xrXtv:2308.06782,222 2023.
Michal Forišek. On the suitability of programming tasks for automated evaluation. Infor- matics in Education-An International Journal, 5(1):63 76, 2006
Alex Gu, Wen-Ding Li, Naman Jain, Theo Olausson, Celine Lee, Koushik Sen, and Armando Solar- The counterfeit conundrum: Can code language models grasp the nuances of their incorrect generations? In Findings of the Association for Compulational Linguistics: ACL. 2024, 2024. URL https: //acllattollogy.ooo orw.hholllooooog//////g/ 2024 ttt findings-achh acl.7/
12

---

Published as a conference paper at COLM 2025
Zhijiang Guo, Michael Schlichtkrull, and Andreas Vlachos. A survey automated fact-
checking. Transactions of the Association for Computational Linguisties, 10:178-206, 2022.
Gerard J Holzmann. The logic of bugs. ACM SIGSOFT Software Engineering Notes, 27(6): 81-87, 2002.
Xueyu Hu, Kun Kuang, Jiankai Sun, Hongxia Yang, and Fei Wu. Leveraging prnneragnggppinnddeeege debugging to improve code generation in large language models, 2024. URLhttps://axxiv.orgg hos/2401.05319,
Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Wei Yu, Xinying Song, and Denny Zhou. Large language models cannot self-correct reasoning yet. In ICIR,, 2024a.
URL.ttpss:
Linghan Huang, Peizhou Zhao, Huaming Chen, and Lei Ma. Large language models based fuzzing techniques: A survey, 2024b. URL https: /ttt:::://aaxi.oooo/ g/ abs 2402. 00350.
David Hume. A treatise of human nature. Oxford University Press, 2000.
Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Ar- mando Solar-Lezama, Koushik Sen, and Ion Stoica. Livecodebench: Holistic and contami- nation free evaluation of large language models for code. arXiv preprint arXim:2403.07974, 2024.
Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R Narasimhan. SWE-bench: Can language models resolve real-world github issues? In The Twelfth International Conference on Learning Representations, 2024. URL https://openrevieet www.rreiiwweeeeeeeeeeee formff www.
John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ron- neberger, Kathryn Tunyasuvunakool, Russ Bates, Augustin Zidek, Anna Potapenko, al. Highly accurate protein structure prediction with alphafold. nature, 596(7873):583--55 2021.
Zachary Kenton, Noah Y. Siegel, János Kramár, Jonah Brown-Cohen, Samuel Albanie, Jannis Bulian, Rishabh Agarwal, David Lindner, Yunhao Tang, Noah D. Goodman, and Rohin Shah. On scalable oversight with weak Ilms judging strong Ilms, 2024. URL httpps://ara http::////xxv.rg//bb///////// wbwgg//b////...... 04622.
Omar Khattab, Arnv Singhvi, Paridhi Maheshwari, Zhiyuan Zhang, Keshav Santhanam, Sri Vardhamanan, Saiful Haq, Ashutosh Sharma, Thomas T Joshi, Hanna Moazam, al. Dspy: Compiling declarative language model calls into self-improving pipelines. aiv preprint 2rXio:2310.03714, 2023.
Joseph B Kruskal. On the shortest spanning subtree of a graph and the traveling salesman problem. Proceedings of the American Mathematical society, 7(1) 50, 1956.
Imre Lakatos. Proofs and refulations: The logic of mathematical discovery. Cambridge university press, 2015.
Kefan Li and Yuan Yuan. Large language models as test case generators: Performance evaluation and enhancement, 2024.
13340.
Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune, and David Ha. The Al Scientist: Towards fully automated open-ended scientific discovery. arXiv preprint arXie:2408.00229, 2024.
Farzad Nourmohanmadzader Motlagh, Mehrdad Hajizadeh, Mehryar Majd, Pejman Najafi, Feng Cheng, and Christoph Meinel. Large language models in cybersecurity: State-of-the art. arXiv preprint ar 2rXio=2402.00891, 2024.
Reichiro Nakano, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christo- pher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, et al. Webgpt: Browser- assisted question-answerinn with human feedback. arXiv preprint arXin:2112209332, 2021.
13

---

Published as a conference paper at COLM 2025
Preslav Nakov, David Corney, Maram Hasanain, Firoj Alam, Tamer Elsayed, Alberto Barrón- Cedeño, Paolo Papotti, Shaden Shaar, and Giovanni Da San Martino. Automated fact- checking for assisting human fact-checkers, arXiv preprint arXtr:2108.07769, 2021.
Theo X. Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. Is self-repair silver bullet for code generation?, 2024. URL https: //arxiv.or or g/ http://3.6..999900
OpenAI. Openai o3 mini. https:/
Ethan Perez, Saffron Huang, Francis Song, Trevor Cai, Roman Ring, John Aslanides, Amelia Glaese, Nat McAleese, and Geoffrey Irving. Red teaming language models with language models. In EMNLP, 2022. URL https: a lantho logy. woo.oooo...oooooooooooooooooooo. orgg/022...2.. emn manll-mma7 1o-mmain main. 225/.
Long Phan, Alice Gatti, Ziwen Han, Nathaniel Li, Josephina Hu, Hugh Zhang, Sean Shi, Michael Choi, Anish Agrawal, Arnav Chopra, et al. Humanity's last exam. arXiv preprint (rXio:2501.14249, 2025.
Elizabeth Polgreen, Ralph Abboud, and Daniel Kroening. Counterexample guided neural synthesis. arXiv preprint arXiv:2001.09245 2020.
Karl Popper. The logic of scientific discovery. Routledge, 2005.
Ori Press, Andreas Hochlehnert, Ameya Prabhu, Vishaal Udandarao, Ofir Press, and Matthias Bethge. Citeme: Can language models accurately cite scientific claims? arv preprint ar xxx::2407.12861, 2024
Bernardino Romera-Paredess Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models. Nature, 2024.
Kristin Yvonne Rozier. Specification: The biggest bottleneck in formal methods and au- tonomy. In Verified Software. Theories, Tools, and Experiments: 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers 8, pp. 8-26. Springer, 2016.
Per Runeson, Carina Andersson, Thomas Thelin, Anneliese Andrews, and Tomas Berling, What do we know about defect detection methodss?|software testing]. IEEE software, 23(3): 82-90, 2006.
Mrinank Sharma, Meg Tong, Tomasz Korbak, David Duvenaud, Amanda Askell, Samuel Bowman, Esin DURMUS, Zac Hatfield-Dodae Scott Johnston, Shauna M Kravec, Timo- thy Maxwell, Sam McCandlish, Kamal Ndousse, Oliver Rausch, Nicholas Schiefer, Da Yan, Miranda Zhang, and Ethan Perez. Towards understanding sycophancy in language mod- els. In JCLR, 2024. URL htwptt:t/ /otp:s//////eeeeeeeeee www.t//ooorrmdtta/aaaaaaaaa
Chenglei Si, Diyi Yang, and Tatsunori Hashimoto. Can llms generate novel research ideas? large-scale human study with 100+ nlp researchers. aiv preprint arXiv:2409.0415 2024.
Yuda Song, Hanlin Zhang, Carson Eisenach, Sham Kakade, Dean Foster, and Udaya Ghai. Mind the gap: Examining the self-immpoveeentt capabilities of large language models, 2024. URL https: http///xxvvv./////////// /bs/a/
James Thome,, Andreas Vlachos, Christos Christodoulopoulls, and Arpit Mittal, Fever: large-scale dataset for fact extraction and verification. arXio preprint ar 2018.
Gladys Tyen, Hassan Mansoor, Victor Carbune, Peter Chen, and Tony Mak. LLMs cannot find reasoning errors, but can correct them given the error location. In ACL Findings, 2024. URL https: huR.httts://aclattoon wog.oloooy...yo..oooo 002/ findings Findings-acl..226 822.6
14

---

Published as a conference paper at COLM 2025
Joseph E Uscinski and Ryden W Butler. The epistemology of fact checking. Critical Review, 25(2):162-180, 2013.
Otávio Vinhas and Marco Bastos. Fact-checking misinformation: Eight notes on consensus reality. Journalism Studies, 468,) 2022.
Adam Zsolt Wagner. Constructions in combinatorics via neural networks. 1-23, 2021.
Xingyao Wang, Yangyi Chen, Lifan Yuan, Yizhe Zhang, Yunzhu Li, Hao Peng, and Heng Ji. Executable code actions elicit better Ilm agents. arv preprint ar arXio:2402.001330 2024.
Yubo Wang, Xiang Yue, and Wenhu Chen. Critique fine-tuning; Learning to critique is more effective than learning to imitate, 2025. URL htwps: /ttp://////axxoor//aa////
org/ www.or//aa/b/aaaae 17703.
Hjalmar Wijk, Tao Lin, Joel Becker, Sami Jawhar, Neev Parikh, Thomas Broadley, Lawrence Chan, Michael Chen, Josh Clymer, Jai Dhyani, Elena Ericheva, Katharyn Garcia, Brian Goodrich, Nikola Jurkovic, Megan Kinniment, Aron Lajko, Seraphina Nix, Lucas Sato, William Saunders, Maksym Taran, Ben West, and Elizabeth Barnes, 2024. URL https: //arxiv.org 2tbp/2411.1111..
Phil Williamson. Take the time and effort to correct misinformation. Nature, 540(763 171-171, 2016.
Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. React: Synergizing reasoning and acting in language models. arXiv preprint axXiv:2210.03629, 2022.
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, Hao Zhang, Joseph E Gonzalez, and Ion Stoica. Judging llm-as-a-judge with mt-bench and chatbot arena. In NeurIPS, 2023. URL https::/procceedngs..eeeet neuriis cc paper_ fi files pttp//ppprrr//22/// ffile/ www.anndnnnrrkss.....mama
pdf.
Hong Zhu, Patrick AV Hall, and John HR May. Software unit test coverage and adequacy.
Acm computing surveys (csur), 2664)36664477, 1997.
15

---

Published as a conference paper at COLM 2025
Appendix
We now provide thorough details about the benchmark, baselines, and prompts.
Contents
A More Details About Baselines
17
A.1 Random Search
17
A.2 Random Search (Oracle)
17
B More Details About Evaluation
18
B.1 Results Hacked Subset
18
B.2 Sample Length Analysis
19
Examples of Tasks: Samples from REFUTE
D Future Extensions
22
Limitations
23
Prompts
24
F1
Zero-Shot
24
F2
Few-Shot
25
F3
Zero-Shot Agent
25
F4
ReAct Agent (With Sample Trajectory)
27
F.5
Few-Shot Random Search
30
F.6
Zero-Shot (Oracle)...
31
F.7
Random Search (Oracle)
16

---

Published as a conference paper at COLM 2025
A More Details About Baselines
A.1 Random Search
This method is motivated by the observation that often trivial solve algorithmic problems under smaller constraints, potentially allowing suboptimal efficiency. For instance, consider the task of finding minimum spanning tree of connected graph. A trivial solution is to try all possible subsets of edges. Among all such subsets, we pick one which retains the connectivity of the graph while minimising the sum of edge weights. This solution doesn't t require any elaborate reasoning and follows directly from the definition of an MST. Notice that this is much slower than optimal solutions like Kruskal's algorithm
(Kruskal, 1956), which run in ( log E) instead of our inefficient (E2 However, this inefficient solution
execute within a few seconds for smaller graphs, with say around 20 edges, and provide valuable ground-trute outputs for arbitrary (small) inputs. This can be then used to check the correctness of the efficient but buggy solution. It is still possible for a model to write an incorrect solution or to make a test-case generator that prints invalid inputs to the problem. In such cases, the test-case discovered by this random testing will fail the subsequent evaluation. The model also needs to ensure that the random test-cases generated by its script are small enough that its own correct solution can finish execution in time.
We prompt the model output two pieces of code: (1) randomised test-case generator following the input constraints of the problem, and (2) an inefficient solution to the problem. This could be simple brute-force enumeration of all possibilites for small constraints, and finding the optimal solution using them. After obtaining these, we repeatedly generate test-cases using the generator until we find an input for which the answers provided by the incorrect and the model-generaal execution time, it is taken be the attempted counterexample and evaluated. Otherwise, this search for a test-case terminates with the model receiving no credit. We include three demonstrations for creating a randomised input generator along with a simple correct solution in our prompt.
solution differ. If such a case is found within 1 minute of
A.2 Random Search (Oracle)
We augment the Random Search baseline to reveal the efficient, correct solution to the model alongside the initial setup of providing the problem details and the buggy code. This has three important consequences.
1. Comparative Analysis. The model now knows the exact steps to solve an arbitrary instance of the problem. It does not have to engage in careful analysis and reasoning to arrive at this. The counterexample search can be guided by comparing the high-level conceptual approaches of the two implementations, well as the low-level details such as handling of edge cases, array sizes, and variable bounds.
Large Randomised Generations. Unlike RandSearch, where the correct code was prohibitively inefficient, the model's test-case generation script is no longer forced to output smaller test-cases. Both the correct and incorrect solutions can now run quickly under the full scale of the original problem's constraints. As result, random testing is much more likely to uncover bugs that only arise with larger problem instances, e.g. overflows, out-of-bounde
access, edge cases, etc.
3. Eliminates Error in 'Assumed Truth'. In RandSearch, the search for an input that caused a discrepancy between the two codes often terminated quickly. However, the issue was frequently an inaccurate brute-force solution generated by the model rather than bug acting up in the provided incorrect code. In this new setup, if the search for a failing test-case terminates within 1 minute, it is guaranteed to pass the subsequent evaluation phase (given that it follows the input format).
17

---

Published as a conference paper at COLM 2025
B More Details About Evaluation
Environment. In line with the judging environment used by Codeforces, we per- form our experiments for C++, specifically: -wall -Wextra -Nconversion -static DONLINNEJUUDGE -WL,-stcck=26445445
Windows machine. We also mimic the compilation flags
-02 -std=c++23 program. cpp -Is cuting the incorrect and ground-truth code on inputs, we allow a liberal time limit of 30 seconds. This is more than the limit imposed by Codeforces for the problems in REFUTE, which is at most 15s with a mean of 2.4s.
For exe-
Programming Languages. In REFUTE, we provide the exact programming language de- scription as supplied by Codeforces. The distinct languages spanned by the dataset are: C++14 (GCC 6-32), C++17 (GCC 7-32), C++17 (GCC 9-64), C++20 (GCC 11-64), C++20 (GCC 14), C++ (GCC msys2), PyPy 3-64, and Python 3. For execution, all C++ programs are compiled with -std=c++25 ++33, leveraging backward compatibility We use the standard CPython interpreter. We verified that these choices do not alter the behavior of the code in our benchmark.
change
aange
walerata cstell deles besed release data und pariormance var Mhodeds teghingtioal nnd lively
conteninatted on some traction prostems the given time windoww nest axquett stider inaderboard difirent time windowe. Please offer feethack you find any isssee!
Arnouncenarta:
We have made revelione to our offecist sutograder, ficiing some unhandied canes. in case you are performiig
local avatuadion, please use the looest codaitase.
2 We have been introdusing larger fraction of diffouut problems for the more recent releases lines with model parform anoae the leker munthh expaeded..
capabiiity improverants.
Rank
Nodol
Passø1
Passs1
01-15ni--811-91-111
(tish)
73.1
98..2
12.2924:22112 12 (le1)_HHa))
98.2
82-Mint: 2625-01-51 (te1) (ted)
68.7
90.2
4
01-1914-12-12 1es1 Paael
55.2
98.2
6
01:HinL N---MN---222-----11 2825-81-311 (isll Food
51.7
98.2
7
01-2826:12-112 (ee1
68.8
68.2
D1-Hini 2814--1--777---1122 (l:12
92.7
Lundadk 81 Li 2ravii
48.9
95.8
11
S1-Presian: 2024 2024-19-11 12-12
43.2
96.4
12
Beatin- Flant- www.hhhiiiigg2222 (1-1)
61.9
96.4
13
Pr
$2.7
24
Claiste- www.oottttttttoooo
57.6
19.8
1esnfost-12
82.7
16
iasini auEas
85.8
17
871-99-2226-1--13
32.4
$2.9
Claude-1, E:Sammtt
19
Semini-Proo1
52.2
12.5
OPT-69-2026-98-4
Figure 5: LiveCodeBench leaderboard in Feburary 2025, which we used to select the final models used for our benchmarking. We took the top reasoning models from unique developers, highlighted in red, and the top 2 chat models highlighted in yellow.
B.1 Results on Hacked Subset
We report model performance on the "hacked subset" where humans found the counterex- ample in extremely time-limit setting in Table 4.
18

---

Published as a conference paper at COLM 2025
Table 4: Performance of various strategies and models on the hacked subset of problems.
Model
Zero-shot
Few-shot
w/ Correct
Agent w/o Demo
Agent w/ Demo
DeepSeek-V3
0.0
0.0
2,4
2,4
2.4
Sonnet 3.5
4.8
4.8
2.4
2.4
Flash 2.0 (Thinking)
0.0
0.0
2.4
2.4
4.8
DeepSeek-R1
2.4
2.4
03-mini (high)
7.1
0.0
4.8
B.2 Sample Length Analysis
Sample component
Median Length
Problem Description
1018
Incorrect Submission
1962
Correct Solution
1552
Table We report median lengths (number of characters) of problem description and incorrect submission as these are fed as input to models. This affects the minimum input context length required and evaluation costs for our benchmark. We also report the median length of the correct solution for reference.
100
Stonos Thate 196)
7,5
Succes Rate
8.0
28.07
wi-f66
1144118
HoSSte
0.0
114-220
1200-729
178-367
2657-781
2ms-31
Profiem Statment Langee
homeet Selution length
Figure 6: Analysis of R1, 03-mini (high) success rate at creating counterexamples based sample length, combining success across strategies like prompting, agent and program- matic search. We find that model successes are not predictable based on problem statement length and incorrect solution length in characters.
19

---

Published as a conference paper at COLM 2025
C Examples of Tasks: Samples from REFUTE
Although each incorrect submission requires individual reasoning to refute, we include few examples showing three distinct kinds of bugs among the several present in our dataset in Figures 8, and 9.
nemory ind par Mnd 1664 negitopes
ferm
expld
Bug
"ieer WWbl-th Yona
usall
to ae secatio vatical glo uess Whar crnec thes are coverad
count il ariku ation
fos Clice wadder erey anyy sie caker de ideo that
points cam plutely white columa
surroundes by in
Tre calo un wede conraced they shane an edge Tho cals and pae idinccty sowd
exompepple
columin
surroundes black every
i (1-2 (o. wilkir
divudy caneecas or cals laniu singl
anticuiation point might
2o0baa7 171 2305.
Thaggh
indeoad hon tn
dtset theh cosams with ifth wherr S tor
adppcent counteeesmpple
kitwwing fagc upo pip - mose goa undend
vertical Colo miodle splits which the code wortt detect.
losge frr in comnedet component
Irpud
begia with the dona nigg eady rageri andg This doliss phc an and
tw inai conaiie eaady fime imeging de and A..
Thee aoaa vide cals and wiil forn cornecte cargle
Ourput
sape
undl
line singo aenesaed companee
Figure 7: REFUTE Sample 1. The underlying approach in the code is flawed and the model must construct grid which exposes it.
contu bedt megatee
mey
the
Bug
the peltering the sprseess virite pome
The bug the exponent calculation Q strucure. The code apolles Fermar's Little
Theorem by modsing the exponent with p-1
(999999922)
calculating lomni Y..
Hroweves, incorrect becouse representss elements 2[v2) mode dl pu
Formar's theorem holds. This leads to wrong exponentials when y large. A bost case like Nipp (999 999 trigeers compute (V2NN as (V2PIN mod p-1) instewd of Use correct valum.
Figure 8: REFUTE Sample 2. The code demonstrates perfect understanding of the core solution, but makes error while reporting it. The problem asks for the output to be reported in a certain format using exponents for the sake of easier evaluations, but the contestant made error in assuming that using Fermat's theorem directly will work well in the given space. Only the part of the code responsible for reporting the answer needs to be fixed.
20

---

Published as a conference paper at COLM 2025
Than PIPRUS VeLLoNe
LENEL
Pabi creer Thes the
Bug
tire
can
yoat:
Since colours, optimal path awwys requre elther jumping to the destination directly of passible), otherwis intermediate
means upto
The
minimum absolute difference in their positions, The arswer intielized to be INF the code, but should be stleast
in to 11 requiring hops
aibilli vatioa
sattsfied
aM =
testcasee with from (n to and then to the destination of
ABC
*
+53
Alt Trensteekcll Seakinee 093
stsiente 40 woth mn
Figure 9: REFUTE Sample 3. The contestant simply underestimated what the maximum answer can be, and initialised variable acting as a placeholder for 'Infinity' to be too small. Just doubling this value will fix the bug.
21

---

Published as a conference paper at COLM 2025
D
Future Extensions
A natural extension of our work is to broaden the scope of inverse benchmarks beyond algo- rithmic reasoning. While existing benchmarks like FrontierMath and HumanEval primarily assess problems-solving by requiring models to generate correct solutions that are directly matched against ground-truth, inverse benchmarks will require mechanisms to verify cor- rectness of proposed claims over arbitrary instances. An example of such an interaction is provided in Figure 10.
Another promising avenue is to explore how the abstraction of an LLM attempting to falsify by generating code allows for hypothesis testing, data analysis, and simulations. In principle, code serves general medium that enables verification through diverse means only limited by digital capabilities that models are fundamentally bound by already. This implies that leveraging code execution across diverse domains. As models improve, this paradigm may not only allow them to generate counterexamples but also to systematically explore patterns and behaviors, leading to more reliable scientific and mathematical discoveries.
mechanism for falsification has broad applicability
Generation Benchmarks
FrontierMath
HumanEval
Construct degree polynomial p(x)
Python code increment elements list
C(x] such that Calculate p(19).
187657207197400480330000
def incr, list(lk return for
metches
pre-defined tests
Inverse Benchmarks
Can a polynomial generate primes all positive integers? think fin) n#-79n-1601 works if isn't multiplee of 1601. Correct?
H(x): x is positive integer not divisible 1601.
((:):: x² - 79x + 1601 is prime.
Find x such that H(x) holds but not P(x))
generates primes initielly, fit) 1523, But since 1!1 1523) must be muttiple of 1523, ((1524) composite. This polynomial doesn't work.
Figure 10: Example of an inverse benchmark task in mathematics, contrasting with standard solution-generation benchmarks. This illustrates how our general formulation of (x) and (xx) (Section 3) extends to other domains, offering broad potential for future work.
22

---

Published as a conference paper at COLM 2025
E Limitations
We note several limitations of our current benchmark:
REFUTE benchmark is based on solutions in C++. It could skew the benchmark in favor of models with higher C++ capability. However, this an inherent property stemming from the nature of competitive programming data source. While Python-based version is possible, most real-world competition data C++. C++ is preferred due to its efficiency and suitability for strict runtime constraints. We highlight that the models we test are proficient in C++ given that their competitive programming capabilities are reported based on C++ solutions. This is also because there is abundant high-quality C++ code available online as training data for competition tasks.
REFUTE benchmark is only proof of concept for how LLM falsification. We highlight that REFUTEE benchmark is not representative of general falsification capabilities, Our work is meant to demonstrate that: (1) Falsification capabilities can be evaluated as generating code that creates counterexamples which demonstrate claim or solution is wrong. (2) As first step, we chose domain where automatic verification is relatively easy for novel counterexamples, and recent reasoning models already perform well at solution generation. We found that despite this, they are not good at generating counterexamples for incorrect solutions. More research will be required to create falsification benchmarks with better domain coverage and diversity
23

---

Published as a conference paper at COLM 2025
F
Prompts
In this section, few-shot samples are denoted by <examples>, Similarly, long code snippets have been reduced to [...]. Full prompts with our samples and expert rationales are available in our code repository.
Task Description Format
The problem statement along with the incorrect code is presented to the model in this format. In all query formats described below, this is referred to
## Statement
ggroblem_statemee
Time Limit: <time_limit>
Memory Limit: Limits
## Input Format <input_format>
#* Output Format format
#* Example Input
cexample_inputs>
## Example Output
<example_outpurs
## Note <optional_notes>
## Incorrect Code
<incorrect_code>
E1 Zero-Shot
System: You expert at finding errors in code. You will be given buggy code and the complete description of problem it intends to solve. Your job is to find a valid input in the expected format, satisfying all input constraints, on which the code fails.
Write program to print this failing test-case. Provide this to in the exact XML format show below. Do not include anything other than your thoughts and this program to print failing test-case.
<reason>
[Your concise reasoning here]
</reason>
24

---

Published as a conference paper at COLM 2025
<action>
<code>
[code to print failing test-case]
</code>
<lang 3</lang>
</action>
User: You are now given problem description and buggy code. Help find failing test-case by providing script in the exact XML format mentioned earlier. Don't output anything else.
<task_descriptionn
F2
Few-Shot
You are an expert finding errors code. will be given a bugay code and the complete description of the problem it intends to solve. Your job is to find a valid input in the expected format, satisfying all input constraints,
System:
which the code fails.
Write program to print this failing test-case. Provide this to me exact XML format show below. Da not include anything other than your thoughts and this program to print failing test-case.
<reason>
[Your concise reasoning here]
</reason>
<action>
<code>
[code to print failing test-case]
</code>
<yahon 3</lang>
</action>
<examples>
User: You given problem description and buggy code. Help find failing test-case by providing a script in the exact XML format mentioned earlier. Don't output anything else.
<task ttaskddescription
F.3
Zero-Shot Agent
You are an expert at finding errors code. You will given buggy code and the complete description of the problem it intends to solve. Your job is to find valid input in the expected format, satisfying all input constraints, on which the code fails.
In your final submission, you need provide code to print this failing- test case along with your reasoning to back it. If your generated test-case
25

---

Published as a conference paper at COLM 2025
doesn't match the input constraints and expected format, you will receive VALIDATION_ERRE with relevant feedback. In such case, you will have upto chances fix your submission. make your submission, output an XML in the following format:
<reason>
[Your concise reasoning here]
</reason>
<action>
<code>
[code print failing test-case]
</code>
<anno 3</lang>
</action>
You are also equipped with a code execution tool that you can use upto times before your final submission. This will help you understand and narrow down to the failure case. You can execute any code you want with an arbitrary input. You will receive the output in response. Each code execution will be limited to 30 seconds. To use this tool, output an XML in the following format:
<reason>
[Your concise reasoning here]
</reason>
<action>
<name>run_code</nee
<code>
[source the code you want to obtain output from]
</code>
<lang> [language of the source code -- one of 'Python 3' or 'C++ 23 23'
</action>
<action>
<name>inpuue iitteeinnttpiiitt/nmeee
<code>
[code to print the input that will be passed to the code execution tool]
</code>
<lang> (Language the input printer one of 'Python 'C+ 23']</lanp
</action>
Your responses should ONLY an XML one of the two formats above. Thus, in an interaction, you will output an XML corresponding to the exeeexxcnttion tool upto 10 times, and then
output an for your final submission.
The interaction ends after you make a submission. **Use the code-execution tool gyneroussy** and only make submission once you're rr certain of having if you run out of your 10 attempts at the code -execution tool. You must the code-execution tool atleast once. Utilise it generously to understand the code and verify your thoughts.
found failing test-case,
User: You are now given problem description and buggy code. Help me find failing test-case using the exeeuexecttion tool and submission format provided above.
26

---

Published as a conference paper at COLM 2025
ttaskdeesciiptions
F4 ReAct Agent (With Sample Trajectory)
You are an expert at finding errors code. You will given buggy code and the complete description of the problem it intends to solve. Your job is to find valid input in the expected format, satisfying all input constraints, which the code fails.
In your final submission, you need to provide code to print this failing- test case along with your reasoning to back it. If your generated test-case doesn't match the input constraints and expected format, you will receive VALIDATION_ERAE ERRRRR with relevant feedback. In such case, you will have upto chances fix your submission. make your submission, output XML in the following format:
<reason>
[Your concise reasoning here] </reason>
<action>
<code>
[code print failing test-case]
</code>
<ython 3</lang>
</action>
You are also equipped with a code execution tool that you can use upto 18 times before your final submission. This will help you understand and narrow down to the failure case. You can execute any code you want with an arbitrary input. You will receive the output in response. Each code execution will be limited 30 seconds. the following format:
this tool, output XML in
<reason>
[Your concise reasoning here] </reason>
<action>
<name>>run_cod<</nam>>
<code>
[source the code you want obtain output from]
</code>
<lang> [language of the source code -- one of 'Python 3' or IC+ 23 <3]]</lagg>
</action>
<action>
<name> hatneeeitpt_pittt/nmmaa
<code>
[code to print the input that will be passed to the code execution tool]
</code>
<lang> (langugge the input printer one of 'Python 'C+ 23']</lang
</action>
responses should be XML in of formats above. Thus, in an interaction, you will
27

---

Published as a conference paper at COLM 2025
output an XNL corresponding to the code-execution tool upto 16 times, and then output an
your final submission.
The interaction ends after make a submission. **Use the exdetexttttion tool generously*x and only make submission once you're certain of having found failing test-case, if you out of your 10 attempts the code -execution tool. Your first output MUST use the code-execution tool.
Here's an example of a valid interaction. You'll be given an input: <task_ descriptocn
You could respond with:
<reason>
The answer will not be 'Infinity' only when there is atleast one reaction each with requirements of the form (a, 8, 0), (0, b, 0), and (0, 9, c), where a, b, с This sets an independent upper bound on each of three chemicals. The code seems to correctly handle this case.
In the other case, it appears first sort the requirements array. It then continually adds the requirements (b, in monotonic sequence which is increasing
decreasing in c. In another set, it stores the values (b[1 1] c[i]) derived from consecutive entires the earlier sequences, with the claim being that the optimal answer is always of this configuration. The claim seems to be correct, but want to dig deeper into the implementation.
First, to verify my understanding, have added an assertion to check whether prev(it) while pruning the monotonic sequence always refer to pl. moved the original solver code to separate function, and call it of time
repeatedly on randomly generated sequences. It this code without throwing runtime error, I will know that my understanding of that part was correct. Since I'm generating the inputs randomly inside the code, don't need to provide separate input generator.
</reason>
<action>
<name>rrun_code<<name
<code>
[...]
</code>
<lang>C++ 23</lang>
</action>
<action>
mname>>inuttprrnnkk/me
<code>
print("")
</code>
<ython 3</lang>
</action>
You will then be given the input: {"status": LIMM_LLMMTT_EXCEEE "output": "Error while running source code "}
You could then reply:
<reason>
Great, understood that part correctly. find it suspicious that the code isn't checking if b[i 1] before adding corresponding option in
28

---

Published as a conference paper at COLM 2025
the st multiset. Because if b[i 1] == 0 for some i in the monotonic sequence ds, then I can't pick -1 valid amount of chemical b.
Let me an assertion before every addition to st and run on the sample first.
</reason>
<action>
<hame>run_codd<<<namee
<code>
[...]
</code>
<lang>C+ 23</lang>
</action>
<action>
<name>>imott_prrnt<//mme
<code>
(4int(4)
print ("0 0 5")
print(" 5 8*)
print 0 8*)
print("6 7 8")
</code>
<ython 3</lang> </action>
You would then be given the input:
("status": "RUNTIME_ _ "output": "Error while running source code: Assertion failed: (fit).f: 0, file ./tmp/ /'ope/ccode.cp,, line 79\r\n", return_code": 3}
You could then reply:
<reason> Interesting, so even though knew that code does provide correct output on the samples, it fails the assertions that put. So to exploit this, I need to find test-case where the wrong insertions to st do actually affect the output. I'll just plug the modi code (f.e. one that doesn't insert invalid options into st) separate function, and then compare both the given code and this modified on random small inputs until find one on which they differ. </reason>
<action>
Chame>rrun_code<<nnme
<code>
[...]
</code>
<lang>C++ 23</lang>
</action>
<action>
<name>>ippuut_rrink//naaees
<code>
print("")
</code>
<ython 3</lang>
</action>
29

---

Published as a conference paper at COLM 2025
You will then be given the input: {"status" "OK", "output": "7irine 7\rnne 0\rine 9 2\r\n2 e 8ir\n6 5 8\r \n7 0/rine 3'rinfixed: 12, original: 13tr\n")
You could choose to then reply with your final submission:
<reason>
Now that I've found an input on which I think the code is wrong (since output 13 instead of 12), will use that as the submission to make vña @rint_fail_casse
</reason>
<action> <name>print, fail_caae</name>>>>>
<code>
""""Ar\n 0 7\r\ne 1 @\rine 2\r\n2 8\r\no 8\r\n7 0\rine 3\r\n *..
psint(s)
</code>
<lang>Python 3</lang> </action>
User: You are now given problem description and buggy code. Help me find failing test-case using the code-execution tool and submission format provided above.
<task_descripttinn
E5
Few-Shot Random Search
You expert at finding errors in code. You will be given buggy code and the complete description of the problem it intends to solve. Your job is find a valid input the expected format, satisfying all input constraints, on which the code fails.
System:
Write program to print this failing test-case. Provide this to in the exact XML format show below. Do include anything other than your thoughts and this program to print failing test-case.
<reason>
[Your concise reasoning here]
</reason>
<action>
<code>
[code print failing test-case]
</code>
Python 3</lang>
</action>
<examples>
User: You are given problem description and buggy code. Help find failing test-case by providing script in the exact XML format mentioned earlier. Don't output anything else.
30

---

Published as a conference paper at COLM 2025
itask_descriptione
F66
Zero-Shot (Oracle)
System: You expert at finding errors in code. will be given the complete description problem statement, along with buggy code correct code to solve it. Your job is to find valid input in the expected format, satisfying all input constraints, on which the buggy code fails.
write program to print this failing test-case. Provide this to in the exact XML format show below. Do not include anything other than your thoughts and this program to print failing test-case.
<reason>
[Your concise reasoning here]
</reason>
<action>
<code>
[code print failing test-case]
</code>
<ython 3</lang>
</action>
User: You are now given a problem description, a buggy code, and a correct code. Help find a failing test-case by providing a script in the exact XML format mentioned earlier. Don't output anything else.
<task_descripttin>
#* Correct Code
<ground_truth_com taadd__ttttt_deee_eee
E7
Random Search (Oracle)
System:
expert testing code. You will be given the complete description problem statement, along with a buggy code and correct code to solve it. You have to find a test-case where the buggy code fails. To do this, write randomised test case generator script. I wi ll then repeatedly compare the buggy code against the correct solution the generator's case found.
You
outputs until a failing
Aim for diversity and coverage in the generated tests. Feel free to vary the range of all variables as needed while staying within problem constraints.
Provide the test-case generator me the exact format I below. Do not include anything else in your responses. Your code must written in Python 3 or C++ 23.
<action> <name> gentraatttttttt//aa
31

---

Published as a conference paper at COLM 2025
<code>
[code to generate random test-cases)
</code>
<lang> [Python 3 | 23] </lan>>
</action>
<examples>
User: You are now given problem description, a buggy code, and a correct code. Write testcase generator script in the exact XML format mentiones earlier to find where the buggy code fails. Don't output anything else.
<task_description>
## Correct Code
@grunn__truth_code>
32


Reviews:
[{"review_id": "bstYehkJvb", "reviewer": "Reviewer_LiKZ", "summary": "This work presents a compelling and timely investigation into the capabilities of LLMs to engage in falsification through counterexample generation. It also introduces the REFUTE benchmark, aiming to assess LLMs' proficiency in identifying and challenging subtly incorrect algorithmic solutions. In terms of quality, the paper demonstrates a high level of technical soundness. The authors designed the REFUTE benchmark, ensuring that the tasks are both challenging and relevant to the evaluation of LLMs' reasoning abilities. The experimental setup is robust, with comprehensive evaluations that compare various LLMs' performances on the benchmark. The results are presented with clarity, and the authors provide thoughtful analyses that delve into the nuances of the models' successes and failures. As to the clarity, I found the paper well-written and well-structured, which is easy to understand and analyze. The introduction effectively sets the stage, articulating the motivation and significance of the study. The subsequent sections are organized logically, guiding the reader through the methodology, experiments, and discussions. In terms of originality, the paper makes a novel contribution by shifting the focus from LLMs' ability to generate correct solutions to their capacity to identify and challenge incorrect ones. The significance of this work is considerable. By highlighting the importance of falsification in algorithmic reasoning, the work addresses a critical aspect of AI development that has implications for the reliability and trustworthiness of LLMs. The REFUTE benchmark provides a valuable tool for the community, enabling more comprehensive evaluations of LLMs and potentially guiding the development of models with enhanced reasoning abilities.", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "From my understanding, the novel and interesting contribution of this work is introducing the REFUTE benchmark, which shifts evaluation from traditional solution generation to the more cognitively demanding task of falsification through counterexample creation. This represents a clear step forward in how we assess model understanding and aligns closely with COLM's emphasis on deeper reasoning, self-reflection, and model robustness. In my opinion, the work is both conceptually novel and practically impactful, which addresses a blind spot in current benchmarks and proposes an evaluation setup that is grounded in formal semantics and executable verification, and I think it would be an interesting part of this work. The REFUTE benchmark is curated from real Codeforces problems with subtly incorrect solutions, ensuring that counterexample discovery is non-trivial and requires reasoning beyond surface-level understanding. From my view, the work's empirical design is very well, with evaluations across top-tier models using varied prompting strategies and agentic code execution. The finding that models capable of solving nearly 50% of problems fail to falsify over 90% of incorrect solutions is striking and reveals a deep limitation in current LM capabilities. I think this insight highlights a critical challenge in developing self-correcting AI systems, which is scientifically valuable. Beyond the methodology and analysis of this work, I see a strong technological impact. The benchmark fills a gap in the ecosystem of evaluation datasets, and I think it has the potential to become a community standard for measuring falsification. Its dynamic update strategy mitigates data leakage and ensures long-term relevance. Additionally, I think it would be important to mention that the work articulates a forward-looking vision: that models should be able not only to propose answers but also to challenge and reflect on them. This reframing of evaluation is intellectually bold and practically necessary as we move toward more autonomous and trustworthy AI.", "reasons_to_reject": "While I think this work shares promising results and it has a valuable impact to be used in the community, I would like to share some concerns, and I hope the authors could find them useful. Please note that these concerns are to the best of my knowledge, and the main goal is to have a thorough discussion. \n\nIt seems to me that the paper frames counterexample generation as crucial for scientific discovery, yet the actual work is confined to a very specific domain of competitive programming problems. All experiments are conducted on REFUTE, a collection of 324 algorithms coding tasks drawn from Codeforces contests. While the authors hint at broader goals \" with an eye towards subtly incorrect scientific claims \", I do not see any provided evidence that the approach generalizes beyond coding scenarios. I think it disconnect between the grand motivation (falsifying scientific hypotheses) and the limited score (debugging programming contest solutions) contributes feel narrow and conceptually overclaims. In its current form, the work comes across as a specialized benchmark for code debugging rather than a general advancement toward AI-driven falsification in science. The framing promises much more than what is actually achieved, which could mislead readers about the significance of the results. \n\n---\nThe other thing that I would like to add is about the experimental section. From my understanding, there is no comparison to non-LLM approaches or human performance. A simple fuzzing or symbolic execution baseline could have provided a point of reference (e.g., can an automated programmatic method find counterexamples for any of these buggy solutions?). The authors claim to filter out trivial cases solvable by random search, yet they never quantify how a brute-force or heuristic search might perform on the remaining problems. I think this missing baseline makes it hard to gauge the true difficulty of REFUTE and how much LMs lag behind simpler methods. \n\nMoreover, it seems that the evaluation is focusing only on success rates, which are extremely low, under 9% even for the best agent, without deeper analysis. Importantly, I think the paper would need to provide more insights into why the models fail. From what I have discovered in this work, providing the correct solution does not help much (only marginal gains in counterexample success), which highlights a fundamental gap between solving and falsifying. However, the authors do not investigate this gap beyond reporting the numbers. There are several things that I am going to mention. For instance, (1) Are the models failing because they can not comprehend the incorrect code logic, or because they can not generate complex inputs, or due to context length issues? (2) Are certain categories of bugs (e.g., greedy algorithm errors, off-by-one mistakes, etc.) more challenging than others? - I think knowing the details of them could be valuable for the community, and without understanding what the fundamental obstacles are, it would be a bit challenging moving forward.\n\n---\nThe last comment that I have here is: The protocol allowing models up to 10 attempts with an \" agentic \" feedback loop is a reasonable approach inspired by how humans debug code. However, from my understanding, the paper does not justify key settings (why 10 attempts? Is this a random number? How sensitive are results to this limit?) and provides no ablation on the prompt strategies. It's also not clear to me whether the few-shot demonstrations were tuned for optimal performance or how those examples were chosen, which could affect success rates. The result table aggregates outcomes across all 324 tasks, but I think the paper could benefit from at least some breakdown (even if in appendix) - none is given, so it is a bit challenging to know if, say, a handful or trivial cases are being solved vs. everything else failing, or if all failures are uniformly distributed.", "questions_to_authors": "I would invite the authors to check the previous section where I shared some feedback about the weaknesses of the work, but I have an additional suggestion in order to strengthen their interesting work. I would suggest improving the empirical foundation and providing deeper insights into the challenges of counterexample generation, and consider conducting a comprehensive error analysis that categorizes the types of incorrect solutions and corresponding counterexamples within the REFUTE benchmark. By identifying patterns in the failures of LMs, such as specific algorithmic errors they struggle to detect or particular problem structures that hinder counterexample generation. I think this analysis would not only elucidate the specific reasoning deficiencies in existing LMs but also guide future research directions aimed at enhancing model robustness and self-reflection capabilities.", "extra_scores": {"ethics_concerns_details": "N/A"}}, {"review_id": "AoFxuF2YGg", "reviewer": "Reviewer_J67i", "summary": "This paper introduces a benchmark for finding counter-examples for incorrect solutions to programming questions. The benchmark is made up of Codeforces submissions and is filtered according to a list of criteria ensuring the benchmark requires algorithmic reasoning for the model to solve (avoiding brute force, syntax mistakes etc.). The paper evaluates a series of frontier models on the benchmarks across a number of different evaluation strategies (prompting, agentic interation, enforced random search). There is some analysis of failure modes.", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- There seems to be a great need in the community for benchmarks on different types of reasoning than simply solving math/algorithmic problems, especially for verification and falsification. I agree with the authors that this type of task helps delineate reasoning about the problem from simply parroting patterns from similar solutions (which models may be doing when generating solutions to these problems)\n- This paper seems to be very thorough in the different methods of using the benchmark to evaluate the model (prompting, interaction, random search etc.). The interaction in particular is a great idea to assess whether a model is able to edit the code and interpret the difference in output (very valuable for co-operative programming type settings).\n- The filtering process for selecting questions also seems to be quite thorough.", "reasons_to_reject": "- I feel that the framing of this paper differs from the contribution. The framing in the introduction largely focuses on falsifying hypotheses in scientific discovery while the main contribution is to introduce a benchmark for finding counter-examples to programming problems, mostly in C++. It it not clear to me that these are the same kinds of reasoning and that being better at one would help the other. I don't see the value of the discussion related to scientific discovery.\n- There are no error bars in the results tables. Was the evaluation conducted over multiple runs? It seems difficult to conclude how significant these results are and if models perform better on one evaluation strategy over others.\n- The benchmark seems to massively oversample solutions in C++. Though I understand many Codeforces submissions are in C++, I wonder if this doesn't skew the benchmark in favor of models with higher C++ capability. I would feel more comfortable that the benchmark result actually reflected the ability of a model to find counter-examples if more languages were represented or some experiment was done to show this is not the case.\n- Including an expert human baseline in Table 1 could help interpret that 9% result for o3-mini. I'm not sure how good/bad that is.\n- In general, I think the contribution would be more valuable if the error analysis/identification of failure modes was more thorough. I don't feel that I've come away with a strong understanding of the specific failure modes of different models. There are no clear trends in the error analysis and it's surprising to me that models perform almost equally as well across problem difficulty and # test cases passed. Perhaps a more thorough investigation is needed.", "questions_to_authors": "- I'm curious about the formula for problem selection. Did you try other coefficients for these terms / Did this make a difference in the types of problems sampled and the performance of different models?\n- Could you articulate more clearly why the benchmark should not evaluate counter-examples that give OOT errors? Would identifying these gaps in the program not also display some reasonable understanding of the solution?\n- Some of the results in Table 1 are counter-intuitive to me. Why do you think zero-shot performance is sometimes higher than few-shot or w/ correct answer? This would be easier to interpret with error bars. I have a similar question for the ReAct setting w/ demo.\n- Could you include a couple samples of problems in your benchmark? It's difficult to assess the quality of the benchmark/how much it reflects the type of algorithmic reasoning it claims to without seeing a few examples.\n- I'm also curious why these models (which are generally capable at programming and can solve many of the Codeforces questions) fail to write simple brute-force code? (this was identified as the key failure mode for random search). Could it be related to prompting strategy?", "extra_scores": {}}, {"review_id": "dsXU2HLFgg", "reviewer": "Reviewer_uUPk", "summary": "This work focuses on whether LLMs can find suitable counterexamples for fragile code appearing in programming problems. The authors collect problems from Codeforces, carefully clean the data, and design a new benchmark called REFUTE. After testing on state-of-the-art models, they find that existing LLMs may face greater challenges in error verification.", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. This work presents a novel perspective and addresses a critical problem: generating high-quality test cases has always been a challenge for LLMs. By designing this benchmark, the authors help draw the community’s attention to this issue and provide an effective testing scheme for future solutions.\n2. This work conducts evaluations on state-of-the-art LLMs, ensuring both the challenge and the necessity of the proposed benchmark.", "reasons_to_reject": "However, I believe there are several aspects where this work could be further improved:\nFirst, the coverage and diversity of the benchmark are somewhat insufficient. The dataset is sourced from a few programming languages within Codeforces Division, and there is still a lack of sufficient evidence to prove that it is fully representative as a benchmark.\nSecond, the data quality of the benchmark is not fully demonstrated. Although the authors employed a large number of carefully designed automated methods to clean the data, credible evidence is still lacking to confirm that the benchmark data is of high quality.\nThird, the authors should consider incorporating some reflective methods into the baselines to enhance the comprehensiveness of the benchmark [1, 2].\n[1] Self-Refine: Iterative Refinement with Self-Feedback.\n[2] Self-Consistency Improves Chain of Thought Reasoning in Language Models.", "questions_to_authors": "The validation methodology adopted by the authors also deserves reconsideration. For example, if an LLM-generated counterexample leads to a program crash, it should be highly encouraged in the benchmark (as it exposes serious flaws in the solution); I would like to know how the benchmark handles some other special cases.", "extra_scores": {}}, {"review_id": "vzUqTlWCWo", "reviewer": "Reviewer_sybC", "summary": "This paper introduces a novel benchmark, REFUTE, designed to evaluate a model's ability to falsify hypotheses. Based on code execution, the benchmark tests whether models can generate counterexamples for subtly incorrect solutions. The benchmark is well-curated and will be dynamically updated. It reveals several findings—for example, even OpenAI's o3-mini (high), when provided with code execution feedback, can generate counterexamples for fewer than 9% of the incorrect solutions in REFUTE. The authors also conduct further analyses and uncover interesting results, such as the observation that verification can sometimes be more challenging for models than solving the original problem correctly.", "questions": "", "limitations": "", "rating": 7, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. The research question addressed by the authors is valuable and timely. Even state-of-the-art models such as o3-mini (high), when equipped with code execution feedback, are able to generate counterexamples for <9% of incorrect solutions in REFUTE. This benchmark offers a relatively comprehensive evaluation of a model’s reasoning capabilities, particularly in falsification. It also has the potential to assess agentic capabilities when models are used in more autonomous or iterative settings.\n2. REFUTE is a dynamically updating benchmark, which is especially important in the current era where data contamination is a growing concern. Continuous updates help ensure the benchmark remains challenging and free from training leakage.\n3. The dataset is carefully constructed and yields insightful findings. For example, the results support the hypothesis that LLMs' difficulty in repairing their own incorrect code is often due to their limited ability to identify errors in the first place. In some cases, verification proves to be more challenging for models than solving the problem correctly.", "reasons_to_reject": "1. While the authors note that most examples are in C++ because of its popularity in programming competitions, Python is undeniably the dominant language in the AI and machine learning community. From this perspective, the benchmark would be more broadly applicable and valuable if it included a greater proportion of Python examples.\n2. The paper leaves some questions unanswered regarding when and why models can successfully generate counterexamples. Although the authors attempt an analysis across three attributes, they do not observe any clear patterns or trends. This may point to limitations in the benchmark’s design or coverage, particularly in its ability to disentangle the factors that influence counterexample generation success.", "questions_to_authors": "1. Could the authors provide a discussion on how to improve the model’s ability to generate counterexamples based on the observed shortcomings? For example, what kinds of data or training methods might help enhance this capability?\n2. In the analysis of factors that influence the model's ability to generate counterexamples, could the authors examine model performance across different algorithm types or problem topics? This could be a more meaningful attribute, as some algorithmic patterns might inherently make counterexample generation more difficult, while others might be easier. An analysis along these lines could offer deeper insights into the benchmark’s diagnostic power.", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper presents a novel benchmark, REFUTE, for assessing the falsification capabilities of language models. The authors' approach leverages code execution to evaluate the ability of models to generate counterexamples for incorrect solutions, providing a comprehensive assessment of their reasoning capabilities. While the paper's scope is limited to competitive programming, the author addressed several concerns raised by the reviewers include quantitative and qualitative error analysis. Overall, I recommend accepting the paper due to its originality, and potential to inform future research, particularly in the areas of algorithmic reasoning and falsification. 

Several potential areas of improvement: (1) empirically connect the ability to falsify to verification of outputs as correct or incorrect, (2) expanding the dataset to include Python problems, (3) analysis of benchmark performance as a function of test-time compute.
Decision: Accept