Pith. sign in

REVIEW 3 major objections 4 minor 19 references

Disproving Program Equivalence with LLMs

T0 review · 3 major / 4 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read ProbeGen, a white-box, execution-guided search that asks an LLM to generate probe programs until two implementations of the same interface produce observably different results, and on the LBPP benchmark it flags an estimated 18.7% of…

desk verdict The strict counterexample rate is robust; the filtered 18.7% headline rests on a fragile LLM filter precision estimate. read the letter →

arxiv 2502.18473 v1 pith:BHA6VFQJ submitted 2025-02-05 cs.SE cs.LG

Miltiadis Allamanis , Pengcheng Yin This is my paper · ORCID
classification cs.SEcs.LG
keywords programequivalenceprobegenerationcounterexamplesearchdifferentialtestingLLMexecutionfeedbackcodesynthesisevaluationsemanticself-consistencyunittestadequacy
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that the standard way of judging whether an LLM-generated program is correct — running a small set of hand-written unit tests — is too weak, and that the missing behavioral differences can be found by asking an LLM to write probes. A probe is a program that feeds inputs to an interface and returns a value, so that if two implementations produce different probe values they are functionally different, with the difference proven by execution. ProbeGen iterates this process: the LLM sees both implementations and the execution outputs of all previous probes, then generates new probes until the outputs diverge, after which a second LLM filter judges whether the divergence is significant or an artifact of unspecified behavior. On the LBPP code-synthesis benchmark, ProbeGen disproves equivalence to the ground truth for 24.3% of the samples whose unit tests pass, a figure that drops to an estimated 18.7% after correcting for the filter's measured 77.1% precision. If the paper is right, a sizable fraction of code currently marked correct carries hidden semantic differences, and the same machinery, used to cluster candidate solutions by observable behavior, improves pass@1 by about 10%.

What carries the argument

The load-bearing object is the probe: a function $p$ that takes an implementation of an interface and returns a value, so that $p(f_i) \neq p(f_j)$ for two implementations is an execution-proven disproof of their functional equivalence. Unit tests are the special case where the probe returns True or False by comparing against an expected output; generating probes is easier because the LLM only has to produce valid inputs, not predict outputs. ProbeGen is an iterative tree search: at each turn the LLM receives the source of both implementations plus the string-represented outputs of every prior probe, and samples new probes as Python generators, with type checking enforcing explicit preconditions; search strategies trade branching factor against depth, and the paper's Decreasing strategy reaches a 90% probability of finding an existing counterexample at roughly a quarter of the cost of a full uniform search. The final component is the spurious-counterexample filter, another LLM prompt that decides whether a divergence violates implicit preconditions or concerns output details the task leaves unspecified; its measured 77.1% precision is what converts the raw counterexample rate of 24.3% into the headline estimate of 18.7%.

What would settle it

Adjudicate every unit-test-passing counterexample ProbeGen produces on a fresh sample of, say, 1,000 LBPP outputs, using three independent annotators per example instead of two authors on a subset. If the agreement rate on significant differences falls well below 77.1%, or if the implied corrected hidden-divergence rate approaches zero, the claim that ProbeGen finds substantial semantic differences that unit tests miss would be falsified.

Watch

Extended reading notes

Core claim

The paper's central claim is that functional-equivalence checking between two implementations of an interface can be carried out by an LLM-driven, execution-guided search for probe programs, and that this search frequently finds counterexamples in code that passes the official unit tests. In the LBPP code-synthesis benchmark, ProbeGen finds counterexamples in 24.3% of the samples whose unit tests pass; applying the paper's LLM-based filter for spurious counterexamples, and correcting for the filter's measured 77.1% precision, brings that estimate down to 18.7%. The paper further claims that the same probe machinery, used to partition candidate implementations by observable behavior, supports a semantic form of self-consistency: choosing the largest semantic cluster raises pass@1 from 40.6% to 44.6%, a roughly 10% relative gain, while the same procedure without spurious-counterexample filtering yields no gain at all.

Load-bearing premise

The headline numbers stand or fall with the LLM filter that decides which counterexamples count as real differences: its precision is estimated at 77.1% from human annotations of a two-per-problem subset, so if that estimate is optimistic, the 18.7% figure and the 10% pass@1 improvement both shrink.

Editorial extensions

If this is right

  • Running ProbeGen on unit-test-passing samples before declaring a code-generation result correct would reclassify a reported 18.7% of supposedly correct samples as behaviorally different from the ground truth.
  • Where unit tests do not exist, ProbeGen can act as the equivalence oracle itself, since it needs only the implementations and a value-equality operator; it agrees with unit tests on 83.3% of the outcomes for mutually runnable samples.
  • Semantic self-consistency becomes practical: choosing the largest semantic cluster of candidate implementations improves pass@1 by about 10% relative to the baseline, and this gain disappears when spurious counterexamples are not filtered.
  • The recursive success-probability estimator gives a budget-planning tool: for a given LLM, the Decreasing search strategy reaches 90% probability of finding an existing counterexample at roughly a quarter of the cost of a full uniform search.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the only requirements are two executable implementations, a value-equality operator, and bounded execution time, the same probe search could power change-validation tools that compare code before and after an edit — an application the paper names but does not develop.
  • The headline 18.7% is as much a measurement of the LBPP test suites as of the models; rerunning ProbeGen on other benchmarks would yield a directly comparable hidden-divergence rate that quantifies how much semantic slack different test suites leave.
  • The method's practical bottleneck is not finding counterexamples but deciding intent: attaching formally generated preconditions to the significance filter, which the paper cites as adjacent work, would move the pipeline toward verifiable significance instead of relying on the 77.1%-precision judge.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces ProbeGen, a white-box method that uses LLMs with execution feedback to generate probes (input usages) that expose behavioral differences between code implementations, thereby disproving strict functional equivalence. On the LBPP Python benchmark, the authors report that ProbeGen disproves 24.3% of samples that pass the provided unit tests after applying an LLM-based spurious-counterexample filter, and estimate 18.7% (abstract: 18%) after correcting for the filter's measured precision of 77.1%. The paper also uses ProbeGen for semantic clustering and semantic self-consistency, reporting a pass@1 improvement from 40.6 to 44.6. The core mechanism is logically sound: a probe that produces different outputs on two implementations deterministically disproves equivalence. However, the headline quantitative claims rest on a small, non-random human-annotated sample for filter precision, with no confidence intervals and no correction for filter recall.

Significance. If the empirical claims are reliable, the paper makes a useful contribution: it provides a practical method to complement weak unit tests, a new task for LLM code understanding, and a search-strategy analysis with a generalized pass@k estimator. The strict counterexample detection is deterministic and falsifiable, and the appendix gives concrete trajectories illustrating the method. The significance is moderated, however, by the reliance on a single probe model (Gemini Flash 2.0), the subjectivity of the 'significant difference' notion (human κ=0.71), and the lack of statistical rigor in the headline estimates. The paper's central insight—that unit-test equivalence can hide detectable semantic differences—appears robust, but the magnitude of the effect is not yet established to the precision claimed.

major comments (3)
  1. [Sec. 4.2, Table 1, Abstract] The headline 18.7% (abstract: 18%) is computed as 24.3% × 0.771, where 0.771 is the precision of the spurious-counterexample filter estimated from a human-annotated sample described only as '2 samples per LBPP problem (if more than 2 exist)' among counterexample-positive, unit-test-passing samples. The annotation sample size is not reported, the sample is not random (problems with many counterexamples are capped and problems with a single counterexample are over-represented), no confidence interval is given, and the correction uses precision only while ignoring filter recall. Because the filter is acknowledged in Sec. 3.1 to be able to introduce false negatives, 18.7% is neither an unbiased estimate nor a bound. This is load-bearing for the paper's central quantitative claim. Please report the exact annotation sample size and selection procedure, compute a confidence interval for precision (e.g., Wilson interval), perform a sensitivity analysis of the headline rate under plausible precision and recall values, and state explicitly the recall assumption.
  2. [Sec. 5.1, Table 2] The semantic self-consistency improvement (pass@1 40.6 → 44.6, a 10% relative increase) is reported without any measure of uncertainty, and the effect disappears when the spurious-counterexample filter is removed (PROBE GEN w/o Filtering gives 40.6). Since this result depends on the same filter whose precision estimate is uncertain, the improvement is not yet established. Please provide confidence intervals or a significance test, and report the number of samples and a per-problem breakdown of the improvement.
  3. [Sec. 4.2, Human Evaluation] The inter-annotator agreement of κ=0.71, described as 'substantial', means that the ground-truth label of 'significant difference' is unstable for a nontrivial fraction of cases. The paper should quantify how this label noise affects the precision estimate—for example, by reporting per-annotator precision values or a confidence interval that accounts for annotator disagreement—and discuss how the headline rate changes under alternative annotation judgments. This is important because the filter's precision is the only quantity used to correct the central estimate.
minor comments (4)
  1. [Abstract / Sec. 4.2] The abstract's '18%' does not mention that this is an estimate after filtering and correcting for filter precision; the underlying strict counterexample rate (without filtering) is substantially higher (24.3% + 18.8% = 43.1% of unit-test-passing samples). Please state both the strict and the filtered rates explicitly to avoid conflating 'disproved equivalence' with 'significant semantic difference'.
  2. [Appendix, Fig. 6] The captions in Figure 6 are placeholder text ('Lorem ipsum') and do not describe the actual search-strategy contour plots; these must be replaced with informative captions before publication.
  3. [Appendix D] The sample trajectories contain several typos and formatting errors ('differneces', 'For For input', 'count_string(ßßßß)' with mismatched quotes, and an unescaped Greek sigma in the text). These should be corrected for readability.
  4. [Sec. 4.2] The relationship between the mutually-runnable percentages in Table 1 and the statement that unit-test-passing samples 'consist of 44.4% of all samples' is not fully explained; please clarify whether the 24.3% figure is computed over all unit-test-passing samples or only those that are also runnable by ProbeGen.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: ProbeGen's headline rate is an empirical measurement anchored to an external benchmark and human annotation, not a construction or fitted prediction.

full rationale

The paper's central derivation chain is empirical rather than definitional. ProbeGen generates probes with an LLM, executes them against LBPP implementations, and reports the observed counterexample rate among unit-test-passing samples; the 18.7% headline is obtained by taking the observed 24.3% rate and multiplying by a filter precision of 77.1% estimated from human annotations. No equation defines the claimed rate in terms of the filter's own outputs or a fitted parameter, and the strict unfiltered counterexample rate is deterministic once the probes execute. The LLM-based spurious-filter precision estimate is a possible threat to validity, because it is based on a convenience sample and does not correct for recall, but that is an empirical calibration concern, not circularity: the human annotations are independent of the probe-generation process. The only self-citation is Chen et al. (2023a) for traditional self-consistency, which is background and not load-bearing in the derivation. The semantic self-consistency improvement is also evaluated against LBPP unit tests, an external measure, so the central claims retain independent content.

Assumptions & free parameters 6 free parameters · 5 assumptions · 0 invented entities

The method sits on empirical assumptions about LLM behavior, benchmark authority, and filter reliability. No target result is derived from fitted constants, so the circularity burden is low; the main load-bearing premises are the ground-truth correctness of LBPP and the representativeness of the filter precision estimate.

free parameters (6)
  • Search budget for ProbeGen evaluation (branching K, depth D) = K=3, D=4 (max 21 LLM calls per sample)
    Chosen from Fig. 4c Pareto front on the same evaluation data; the reported counterexample rates depend on this budget. No sensitivity analysis is shown.
  • Number of probes NP in semantic clustering = 10
    Section 5.1 sets NP=10; no analysis of how clustering quality varies with NP.
  • Iterable comparison cutoff = first 1,000 elements
    Section 4: "If a function returns an iterable we resort to checking only their first 1k elements." Divergence beyond the cutoff is invisible, so equivalence judgments are blind to late differences.
  • Exception equivalence convention = All exceptions treated as equivalent
    Section 4: exception types and messages are ignored, which can hide meaningful behavioral differences in tasks where exception kinds matter.
  • Float and NaN equality conventions = math.isclose defaults; NaN considered equal to NaN
    Section 4: this equality operator design affects which output differences count as counterexamples.
  • PBT timeout for Hypothesis baseline = 3 CPU-minutes per target
    Section 4.2: the baseline's disagreement rate is bounded by this timeout; different timeouts would change PBT's measured performance.
assumptions (5)
  • domain assumption Probe execution is deterministic and side-effect-free on the supplied inputs.
    Sec. 2 assumes no randomness and that all side-effects can be captured by the probe; otherwise a single differing probe output does not establish non-equivalence.
  • domain assumption The LBPP ground-truth implementation and unit tests are correct and define the intended semantics.
    All pass@1 and correctness comparisons use LBPP ground truth as authoritative; the paper never validates the ground-truth implementation itself.
  • domain assumption Type annotations are sufficient preconditions for input generation and type checking.
    Sec. 4 uses typeguard and Hypothesis type annotations as preconditions; the paper notes implicit preconditions remain and are only handled by the LLM filter.
  • domain assumption The LLM filter's precision, measured on a small annotated subset, extrapolates to all flagged counterexamples.
    The 18.7% headline is computed using the filter's 77.1% precision from the human evaluation; this assumes the annotated subset is representative and the precision estimate is stable.
  • ad hoc to paper Unicode lowercasing behavior (e.g., Greek sigma) is part of the intended task semantics.
    Sample 2 in Appx D treats a difference in lowercasing 'ΣΣ' as a significant semantic difference; human annotators disagreed on some such cases, so this is a judgment call made by the authors.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Disproving Program Equivalence with LLMs." pith.science (2026). https://pith.science/paper/BHA6VFQJ

@misc{pith2026250218473,
  author       = {Pith},
  title        = {Pith review of: Disproving Program Equivalence with LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BHA6VFQJ}},
  note         = {Machine review of arXiv:2502.18473}
}
read the original abstract

To evaluate large language models (LLMs) for code, research has used manually created unit test-based benchmarks. However, these tests are often inadequate, missing corner cases and other implementation-specific oddities. This work introduces ProbeGen, a whitebox method that takes two or more executable pieces of code and searches for counterexamples to their equivalence. Comparing code semantics requires a deep understanding of code. We demonstrate that LLMs with execution feedback perform well at this task. In a common code synthesis benchmark, ProbeGen disproves 18% of samples considered equivalent to the ground truth by the benchmark-provided unit tests. Additionally, using ProbeGen, we can semantically cluster LLM samples for semantic self-consistency, improving pass@1 by 10% by unifying syntactically distinct but semantically similar samples.

Figures

Figures reproduced from arXiv: 2502.18473 by the authors.

Figure 1
Figure 1. Given a task description, an interface (function foo in this example) and a number of implementations of the interface, an LLM is asked to generate code (probe) that uses the inter￾face and causes the implementations to diverge in behavior (in this example, return different output lists). This provides a coun￾terexample where the implementations differ (as proven by their execution). However, the – often implicit – … view at source ↗
Figure 2
Figure 2. Sample probe vs. unit test for a fictional class interface Clazz. A probe only provides inputs in a usage example, whereas a unit test needs to make concrete assertions about the expected values. This makes probes easier to generate and allows us to perform more accurate testing for equivalence. While there are many ways to disprove functional equiv￾alence, we formulate the task as a probe generation task, which can… view at source ↗
Figure 3
Figure 3. PROBEGEN as a tree search process. At each step k independent samples may be drawn, up to a maximum depth D. When a probe successfully disproves the equivalence (green nodes) it forms a leaf node. the implementations efficiently and reduces the complexity of spurious counterexample filtering. We filter spurious counterexamples using the method of Sec. 3.1, the prompt of Appx. C, Gemini Flash 2.03 , and greedy decodi… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Relationship between the branching factor k and search depth to the probability S of successfully generating a probe that exposes a counterexample and the trade-offs with the inference cost. The two contour plots (left) show the probability of success (lighter color is…
Figure 5
Figure 5. Figure 5: Semantic Clustering through Probe Generation. Given a number of implementation f1, ... of an interface I we can generate probes that partition the set of implementations based on their outputs, clustering the implementations based on their semantics. ( [PITH_FULL_IMAG…
Figure 6
Figure 6. Figure 6: Caption A. Generating LBPP Implementations We ask LLMs to generate (possibly incorrect) solutions to the LBPP problems using the following prompt template. You are { adjective } { profession } who is writing Python code . You must respond with complete Python code that…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 10 canonical work pages

  1. [1]

    Automated unit test improvement using large language models at M eta

    Alshahwan, N., Chheda, J., Finogenova, A., Gokkaya, B., Harman, M., Harper, I., Marginean, A., Sengupta, S., and Wang, E. Automated unit test improvement using large language models at M eta. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, pp.\ 185--196, 2024

    work page 2024

  2. [2]

    Code T : Code generation with generated tests

    Chen, B., Zhang, F., Nguyen, A., Zan, D., Lin, Z., Lou, J.-G., and Chen, W. Code T : Code generation with generated tests. arXiv preprint arXiv:2207.10397, 2022

    arXiv 2022

  3. [3]

    Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. D. O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021

    arXiv 2021

  4. [4]

    Universal self-consistency for large language model generation

    Chen, X., Aksitov, R., Alon, U., Ren, J., Xiao, K., Yin, P., Prakash, S., Sutton, C., Wang, X., and Zhou, D. Universal self-consistency for large language model generation. arXiv preprint arXiv:2311.17311, 2023 a

    arXiv 2023

  5. [5]

    Teaching large language models to self-debug

    Chen, X., Lin, M., Sch \"a rli, N., and Zhou, D. Teaching large language models to self-debug. arXiv preprint arXiv:2304.05128, 2023 b

    arXiv 2023

  6. [6]

    Automated testing of refactoring engines

    Daniel, B., Dig, D., Garcia, K., and Marinov, D. Automated testing of refactoring engines. In Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp.\ 185--194, 2007

    work page 2007

  7. [7]

    J., Kaiser, G., Yang, J., and Ray, B

    Ding, Y., Peng, J., Min, M. J., Kaiser, G., Yang, J., and Ray, B. Semcoder: Training code language models with comprehensive semantics. arXiv preprint arXiv:2406.01006, 2024

    arXiv 2024

  8. [8]

    Endres, M., Fakhoury, S., Chakraborty, S., and Lahiri, S. K. Formalizing natural language intent into program specifications via large language models. arXiv preprint arXiv:2310.01831, 2023

    arXiv 2023

Show all 19 references
  1. [9]

    and Bishop, M

    Fink, G. and Bishop, M. Property-based testing: a new approach to testing for assurance. ACM SIGSOFT Software Engineering Notes, 22 0 (4): 0 74--80, 1997

    1997

  2. [10]

    ChangeGuard : Validating code changes via pairwise learning-guided execution

    Gr \"o ninger, L., Souza, B., and Pradel, M. ChangeGuard : Validating code changes via pairwise learning-guided execution. arXiv preprint arXiv:2410.16092, 2024

    2024 arXiv

  3. [11]

    Self-supervised learning to prove equivalence between straight-line programs via rewrite rules

    Kommrusch, S., Monperrus, M., and Pouchet, L.-N. Self-supervised learning to prove equivalence between straight-line programs via rewrite rules. IEEE Transactions on Software Engineering, 49 0 (7): 0 3771--3792, 2023

    2023

  4. [12]

    Compiler validation via equivalence modulo inputs

    Le, V., Afshari, M., and Su, Z. Compiler validation via equivalence modulo inputs. ACM Sigplan Notices, 49 0 (6): 0 216--226, 2014

    2014

  5. [13]

    P., Lahiri, S

    Lemieux, C., Inala, J. P., Lahiri, S. K., and Sen, S. CodaMosa : Escaping coverage plateaus in test generation with pre-trained large language models. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), pp.\ 919--931. IEEE, 2023

    2023

  6. [14]

    S., Wang, Y., and Zhang, L

    Liu, J., Xia, C. S., Wang, Y., and Zhang, L. Is your code generated by ChatGPT really correct? rigorous evaluation of large language models for code generation. Advances in Neural Information Processing Systems, 36, 2024

    2024

  7. [15]

    On leakage of code generation evaluation datasets

    Matton, A., Sherborne, T., Aumiller, D., Tommasone, E., Alizadeh, M., He, J., Ma, R., Voisin, M., Gilsenan-McMahon, E., and Gall \'e , M. On leakage of code generation evaluation datasets. arXiv preprint arXiv:2407.07565, 2024

    2024 arXiv

  8. [16]

    User interaction models for disambiguation in programming by example

    Mayer, M., Soares, G., Grechkin, M., Le, V., Marron, M., Polozov, O., Singh, R., Zorn, B., and Gulwani, S. User interaction models for disambiguation in programming by example. In Proceedings of the 28th Annual ACM Symposium on User Interface Software & Technology, pp.\ 291--301, 2015

    2015

  9. [17]

    McKeeman, W. M. Differential testing for software. Digital Technical Journal, 10 0 (1): 0 100--107, 1998

    1998

  10. [18]

    Self-consistency improves chain of thought reasoning in language models

    Wang, X., Wei, J., Schuurmans, D., Le, Q., Chi, E., Narang, S., Chowdhery, A., and Zhou, D. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171, 2022

    2022 arXiv

  11. [19]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.