--- title: "Semantic Distance for Presburger Formula Generation (2026)" description: "The authors limit their study to Presburger arithmetic, which is linear integer arithmetic with addition and order but no… 5 references." authors: ["Masaya Taniguchi", "Hitomi Yanaka"] year: 2026 venue: "Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)" source: "https://aclanthology.org/2026.naloma-1.9/" licence: "CC BY 4.0 (ACL Anthology)" licence_url: "https://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/taniguchi-2026-semantic-distance-presburger-formula-generation/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/taniguchi-2026-semantic-distance-presburger-formula-generation/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2026](https://md.research.elamur.ai/free/en/papers/2026/page/42/) / Semantic Distance for Presburger Formula Generation # Semantic Distance for Presburger Formula Generation **Authors:** Masaya Taniguchi and [Hitomi Yanaka](https://md.research.elamur.ai/free/en/authors/hitomi-yanaka/) · **Year:** 2026 · **Venue:** [Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)](https://md.research.elamur.ai/free/en/venues/naloma/) ([NALOMA 2026](https://md.research.elamur.ai/free/en/venues/naloma/2026/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://aclanthology.org/2026.naloma-1.9/) · [PDF](https://aclanthology.org/2026.naloma-1.9.pdf) ## Summary String-based metrics are poor judges of formulas generated from natural language. Changing ≥ to > alters a single character, yet it can shift which numbers satisfy the formula. The authors limit their study to Presburger arithmetic, which is linear integer arithmetic with addition and order but no multiplication between variables. Their semantic distance represents a formula by the collection of whole-number grid points that make it true. Each point is weighted by a factor that shrinks exponentially with its L1 norm, so even infinite sets receive finite mass. Two formulas are then compared by a weighted Jaccard ratio: the mass of their symmetric difference divided by the mass of their union. They prove this is a true metric. They also show it is computable via quantifier elimination, a polyhedral split over orthants, and Barvinok-style lattice-point generating functions. Used as a GRPO reward, the distance yields many more parsable and semantically closer formulas than a string-similarity reward. The work is a deliberately narrow first step toward semantics-aware training signals for formal translation. ## Key points - The distance-aware reward (`distance_penalized`) raises parsability from 76.5% to 98.6% compared with a string-similarity-only reward (`similarity_only`). It also lowers semantic distance from 0.295 to 0.167. - The experiments use β = 1. The authors note that splitting space into 2^d orthants becomes costly as the number of variables d grows. - The pipeline relies on QEPCAD for quantifier elimination and LattE for lattice-point counting. Both are expensive, so scalability to larger formulas, coefficients, or nested quantifiers is still unproven. - Neither GRPO reward matches supervised fine-tuning (SFT) on exact string accuracy. The models also often drop quantifier prefixes such as (A …) and (E …). - Acknowledged gaps include: - no pure-distance GRPO ablation; - no isolation of the pretrained base model's contribution; - comparatively simple benchmark formulas; - only a single translation task. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* 📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works ## Cite Cite as: Masaya Taniguchi and Hitomi Yanaka. 2026. Semantic Distance for Presburger Formula Generation. Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA). The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @inproceedings{taniguchi2026semantic, title = {{Semantic Distance for Presburger Formula Generation}}, author = {Masaya Taniguchi and Hitomi Yanaka}, booktitle = {Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)}, year = {2026}, url = {https://aclanthology.org/2026.naloma-1.9/} } ``` - [← previous Semantic Contrastive Adaptation for Multimodal Figurative Language Understanding](https://md.research.elamur.ai/free/en/papers/siddiqui-2026-semantic-contrastive-adaptation-multimodal-figurative/) - [next → Semantic Factor Analysis: Validating Personality Structure Recovery from empirically-mediated Word Embeddings](https://md.research.elamur.ai/free/en/papers/muller-2026-semantic-factor-analysis-validating-personality/) - [↑ back to papers of 2026](https://md.research.elamur.ai/free/en/papers/2026/page/42/) ## References 5 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. Luke S. Zettlemoyer and Michael Collins. 2005. [Learning to map sentences to logical form: Structured classification with probabilistic categorial grammars](https://md.research.elamur.ai/free/en/papers/zettlemoyer-2012-learning-map-sentences-logical-form/). In Proceedings of the 21st Conference in Uncertainty in Artificial Intelligence (UAI), pages 658–666. 2. D. C. Cooper. 1972. Theorem proving in arithmetic without multiplication. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, pages 91–99. Edinburgh University Press. [find](https://scholar.google.com/scholar?q=D%2E+C%2E+Cooper%2E+1972%2E+Theorem+proving+in+arithmetic+without+multiplication%2E+In+Bernard+Meltzer+and+Donald+Michie%2C+editors%2C+Machine+Intelligence+7%2C+pages+91%E2%80%9399%2E+Edinburgh+University+Press%2E) 3. Li Dong and Mirella Lapata. 2016. [Language to logical form with neural attention](https://md.research.elamur.ai/free/en/papers/dong-2016-language-logical-form-neural-attention/). In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 33–43. 4. Jonathan Herzig, Peter Shaw, Ming-Wei Chang, Kelvin Guu, Panupong Pasupat, and Yuan Zhang. 2021. Span-based semantic parsing for compositional generalization. In Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Nat… [find](https://scholar.google.com/scholar?q=Jonathan+Herzig%2C+Peter+Shaw%2C+Ming%2DWei+Chang%2C+Kelvin+Guu%2C+Panupong+Pasupat%2C+and+Yuan+Zhang%2E+2021%2E+Span%2Dbased+semantic+parsing+for+compositional+generalization%2E+In+Proceedings+of+the+59th+Annual+Meeting) 5. Paul Jaccard. 1901. Étude comparative de la distribution florale dans une portion des alpes et du jura. Bulletin de la Société Vaudoise des Sciences Naturelles, 37(142):547–579. [find](https://scholar.google.com/scholar?q=Paul+Jaccard%2E+1901%2E+%C3%89tude+comparative+de+la+distribution+florale+dans+une+portion+des+alpes+et+du+jura%2E+Bulletin+de+la+Soci%C3%A9t%C3%A9+Vaudoise+des+Sciences+Naturelles%2C+37%28142%29%3A547%E2%80%93579%2E) *Updated 1 November 2026*