Program Semantic Inequivalence Game with Large Language Models

Large Language Models (LLMs) can achieve strong performance on everyday coding tasks, but they can fail on complex tasks that require non-trivial reasoning about program semantics. Finding training examples to teach LLMs to solve these tasks can be challenging. In this work, the authors explore a method to synthetically generate code reasoning training data based on a semantic inequivalence game (SInQ): a generator agent creates program variants that are semantically distinct, derived from a dataset of real-world programming tasks, while an evaluator agent has to identify input examples for which they behave differently. The agents train each other semi-adversarially, improving their ability to understand the underlying logic of code. The approach was evaluated on multiple code generation and understanding benchmarks, including cross-language vulnerability detection (Lu et al., 2021), where the method improves vulnerability detection in C/C++ code despite being trained exclusively on Python code, and the challenging Python builtin identifier swap benchmark (Miceli Barone et al., 2023), where modern LLMs still struggle and the approach yields substantial improvements for one of the two base models fine-tuned. The authors release the code needed to replicate the experiments, as well as the generated synthetic data, which can be used to fine-tune LLMs.

Large Language Models (LLMs) are widely used by programmers, but while they perform well on common coding tasks they still struggle with non-trivial reasoning about program semantics (Miceli Barone et al., 2023; Maveli et al., 2025). This can lead to subtle bugs and to missed vulnerabilities and adversarial backdoors (Dinh et al., 2023; Dou et al., 2024), compromising the safety and security of generated code (Wang et al., 2024; Mohsin et al., 2024).

LLMs' coding capabilities are typically improved by fine-tuning on human-annotated and synthetically generated data. Human annotation is expensive and covers few non-trivial scenarios, while typical synthetic pipelines generate problem statements, solutions and unit tests and validate them by execution: this scales easily but gives limited coverage of problem types and introduces noise, as unit tests often misalign with the problem statements in edge cases.

Self-play trains agents by pitting them against each other, incentivizing them to discover and defend against unusual scenarios, and has reached human-level or superhuman play in Go (Silver et al., 2016, 2017b), Chess (Silver et al., 2017a), Dota 2 (OpenAI et al., 2019), StarCraft II (Arulkumaran et al., 2019) and dialogue games such as Diplomacy (FAIR, 2022). However, it typically needs external engines to enforce rules and score play, which is hard for open-ended tasks like coding; recreational coding environments such as CROBOTS are too domain-specific for general code reasoning. The authors are aware of only one concurrent work, Zhao et al. (2025), that uses self-play to train LLMs for arbitrary code generation, while Dong and Ma (2025) apply a similar idea to theorem proving.

In this work, the authors introduce a game based on program semantic inequivalence designed to train agents in code reasoning across arbitrary domains. By design, this game has no theoretical performance cap. They use it to train LLMs through self-play, demonstrating significant performance improvements on challenging tasks.

The approach pits two LLM agents against each other: the generator, Alice, creates challenging code-understanding problems that the evaluator, Bob, must solve (Figure 1). Alice is incentivized to deceive Bob into mistakes, but must also provide solutions, so its instances cannot be unsolvable; training both agents thus drives them towards a deeper understanding of program semantics. The game is based on the semantic (in)equivalence of programs, which allows precise verification of solutions, unlike natural-language specifications or unit tests, and is fundamentally linked to computability theory through reductions to Rice's theorem and the Halting problem. Reasoning about program (in)equivalence is also of practical value for identifying bugs and security vulnerabilities introduced during code refactoring.

Two programs P and Q are semantically equivalent if, for every input x, they either both halt with the same output or both fail to halt. Determining equivalence is fundamental to program verification and compiler design, but proving it automatically is hard: popular languages such as Java and Python are defined by natural-language specifications or reference implementations rather than formal semantics, and even where formal semantics exist, machine-checkable equivalence proofs for non-trivial code are challenging even for experts. The authors sidestep this by defining a program-understanding game that focuses solely on inequivalent programs.

The semantic inequivalence game is defined as a one-shot interaction between two players: the generator, Alice, and the evaluator, Bob:

1. Alice receives a program P and generates another program Q, which has to be inequivalent to P, along with a diverging input x such that P(x) ≠ Q(x).

2. The diverging input is verified by executing both programs on it. If P(x) = Q(x), Alice loses.

3. Bob receives P and Q and attempts to produce a diverging input x̂ (which may or may not be the same as x). If Bob correctly identifies a diverging input, he wins and Alice loses; otherwise, Bob loses and Alice wins.

Correctness is verified simply by executing the programs on the diverging inputs, with no need to generate or check formal proofs. Both agents are trained iteratively through repeated play. The source programs P are sampled from a dataset of short, self-contained exercises spanning many tasks (e.g. MBPP (Austin et al., 2021)), which keeps the game grounded in real-world coding problems; sampling P rather than letting Alice generate it too removes any incentive for it to produce obfuscated code that would not improve Bob's general reasoning. To approximate non-termination detection, a randomized time limit is imposed that significantly exceeds the typical runtime of source programs. Randomizing it prevents Alice from exploiting a fixed limit, e.g. by generating a Q that simply loops for a predetermined duration before returning P's output.

Unlike Go or Chess, where perfect play is possible, the game has no strict performance cap: under an infinite time limit Bob's task is undecidable (Appendix I), so in principle the agents can learn arbitrarily complex coding logic while staying grounded in real-world programs. The game is essentially zero-sum when Alice produces only valid outputs, but making it positive-sum can help integration with supervised fine-tuning (SFT) and avoid degenerate strategies (e.g. Alice generating cryptographically hard puzzles), as discussed in Appendix J.

Although the game is well-suited to reinforcement learning, RL was not available on the OpenAI API at the time of the experiments, so the authors devised a rejection-sampling fine-tuning implementation with explicit difficulty supervision.

When presenting the program pair (P, Q) to Bob, N evaluation responses are sampled and the difficulty of the pair is defined based on the number of correct assessments: d(P, Q, Bob) = 10(1 − N correct/N). For example, if Bob can solve the pair (P, Q) 40% of the time, the difficulty of this instance is 6.

During generation Alice is asked for a program with a specific target difficulty d t, usually the maximum value of 10 (a lower value makes the game positive-sum; see Appendix J). Concretely, the prompt I = Template Alice(P, d t) is formed, O = Alice(I) is sampled, and (CoT, Q, x) = Extractor Alice(O) is extracted. If the output is invalid it is discarded; otherwise it is evaluated with Bob to estimate its actual difficulty and a training example is formed in which the input's target difficulty is replaced by this estimate (rounded to the nearest integer): TE Alice:= (Template Alice(P, d(P, Q, Bob)), O). One or more such examples are generated from each source program P and Alice is batch-trained (e.g. via OpenAI's chat fine-tuning API, with the loss taken on the assistant message O only).

This dataset can be extended across multiple generations of Alice as long as Bob is unchanged; once Bob is updated (via rejection-sampling SFT on its own successful pairs), the difficulty of every instance must be recomputed against the stronger Bob. Since Alice initially generates examples that are too easy for Bob, especially when both share a base LLM, it was found beneficial to train Alice for many rounds, ideally to convergence, before training each new Bob.

Because Alice's early examples are mostly difficulty-zero, using all of them would swamp the training set with unhelpful instances and minimize the loss on programs not wanted Alice to generate. The set is therefore biased towards hard examples (d(P, Q, Bob) ≥ 5, i.e. fooling Bob at least half the time), adding only a fraction of the rest (20% of the hard count), sampled without replacement round-robin across difficulty bins.

The authors also explicitly train Alice to predict instance difficulty, by adding training examples in which Alice must output the difficulty of an instance it has generated; this part of the dataset is biased towards hard examples but retains 50% easy ones, since the loss is minimized only on the predicted difficulty. The exact format of these examples is given in Appendix D. The overall training procedure is summarized in Algorithm 1 (Appendix A). All templates used to interact with the LLM are in Appendix K.

The main set of experiments uses OpenAI gpt-4o-mini-2024-07-18 as the base LLM for both Alice and Bob. The training portion of MBPP is used as the source set of programs, using only the code field from each source example. Additional experiments use OpenAI gpt-4.1-nano-2025-04-14 as the base LLM.

Several precautions are taken against data contamination. As seeds, only the code field of the MBPP training split is used, never its problem statements or unit tests, and the test split is held out for evaluation. More importantly, seeds only ground the generation of new, semantically distinct variants, so memorising MBPP solutions does not by itself help an agent play the game on the resulting pairs. Finally, the headline extrinsic benchmarks are disjoint from MBPP and, for vulnerability detection, in a different language (C/C++), so those gains cannot stem from MBPP memorisation.

N = 10 responses per query are sampled at temperature 1.0 and top p = 0.7, and the generated programs are validated, normalized and executed in a sandbox under a randomized time limit; the generation and validation pipeline is detailed in Appendix H. The models are trained via SFT with difficulty targeting (always set to 10) and difficulty prediction, as described in Section 2.2, using the OpenAI fine-tuning platform, relying on the platform's default hyperparameters: 3 epochs in all cases, with batch size 4–7 and learning-rate multiplier 1.8 for gpt-4o-mini, and batch size 1–3 and multiplier 0.1 for gpt-4.1-nano. Rather than early-stopping on a validation set, Alice rounds are added until the mean instance difficulty against the fixed untrained Bob converges, then a single Bob round is run.

On gpt-4o-mini, 7 Alice rounds are run then one Bob round (fewer than ideal, due to budget limits), and on gpt-4.1-nano 6 Alice rounds, which suffice for convergence, then one Bob round. Difficulty curves are in Figure 2 (gpt-4o-mini) and Figure 4 (gpt-4.1-nano, Appendix G).

Each Alice round starts from the base LLM checkpoint rather than the previous fine-tune, while accumulating training instances across rounds. Retraining from base avoids over-representing the abundant easy instances from early rounds and prevents distribution drift from compounding across fine-tunes, which matters because the per-round sets are small and re-used. Difficulty estimates stay valid as long as Bob is unchanged; after a Bob update they must be recomputed (or the set discarded) before further Alice rounds.

The fine-tuned Bob is taken as the final model for evaluation. An open-weight Qwen3-4B-Thinking-2507 run with a LoRA adapter was also attempted, which gave unstable training curves and was not pursued to evaluation (Appendix C).

The authors first report how much Bob improves at the semantic inequivalence game itself after its single training round. Challenge instances are generated by the final Alice (round 7) from either MBPP-train source programs (as during training) or held-out MBPP-test programs, which neither agent has seen. With gpt-4o-mini, the percentage of instances solved by Bob rises from 75.99% to 86.98% on MBPP-train sources and from 88.37% to 91.67% on MBPP-test sources. The untrained Bob is already strong (Alice was not trained to convergence), yet a single Bob training round still substantially improves its ability to play the game, showing that the protocol effectively teaches LLMs to reason about the inputs on which program variants diverge.

Being proficient at playing the semantic inequivalence game may be directly useful in certain circumstances, such as determining whether a code refactoring has introduced subtle bugs. However, ultimately, the aim is for this game to teach LLMs skills that generalize to a variety of tasks. Therefore, the trained evaluator Bobs, denoted as sinq-gpt-4o-mini (based on gpt-4o-mini), and sinq-gpt-4.1-nano (based on gpt-4.1-nano) are used as the main checkpoints. Each trained model is primarily compared to its own base model. Models based on Qwen3-4B-Thinking-2507 are not evaluated, as that set of experiments yielded inconsistent training curves and was aborted.

The Python builtin identifier swap (Miceli Barone et al., 2023) is a very challenging code-understanding benchmark. In its classification version, the model must decide which of two variants of a Python snippet is more likely correct, where each snippet is prepended with a statement reassigning two builtin functions, e.g. print, len = len, print. One variant is a function from a GitHub repository; the other is the same function with the two builtin identifiers (here len and print) swapped throughout. The reassignment makes the modified snippet correct but highly out-of-distribution, and the original in-distribution but incorrect. Miceli Barone et al. (2023) found this confused all state-of-the-art LLMs of the time, which even did worse as they grew larger, a case of inverse scaling (McKenzie et al., 2023).

The authors evaluate gpt-4o-mini and gpt-4.1-nano (both released after the original study) and the trained Bobs sinq-gpt-4o-mini and sinq-gpt-4.1-nano, using either the original prompt or a chain-of-thought variant; results are in Table 1.

Despite being released years after the benchmark, without chain-of-thought both base models still perform very poorly, worse even than GPT-3.5 (3.35%), confirming that it remains challenging. The two base models then behave differently: on gpt-4o-mini the approach improves accuracy without CoT (+3.7%) and slightly with CoT (+0.4%), whereas on gpt-4.1-nano it does not help, leaving accuracy essentially unchanged without CoT (-0.3%) and lowering it with CoT (-4.3%).

The last row of Table 1 reports a superseded gpt-4.1-nano evaluator that appears to improve substantially on this benchmark (+4.6% without CoT, +0.95% with CoT). That evaluator was trained on instances validated by an earlier version of the verification harness which contained a bug: it compared program outputs by Python object identity rather than by value, and failed to reject inputs invalid for the source program, so a fraction of its training instances were not in fact diverging. The authors report it for transparency rather than as a result: the same checkpoint performs worse than the untrained model on both vulnerability-detection benchmarks (80.5% versus 83.2% on PySecDB under greedy decoding), so its apparent advantage here is not read as evidence of generalizable skill.

This benchmark is quite different from the semantic inequivalence game training data, sharing only the need to reason about the semantics of unusual Python snippets. The gpt-4o-mini improvement therefore suggests that the approach can teach code-reasoning skills that transfer to quite distant tasks, but the gpt-4.1-nano results show that this transfer is not reliable across base models, and it is not claimed as a general property of the method. Additional results on this benchmark with state-of-the-art reasoning models are reported in Appendix M.

Security vulnerabilities often arise from counterintuitive behaviours, where a programmer's (human or LLM) understanding of the code's semantics differs from its actual behaviour on edge cases that evade pre-deployment testing. The game incentivizes Alice to find exactly such edge cases and Bob to become robust to them: to win, Bob must not merely notice that a small edit exists but construct an input on which it becomes observable, which is the reasoning vulnerability detection relies on, since a vulnerable program typically differs from its patched version only on a small set of edge-case inputs. A qualitative analysis of the edits Alice actually produces is given in Appendix F. This is tested on two benchmarks.

PySecDB (Sun et al., 2023) is a dataset of Python commits, as diff patches, labelled by whether they contain a security fix. The LLMs are asked to classify each patch without the rest of the repository as context, making this challenging, and the few commits exceeding the 128,000-token context limit are discarded.

CodeXGLUE Defect Detection (Lu et al., 2021) is a dataset of C/C++ snippets labelled by whether they contain known vulnerabilities, a particularly challenging target since the models were fine-tuned only on Python.

Greedy classification (temperature 0.0), majority voting over 9 samples (temperature 1.0), and CoT (temperature 0.6, N = 1) are used; results are in Table 2. The approach yields small but consistent improvements across both datasets, tasks and languages, suggesting it confers additional vulnerability-reasoning ability despite no task-specific training.

For both the baseline and the models, chain-of-thought prompting lowers accuracy on these benchmarks relative to direct classification, and SInQ degrades slightly under CoT on some model/dataset combinations. This is attributed to the nature of the task: these benchmarks require a holistic binary judgement over an entire diff or snippet rather than the construction of a single diverging input, and free-form reasoning appears to give the model more opportunities to argue itself out of a correct initial judgement. This mirrors the identifier-swap results (Section 3.3.1), where what gains there are likewise occur without CoT, so the most consistent benefits of the method are obtained in the direct and majority-voting settings.

A standard code generation experiment is run using the EvalPlus harness (Liu et al., 2023, 2024), which evaluates LLMs on the test portions of MBPP and HumanEval (Chen et al., 2021), as well as on augmented versions of these datasets, MBPP+ and HumanEval+, which contain additional unit tests per instance; full Pass@1 rates are in Table 3 (Appendix L).

For gpt-4o-mini the approach improves Pass@1 on MBPP (+2.1%) and MBPP+ (+0.8%), matches it on HumanEval, and loses slightly on HumanEval+ (-0.6%). For gpt-4.1-nano it gives a small drop on MBPP (-1.6%) and MBPP+ (-0.3%), is roughly unchanged on HumanEval (+0.6%), and improves substantially on HumanEval+ (+3.1%).

Although trained on MBPP-train code, the models were never trained on the MBPP task itself nor shown its natural-language instructions, and they are the evaluators (Bobs), not fine-tuned for code generation, yet they still improve or maintain generation performance. For generation-oriented tasks it may help to train a separate model combining the final Alice and Bob datasets.

A neurosymbolic reading. The gains are largest on code understanding and neutral on generation, as expected since only the evaluator is trained. The design choice behind them is that the learning signal is computed symbolically rather than learned: every round is adjudicated by executing both programs on a candidate input under the operational semantics of the language, so a diverging input is a certificate of inequivalence, checkable in bounded time, with no reward model, LLM judge or human labels in the loop. SInQ therefore sits in the neurosymbolic tradition of supervising a neural learner with a symbolic verifier, and the asymmetry it exploits is itself formal: deciding full semantic equivalence is impossible in general by Rice's theorem (Appendix I), but inequivalence is semi-decidable and its witnesses are cheap to check, so the game is built on the side of the problem where symbolic verification is tractable and the neural component is delegated the search that verification cannot perform. This is also why the game has no theoretical performance cap: the verifier stays sound however strong the players become, whereas a learned reward can be gamed.

Relation to other self-play approaches. Zhao et al. (2025) also apply self-play to code with an executor for validation, but their proposer invents tasks from scratch, whereas the generator here is grounded in a corpus of real-world programs, which is regarded as the main reason the skill transfers to real security commits and to a language unseen in training. Dong and Ma (2025) apply a conjecture-and-prove variant to formal theorem proving, where the verifier is a proof assistant and the statements are formal by construction; the contribution in that comparison is to show that an ordinary interpreter can serve as the verifier for informal, real-world code. Subsequent work by Poon and Miceli Barone (2026) instead strengthens the verifier, using Liquid Haskell proofs as certificates of equivalence while keeping execution-based counterexamples for inequivalence; their ablations indicate that inequivalence supervision of the kind used here mainly contributes data volume, while the equivalence proofs account for most of the gain in reasoning ability. The strength of the symbolic verifier, rather than the self-play loop by itself, therefore looks like the most promising axis for improvement, at the price of restricting the method to languages with mature verification tooling.

The authors presented a self-play method, the semantic inequivalence game, for improving the code-understanding capabilities of LLMs, which is both grounded in a dataset of real-world programs and free of any theoretical performance cap. Evaluated on two vulnerability-detection benchmarks, it learns skills that generalize across tasks and programming languages, and on the challenging Python builtin identifier swap benchmark it substantially improves one of the two base models fine-tuned. All code and the generated synthetic data are released; exact replication, up to sampling randomness, should be possible with a modest budget (approximately 600) as long as gpt-4o-mini-2024-07-18 and gpt-4.1-nano-2025-04-14 remain available on the OpenAI platform.

The method has the following limitations, primarily due to limited budget. Model scale: only gpt-4o-mini and gpt-4.1-nano were fine-tuned, plus an unstable open-weight Qwen3-4B-Thinking-2507 run (Appendix C); larger and state-of-the-art reasoning models would strengthen the empirical claims. Training regime: supervised fine-tuning on the OpenAI platform was used, likely with LoRA-style adapters; reinforcement learning and full-parameter tuning remain to be explored. Self-play depth: due to budget, Bob was trained for a single round; multiple rounds with Alice trained to convergence between them, as in AlphaZero-style self-play, are left to future work. Baselines: no comparison against non-adversarial synthetic data (e.g. rule-based perturbations or hardness-filtered examples) is made, which would isolate the benefit of self-play. A fixed perturbation scheme is expected to plateau once its patterns are learned, whereas the game has no intrinsic performance cap (Appendix I); confirming this remains future work.

Based on the paper, here are the specific improvements I can implement in an AI system, along with what the improved system can do:

1. Add a semantic inequivalence game module to the AI's training pipeline.

• The system will include two agents: a generator (Alice) and an evaluator (Bob).

• Alice receives a real-world program (e.g., from MBPP) and produces a semantically distinct variant plus a diverging input.

• Bob receives both programs and must find a different diverging input.

• Correctness is verified by executing both programs on the candidate inputs under a randomized time limit (2.5–5.5 seconds) to prevent exploitation of fixed timeouts.

2. Implement rejection-sampling fine-tuning with difficulty targeting.

• During training, Alice is prompted to generate instances with a target difficulty (e.g., 10).

• Bob evaluates each instance multiple times (N=10) to estimate actual difficulty: d = 10 * (1 - N correct / N).

• Training examples are biased toward hard instances (d ≥ 5), keeping only 20% of easy ones, and include explicit difficulty-prediction tasks.

3. Retrain from the base model each round, accumulating training data across rounds.

• This prevents distribution drift and over-representation of early easy examples.

• Alice is trained for multiple rounds until mean difficulty converges against a fixed Bob; then Bob is trained for one round on its successful plays.

4. Use a symbolic verifier (Python interpreter) as the sole adjudicator.

• No reward model, LLM judge, or human labels are used.

• This ensures soundness and avoids gaming, and it exploits the semi-decidability of inequivalence (witnesses are cheap to check).

• Detect subtle code vulnerabilities across languages it was not trained on.

• Example: After training only on Python, the system improves vulnerability detection in C/C++ code (CodeXGLUE Defect Detection) by +0.37% to +0.51% accuracy over baseline, and on Python security commits (PySecDB) by +0.08% to +0.32%.

• Solve the extremely challenging Python builtin identifier swap benchmark.

• The system (based on gpt-4o-mini) improves accuracy from 1.65% to 5.35% without chain-of-thought, and from 1.90% to 2.30% with chain-of-thought.

• This benchmark confuses even large state-of-the-art models, so this is a meaningful gain in code-understanding capability.

• Maintain or improve code generation performance on standard benchmarks.

• On MBPP+, the system improves Pass@1 by +0.8% (gpt-4o-mini) and +3.1% on HumanEval+ (gpt-4.1-nano), while remaining roughly neutral on other generation tasks.

• Reason about edge-case inputs that cause programs to diverge.

• The system learns to identify inputs where a small edit (e.g., removing a reset statement in a maximum-subarray algorithm) changes behavior, which is exactly the reasoning needed for refactoring safety and vulnerability discovery.

• Continue improving without a theoretical performance cap.

• Because semantic inequivalence is undecidable in general (by Rice’s theorem), the game has no ceiling; the system can always be pushed to learn more complex logic, as long as resources are increased.

These improvements make the AI system a stronger, more reliable code-reasoning tool, particularly for security-critical tasks, while requiring no additional human annotation or task-specific training.

Large Language Models (LLMs) can achieve strong performance on everyday coding tasks, but they can fail on complex tasks that require non-trivial reasoning about program semantics. Finding training examples to teach LLMs to solve these tasks can be challenging. In this work, we explore a method to synthetically generate code reasoning training data based on a semantic inequivalence game (SInQ): a generator agent creates program variants that are semantically distinct, derived from a dataset of real-world programming tasks, while an evaluator agent has to identify input examples for which they behave differently. The agents train each other semi-adversarially, improving their ability to understand the underlying logic of code. We evaluated our approach on multiple code generation and understanding benchmarks, including cross-language vulnerability detection (Lu et al., 2021),, where our method improves vulnerability detection in C/C++ code despite being trained exclusively on Python code, and the challenging Python builtin identifier swap benchmark (Miceli Barone et al., 2023),, showing that whereas modern LLMs still struggle with this benchmark, our approach yields substantial improvements. We release the code needed to replicate the experiments, as well as the generated synthetic data, which can be used to fine-tune LLMs.