Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918479084388352 |
|---|---|
| author | Barone, Antonio Valerio Miceli Nok, Poon Tsz |
| author_facet | Barone, Antonio Valerio Miceli Nok, Poon Tsz |
| contents | 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 \textbf{OpInstruct-HSx}, a synthetic dataset of $\approx$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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_17010 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification Barone, Antonio Valerio Miceli Nok, Poon Tsz Computation and Language Artificial Intelligence Machine Learning Programming Languages 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 \textbf{OpInstruct-HSx}, a synthetic dataset of $\approx$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. |
| title | Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification |
| topic | Computation and Language Artificial Intelligence Machine Learning Programming Languages |
| url | https://arxiv.org/abs/2604.17010 |