High-definition map transformations are essential in autonomous driving systems, enabling interoperability across simulation and planning tools. Verifying the semantic correctness of these transformations is challenging, as existing rule-based frameworks rely on manually authored formulas and domain-specific function implementations, which limit scalability.

In this paper, we propose an LLM-assisted pipeline that jointly generates both logical formulas and corresponding executable functions within a computational first-order logic (FOL) framework. Our approach extends the CommonRoad verification framework by introducing elevation as a new semantic domain. The pipeline leverages prompt-based LLM generation to produce grammar-compliant rules and semantically defined predicate functions, enabling seamless integration into the existing verifier.

We implement a prototype and evaluate it on synthetic scenarios involving bridges and slopes. Results show that the proposed pipeline significantly reduces manual engineering effort while maintaining correctness, demonstrating the feasibility of a scalable, semi‑automated, human‑in‑the‑loop prototype tool for joint rule–function generation in map‑transformation verification.