{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T12:04:59Z","timestamp":1784203499450,"version":"3.55.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,7]]},"abstract":"<jats:p>Large language models (LLMs) are increasingly used to control embodied agents by mapping natural-language commands to high-level actions. While this paradigm enables flexible human-robot interaction, it also introduces significant safety risks, as LLM-generated commands are not guaranteed to respect physical, environmental, or mission-critical constraints. In this paper, we present an application of reactive synthesis modulo theories to the real-time guardrailing of an LLM-controlled quadruped robot, using the first-order theory of bitvectors as a symbolic abstraction of the robot's action space and environment.\n\nOur system translates natural-language commands into discrete bitvector-encoded actions, which are then filtered by a formally synthesized guardrail (also called shield) that enforces safety and liveness properties expressed in Linear Temporal Logic modulo bitvector constraints. The shield operates online and corrects unsafe commands  while preserving the intent of the human operator. We instantiate our framework in a realistic locomotion setting, inspired by recent work on language-driven robot control, and demonstrate that the robot maintains safety under adversarial and dynamic environmental conditions.\n\nThis work illustrates how theory-aware synthesis can serve as a practical foundation for trustworthy human--robot interaction, enabling the deployment of learning-based controllers in safety-critical settings with formal guarantees.<\/jats:p>","DOI":"10.24963\/kr.2026\/104","type":"proceedings-article","created":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:15:53Z","timestamp":1784200553000},"page":"1109-1120","source":"Crossref","is-referenced-by-count":0,"title":["SafeTap: Trustworthy Neurosymbolic Language to Quadrupedal Locomotion via Shield Synthesis Modulo Bitvectors"],"prefix":"10.24963","author":[{"given":"Andoni","family":"Rodr\u00edguez","sequence":"first","affiliation":[{"name":"IMDEA Software Institute"},{"name":"Universidad Polit\u00e9cnica de Madrid"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"10584","event":{"name":"23nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2026}","theme":"Artificial Intelligence","location":"Lisbon, Portuagal","acronym":"KR-2026","number":"23","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","European Association for Artificial Intelligence"],"start":{"date-parts":[[2026,7,20]]},"end":{"date-parts":[[2026,7,18]]}},"container-title":["Proceedings of the TwentyThird International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:16:21Z","timestamp":1784200581000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2026\/104"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2026\/104","relation":{},"subject":[],"published":{"date-parts":[[2026,7]]}}}