Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
On the map: LLM reasoning → Reasoning benchmarks and evaluation
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.
Key facts. No citing papers in the map yet (data through 7 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.
Builds on
20 of 34 references.
References · 20
- 2022Training language models to follow instructions with human feedbackcited by 15,712
- 2024Qwen2.5-Coder Technical Reportcited by 1,151
- 2019Dota 2 with Large Scale Deep Reinforcement Learningcited by 1,084
- 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
- 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
- 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
- 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
- 2022MultiPL-E: A Scalable and Extensible Approach to Benchmarking Neural Code Generationcited by 132
- 2025OpenCodeInstruct: A Large-scale Instruction Tuning Dataset for Code LLMscited by 57
- 2025Learning to Solve and Verify: A Self-Play Framework for Code and Test Generationcited by 34
- 2025EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checkingcited by 23
8 more
- 2025SuperRL: Reinforcement Learning with Supervision to Boost Language Model Reasoningcited by 18
- 2025Enhancing Code Generation for Low-Resource Languages: No Silver Bulletcited by 9
- 2025Repetitions are not all alike: distinct mechanisms sustain repetition in language modelscited by 9
- 2024Investigating the Performance of Language Models for Completing Code in Functional Programming Languages: a Haskell Case Studycited by 7
- 2024Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesiscited by 7
- 2023Exploring Security Commits in Pythoncited by 5
- 2025Assessing Code Understanding in LLMscited by 2
- 2025Program Semantic Inequivalence Game with Large Language Modelscited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
- 2026The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis
- 2025Disproving Program Equivalence with LLMs
- 2026VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
- 2025Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
- 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
- 2025Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning
- 2026A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation