# Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 20 of its 34 references that are in the map.
- First posted on arXiv 18 Apr 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

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

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [Dota 2 with Large Scale Deep Reinforcement Learning](https://mlsanity.com/paper/1912.06680/) (2019)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [MultiPL-E: A Scalable and Extensible Approach to Benchmarking Neural Code Generation](https://mlsanity.com/paper/2208.08227/) (2022)
- [OpenCodeInstruct: A Large-scale Instruction Tuning Dataset for Code LLMs](https://mlsanity.com/paper/2504.04030/) (2025)
- [Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation](https://mlsanity.com/paper/2502.14948/) (2025)
- [EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking](https://mlsanity.com/paper/2502.12466/) (2025)
- [SuperRL: Reinforcement Learning with Supervision to Boost Language Model Reasoning](https://mlsanity.com/paper/2506.01096/) (2025)
- [Enhancing Code Generation for Low-Resource Languages: No Silver Bullet](https://mlsanity.com/paper/2501.19085/) (2025)
- [Repetitions are not all alike: distinct mechanisms sustain repetition in language models](https://mlsanity.com/paper/2504.01100/) (2025)
- [Investigating the Performance of Language Models for Completing Code in Functional Programming Languages: a Haskell Case Study](https://mlsanity.com/paper/2403.15185/) (2024)
- [Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis](https://mlsanity.com/paper/2410.19736/) (2024)
- [Exploring Security Commits in Python](https://mlsanity.com/paper/2307.11853/) (2023)
- [Assessing Code Understanding in LLMs](https://mlsanity.com/paper/2504.00065/) (2025)
- [Program Semantic Inequivalence Game with Large Language Models](https://mlsanity.com/paper/2505.03818/) (2025)

## Abstract (arXiv)

We introduce a self-play framework for semantic equivalence in Haskell, utilizing formal verification to guide adversarial training between a generator and an evaluator. The framework leverages Liquid Haskell proofs for validating equivalence and execution-based counterexamples for inequivalence, organized via a difficulty-aware curriculum. To facilitate this, we release OpInstruct-HSx, a synthetic dataset of ≈28k validated Haskell programs. Empirical experiments show that our evaluator transfers effectively to downstream tasks, achieving up to 13.3pp accuracy gain on EquiBench and consistent gains on PySecDB. Ablation studies on the SEQ-SINQ regimes indicate that while inequivalence supervision provides data volume, equivalence proofs are uniquely responsible for the model's reasoning capabilities. The entire training pipeline and dataset are publicly released on GitHub and Hugging Face respectively.