# A Theorem-Proving-Based Evaluation of Neural Semantic Parsing

arXiv: https://arxiv.org/abs/2510.11225 · HTML: https://mlsanity.com/paper/2510.11225/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 47 references that are in the map.
- First posted on arXiv 13 Oct 2025.

## Builds on (most cited first, 16 of 16)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [COGS: A Compositional Generalization Challenge Based on Semantic Interpretation](https://mlsanity.com/paper/2010.05465/) (2020)
- [Language to Logical Form with Neural Attention](https://mlsanity.com/paper/1601.01280/) (2016)
- [Latent Predictor Networks for Code Generation](https://mlsanity.com/paper/1603.06744/) (2016)
- [Neural AMR: Sequence-to-Sequence Models for Parsing and Generation](https://mlsanity.com/paper/1704.08381/) (2017)
- [Graph Pre-training for AMR Parsing and Generation](https://mlsanity.com/paper/2203.07836/) (2022)
- [The Parallel Meaning Bank: Towards a Multilingual Corpus of Translations Annotated with Compositional Meaning Representations](https://mlsanity.com/paper/1702.03964/) (2017)
- [ReCOGS: How Incidental Details of a Logical Form Overshadow an Evaluation of Semantic Interpretation](https://mlsanity.com/paper/2303.13716/) (2023)
- [A* CCG Parsing with a Supertag and Dependency Factored Model](https://mlsanity.com/paper/1704.06936/) (2017)
- [AMR Similarity Metrics from Principles](https://mlsanity.com/paper/2001.10929/) (2020)
- [SLOG: A Structural Generalization Benchmark for Semantic Parsing](https://mlsanity.com/paper/2310.15040/) (2023)
- [SMATCH++: Standardized and Extended Evaluation of Semantic Graphs](https://mlsanity.com/paper/2305.06993/) (2023)
- [Evaluating Scoped Meaning Representations](https://mlsanity.com/paper/1802.08599/) (2018)
- [A Statistical Parsing Framework for Sentiment Classification](https://mlsanity.com/paper/1401.6330/) (2014)

## Built on by (most cited first, 1 of 1)

- [Quizzing the Translation: A Prover-Grounded Evaluation Metric for NLrightarrowFOL](https://mlsanity.com/paper/2609.33612/) (2026)

## Abstract (arXiv)

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 code and data for our experiments are publicly available.