<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="nok-barone-2026-improving">
    <titleInfo>
        <title>Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Poon</namePart>
        <namePart type="given">Tsz</namePart>
        <namePart type="family">Nok</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Antonio</namePart>
        <namePart type="given">Valerio</namePart>
        <namePart type="given">Miceli</namePart>
        <namePart type="family">Barone</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-07</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Findings of the Association for Computational Linguistics: ACL 2026</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Maria</namePart>
            <namePart type="family">Liakata</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Viviane</namePart>
            <namePart type="given">P</namePart>
            <namePart type="family">Moreira</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jiajun</namePart>
            <namePart type="family">Zhang</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">David</namePart>
            <namePart type="family">Jurgens</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">San Diego, California, United States</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-395-1</identifier>
    </relatedItem>
    <abstract>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 \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.</abstract>
    <identifier type="citekey">nok-barone-2026-improving</identifier>
    <location>
        <url>https://aclanthology.org/2026.findings-acl.1615/</url>
    </location>
    <part>
        <date>2026-07</date>
        <extent unit="page">
            <start>32273</start>
            <end>32292</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
%A Nok, Poon Tsz
%A Barone, Antonio Valerio Miceli
%Y Liakata, Maria
%Y Moreira, Viviane P.
%Y Zhang, Jiajun
%Y Jurgens, David
%S Findings of the Association for Computational Linguistics: ACL 2026
%D 2026
%8 July
%I Association for Computational Linguistics
%C San Diego, California, United States
%@ 979-8-89176-395-1
%F nok-barone-2026-improving
%X 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 \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.
%U https://aclanthology.org/2026.findings-acl.1615/
%P 32273-32292

Markdown (Informal)

[Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification](https://aclanthology.org/2026.findings-acl.1615/) (Nok & Barone, Findings 2026)

• Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification (Nok & Barone, Findings 2026)

ACL

• Poon Tsz Nok and Antonio Valerio Miceli Barone. 2026. Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification. In Findings of the Association for Computational Linguistics: ACL 2026, pages 32273–32292, San Diego, California, United States. Association for Computational Linguistics.