<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="nag-sarkar-2026-decide">
    <titleInfo>
        <title>Who Should Decide Mathematical NLI? Auditing Evidence Selection, Solver Gating, and Benchmark Shortcuts</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Soumyadeep</namePart>
        <namePart type="family">Nag</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Suparnojit</namePart>
        <namePart type="family">Sarkar</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>The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Marco</namePart>
            <namePart type="family">Valentino</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Deborah</namePart>
            <namePart type="family">Ferreira</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Mokanarangan</namePart>
            <namePart type="family">Thayaparan</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Leonardo</namePart>
            <namePart type="family">Ranaldi</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jo-Ku</namePart>
            <namePart type="family">Cheng</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Andre</namePart>
            <namePart type="family">Freitas</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-468-2</identifier>
    </relatedItem>
    <abstract>Neuro-symbolic mathematical NLI combines the flexibility of language models with the exactness of formal solvers. The formal guarantee, however, applies only when selected evidence is relevant, generated constraints are faithful, and the solver actually determines the final label. We study credit assignment at this boundary.\par We audit a four-stage architecture combining knowledge-infused premise selection, Llama-3-8B-Instruct autoformalization, token-likelihood gating, and Z3 verification. Using the supplied implementation, original 500-example trace, and corrected JSON, we reconstruct the executable routing logic and evaluate selection, formalization, execution, fallback, and final-label correctness as separate stages.\par In this synthetic setting, premise selection attains 100.0% precision but 33.4% recall, while the gated and neural-only routes make identical predictions at 81.2 macro-F1 (p=1.0000). On the corrected JSON, a target-group-held-out hypothesis-only rule reaches 96.1 macro-F1, and the hypothesis string accounts for 89.7% of label entropy. These results expose two evaluation risks in this run: fallback can resemble verification, and hypothesis form can support premise-free prediction. We contribute an executable system account, a reproducible grouped shortcut diagnostic, and a trace-provenance checklist. The findings are scoped to the supplied benchmark and execution.</abstract>
    <identifier type="citekey">nag-sarkar-2026-decide</identifier>
    <location>
        <url>https://aclanthology.org/2026.mathnlp-main.23/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>305</start>
            <end>311</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Who Should Decide Mathematical NLI? Auditing Evidence Selection, Solver Gating, and Benchmark Shortcuts
%A Nag, Soumyadeep
%A Sarkar, Suparnojit
%Y Valentino, Marco
%Y Ferreira, Deborah
%Y Thayaparan, Mokanarangan
%Y Ranaldi, Leonardo
%Y Cheng, Jo-Ku
%Y Freitas, Andre
%S The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-468-2
%F nag-sarkar-2026-decide
%X Neuro-symbolic mathematical NLI combines the flexibility of language models with the exactness of formal solvers. The formal guarantee, however, applies only when selected evidence is relevant, generated constraints are faithful, and the solver actually determines the final label. We study credit assignment at this boundary.\par We audit a four-stage architecture combining knowledge-infused premise selection, Llama-3-8B-Instruct autoformalization, token-likelihood gating, and Z3 verification. Using the supplied implementation, original 500-example trace, and corrected JSON, we reconstruct the executable routing logic and evaluate selection, formalization, execution, fallback, and final-label correctness as separate stages.\par In this synthetic setting, premise selection attains 100.0% precision but 33.4% recall, while the gated and neural-only routes make identical predictions at 81.2 macro-F1 (p=1.0000). On the corrected JSON, a target-group-held-out hypothesis-only rule reaches 96.1 macro-F1, and the hypothesis string accounts for 89.7% of label entropy. These results expose two evaluation risks in this run: fallback can resemble verification, and hypothesis form can support premise-free prediction. We contribute an executable system account, a reproducible grouped shortcut diagnostic, and a trace-provenance checklist. The findings are scoped to the supplied benchmark and execution.
%U https://aclanthology.org/2026.mathnlp-main.23/
%P 305-311

Markdown (Informal)

[Who Should Decide Mathematical NLI? Auditing Evidence Selection, Solver Gating, and Benchmark Shortcuts](https://aclanthology.org/2026.mathnlp-main.23/) (Nag & Sarkar, MathNLP 2026)

• Who Should Decide Mathematical NLI? Auditing Evidence Selection, Solver Gating, and Benchmark Shortcuts (Nag & Sarkar, MathNLP 2026)

ACL

• Soumyadeep Nag and Suparnojit Sarkar. 2026. Who Should Decide Mathematical NLI? Auditing Evidence Selection, Solver Gating, and Benchmark Shortcuts. In The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026), pages 305–311, Budapest, Hungary. Association for Computational Linguistics.