# Disproving Program Equivalence with LLMs

arXiv: https://arxiv.org/abs/2502.18473 · HTML: https://mlsanity.com/paper/2502.18473/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 21 references that are in the map.
- First posted on arXiv 5 Feb 2025.

## Builds on (most cited first, 11 of 11)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Universal Self-Consistency for Large Language Model Generation](https://mlsanity.com/paper/2311.17311/) (2023)
- [Automated Unit Test Improvement using Large Language Models at Meta](https://mlsanity.com/paper/2402.09171/) (2024)
- [On Leakage of Code Generation Evaluation Datasets](https://mlsanity.com/paper/2407.07565/) (2024)
- [SemCoder: Training Code Language Models with Comprehensive Semantics Reasoning](https://mlsanity.com/paper/2406.01006/) (2024)
- [ChangeGuard: Validating Code Changes via Pairwise Learning-Guided Execution](https://mlsanity.com/paper/2410.16092/) (2024)
- [Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules](https://mlsanity.com/paper/2109.10476/) (2021)

## Built on by (most cited first, 5 of 5)

- [From Code Foundation Models to Agents and Applications: A Comprehensive Survey and Practical Guide to Code Intelligence](https://mlsanity.com/paper/2511.18538/) (2025)
- [Scaling Agentic Verifier for Competitive Coding](https://mlsanity.com/paper/2602.04254/) (2026)
- [Towards Verified Code Reasoning by LLMs](https://mlsanity.com/paper/2509.26546/) (2025)
- [Barriers to Discrete Reasoning with Transformers: A Survey Across Depth, Exactness, and Bandwidth](https://mlsanity.com/paper/2602.11175/) (2026)
- [How Robustly do LLMs Understand Execution Semantics?](https://mlsanity.com/paper/2604.16320/) (2026)

## Abstract (arXiv)

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.