LLM-Assisted Tool for Joint Generation of Formulas and Functions in Rule-Based Verification of Map Transformations

TL;DR

This paper introduces an LLM-assisted pipeline that automates the generation of formulas and functions for verifying map transformations in autonomous driving, reducing manual effort and enhancing scalability.

Contribution

It extends existing verification frameworks with an LLM-based approach for joint formula and predicate generation, improving efficiency and correctness.

Findings

Reduced manual engineering in map verification

Successfully integrated elevation support into the verification system

Demonstrated feasibility on synthetic map scenarios

Abstract

High-definition map transformations are essential in autonomous driving systems, enabling interoperability across tools. Ensuring their semantic correctness is challenging, since existing rule-based frameworks rely on manually written formulas and domain-specific functions, limiting scalability. In this paper, We present an LLM-assisted pipeline that jointly generates logical formulas and corresponding executable predicates within a computational FOL framework, extending the map verifier in CommonRoad scenario designer with elevation support. The pipeline leverages prompt-based LLM generation to produce grammar-compliant rules and predicates that integrate directly into the existing system. We implemented a prototype and evaluated it on synthetic bridge and slope scenarios. The results indicate reduced manual engineering effort while preserving correctness, demonstrating the feasibility of a scalable, semi-automated human-in-the-loop approach to map-transformation verification.