📄 Semantic Distance for Presburger Formula Generation

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.