@inproceedings{taniguchi-yanaka-2026-semantic,
    title = "Semantic Distance for Presburger Formula Generation",
    author = "Taniguchi, Masaya  and
      Yanaka, Hitomi",
    editor = "Yanaka, Hitomi  and
      Abzianidze, Lasha",
    booktitle = "Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning ({NALOMA})",
    month = aug,
    year = "2026",
    address = "Prague, Czechia",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-naloma/2026.naloma-1.9/",
    pages = "71--79",
    ISBN = "979-8-89176-389-0",
    abstract = "We study how to evaluate and train natural-language-to-formula generation whensurface similarity is a poor proxy for semantic correctness. Focusing ontranslation into Presburger arithmetic, we introduce a geometric distancebetween formulas by viewing each formula as a set of integer lattice pointsand assigning an exponentially decaying weight to that set. The resultingdistance yields finite comparisons even for infinite definable sets, can becomputed through quantifier elimination, polyhedral decomposition, andlattice-point generating functions, and inherits the standard metric properties. Wethen use this distance in experiments on supervised fine-tuning and GRPO fortranslating arithmetic statements into formal formulas. The results show thata distance-aware reward substantially improves parsability and adjustedsemantic quality compared with a string-similarity-only reward, while alsorevealing the remaining challenge of preserving quantifier structure."
}