<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="funakura-etal-2025-theorem">
    <titleInfo>
        <title>A Theorem-Proving-Based Evaluation of Neural Semantic Parsing</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Hayate</namePart>
        <namePart type="family">Funakura</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Hyunsoo</namePart>
        <namePart type="family">Kim</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Koji</namePart>
        <namePart type="family">Mineshima</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2025-11</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the 8th BlackboxNLP Workshop: Analyzing and Interpreting Neural Networks for NLP</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Yonatan</namePart>
            <namePart type="family">Belinkov</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Aaron</namePart>
            <namePart type="family">Mueller</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Najoung</namePart>
            <namePart type="family">Kim</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Hosein</namePart>
            <namePart type="family">Mohebbi</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Hanjie</namePart>
            <namePart type="family">Chen</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Dana</namePart>
            <namePart type="family">Arad</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Gabriele</namePart>
            <namePart type="family">Sarti</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Suzhou, China</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-346-3</identifier>
    </relatedItem>
    <abstract>Graph-matching metrics such as Smatch are the de facto standard for evaluating neural semantic parsers, yet they capture surface overlap rather than logical equivalence. We reassess evaluation by pairing graph-matching with automated theorem proving. We compare two approaches to building parsers: supervised fine-tuning (T5-Small/Base) and few-shot in-context learning (GPT-4o/4.1/5), under normalized and unnormalized targets. We evaluate outputs using graph-matching, bidirectional entailment between source and target formulas with a first-order logic theorem prover, and well-formedness. Across settings, we find that models performing well on graph-matching often fail to produce logically equivalent formulas. Normalization reduces incidental target variability, improves well-formedness, and strengthens logical adequacy. Error analysis shows performance degrades with increasing formula complexity and with coordination, prepositional phrases, and passive voice; the dominant failures involve variable binding and indexing, and predicate naming. These findings highlight limits of graph-based metrics for reasoning-oriented applications and motivate logic-sensitive evaluation and training objectives together with simplified, normalized target representations. All data and code will be publicly released.</abstract>
    <identifier type="citekey">funakura-etal-2025-theorem</identifier>
    <location>
        <url>https://aclanthology.org/2025.blackboxnlp-1.18/</url>
    </location>
    <part>
        <date>2025-11</date>
        <extent unit="page">
            <start>295</start>
            <end>306</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T A Theorem-Proving-Based Evaluation of Neural Semantic Parsing
%A Funakura, Hayate
%A Kim, Hyunsoo
%A Mineshima, Koji
%Y Belinkov, Yonatan
%Y Mueller, Aaron
%Y Kim, Najoung
%Y Mohebbi, Hosein
%Y Chen, Hanjie
%Y Arad, Dana
%Y Sarti, Gabriele
%S Proceedings of the 8th BlackboxNLP Workshop: Analyzing and Interpreting Neural Networks for NLP
%D 2025
%8 November
%I Association for Computational Linguistics
%C Suzhou, China
%@ 979-8-89176-346-3
%F funakura-etal-2025-theorem
%X Graph-matching metrics such as Smatch are the de facto standard for evaluating neural semantic parsers, yet they capture surface overlap rather than logical equivalence. We reassess evaluation by pairing graph-matching with automated theorem proving. We compare two approaches to building parsers: supervised fine-tuning (T5-Small/Base) and few-shot in-context learning (GPT-4o/4.1/5), under normalized and unnormalized targets. We evaluate outputs using graph-matching, bidirectional entailment between source and target formulas with a first-order logic theorem prover, and well-formedness. Across settings, we find that models performing well on graph-matching often fail to produce logically equivalent formulas. Normalization reduces incidental target variability, improves well-formedness, and strengthens logical adequacy. Error analysis shows performance degrades with increasing formula complexity and with coordination, prepositional phrases, and passive voice; the dominant failures involve variable binding and indexing, and predicate naming. These findings highlight limits of graph-based metrics for reasoning-oriented applications and motivate logic-sensitive evaluation and training objectives together with simplified, normalized target representations. All data and code will be publicly released.
%U https://aclanthology.org/2025.blackboxnlp-1.18/
%P 295-306

Markdown (Informal)

[A Theorem-Proving-Based Evaluation of Neural Semantic Parsing](https://aclanthology.org/2025.blackboxnlp-1.18/) (Funakura et al., BlackboxNLP 2025)

• A Theorem-Proving-Based Evaluation of Neural Semantic Parsing (Funakura et al., BlackboxNLP 2025)

ACL

• Hayate Funakura, Hyunsoo Kim, and Koji Mineshima. 2025. A Theorem-Proving-Based Evaluation of Neural Semantic Parsing. In Proceedings of the 8th BlackboxNLP Workshop: Analyzing and Interpreting Neural Networks for NLP, pages 295–306, Suzhou, China. Association for Computational Linguistics.