用自动定理证明评估神经语义解析，发现传统方法常误判逻辑等价性。
A Theorem-Proving-Based Evaluation of Neural Semantic Parsing
- 结合图匹配与一阶逻辑定理证明，从逻辑等价性而非表面结构评估解析结果
- 规范化目标能提升公式正确率，尤其在复杂句式中表现更优
- 适合关注逻辑推理能力的模型评估与训练，尤其在自然语言理解领域
图匹配指标如Smatch是神经语义解析的标准评估方法，但仅捕捉表面重叠而非逻辑等价性。本文通过将图匹配与自动定理证明结合，重新评估解析性能。比较了监督微调（T5-Small/Base）和少样本上下文学习（GPT-4o/4.1/5）两种方法，在归一化与非归一化目标下的表现。评估包含图匹配、源目标公式间的双向蕴含关系（使用一阶逻辑定理证明器）、以及公式合法性。结果显示，高图匹配分数的模型常无法生成逻辑等价的公式。归一化可减少目标偶然差异，提升公式合法性，并增强逻辑充分性。错误分析表明，随着公式复杂度增加，以及涉及并列结构、介词短语和被动语态时，性能下降；主要失败类型为变量绑定与索引错误、谓词命名不当。这些发现揭示了图基指标在推理类应用中的局限性，推动采用对逻辑敏感的评估与训练目标，以及简化且归一化的目标表示。所有代码与数据均已公开。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。