<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="zouak-etal-2026-counterexample">
    <titleInfo>
        <title>Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Omar</namePart>
        <namePart type="given">Farouk</namePart>
        <namePart type="family">Zouak</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Houssam</namePart>
        <namePart type="given">Eddine</namePart>
        <namePart type="family">Boukhalfa</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Lakehal</namePart>
        <namePart type="family">Soumaya</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Shiv</namePart>
        <namePart type="family">Katiyar</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Prof</namePart>
        <namePart type="given">Samia</namePart>
        <namePart type="family">Nefti-Meziani</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-10</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Hung-Yi</namePart>
            <namePart type="family">Lee</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Sunipa</namePart>
            <namePart type="family">Dev</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jessy</namePart>
            <namePart type="family">Li</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Desmond</namePart>
            <namePart type="family">Elliott</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Budapest, Hungary</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-462-0</identifier>
    </relatedItem>
    <abstract>Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.</abstract>
    <identifier type="citekey">zouak-etal-2026-counterexample</identifier>
    <location>
        <url>https://aclanthology.org/2026.findings-emnlp.2112/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>45032</start>
            <end>45047</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
%A Zouak, Omar Farouk
%A Boukhalfa, Houssam Eddine
%A Soumaya, Lakehal
%A Katiyar, Shiv
%A Nefti-Meziani, Prof Samia
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F zouak-etal-2026-counterexample
%X Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.
%U https://aclanthology.org/2026.findings-emnlp.2112/
%P 45032-45047

Markdown (Informal)

[Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs](https://aclanthology.org/2026.findings-emnlp.2112/) (Zouak et al., Findings 2026)

• Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs (Zouak et al., Findings 2026)

ACL

• Omar Farouk Zouak, Houssam Eddine Boukhalfa, Lakehal Soumaya, Shiv Katiyar, and Prof Samia Nefti-Meziani. 2026. Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs. In Findings of the Association for Computational Linguistics: EMNLP 2026, pages 45032–45047, Budapest, Hungary. Association for Computational Linguistics.