FMitF: Track I: Abstraction Refinement-guided Program Synthesis for Verifiable Robot Learning

This project advances science at the intersection of robotics, artificial intelligence, and formal verification to enable reliable and transparent robot behavior in real-world settings. As robots increasingly assist with complex tasks—from warehouse logistics to supporting independent living—ensuring their safe and trustworthy operation is essential. However, state-of-the-art robot learning methods, such as deep reinforcement learning, rely heavily on opaque neural network controllers that are difficult to interpret, verify, and generalize, limiting their use in safety-critical domains. This research addresses these challenges by developing a new class of interpretable control programs, written in domain-specific languages with automatically-inferred domain knowledge. These programs enable robots to reason over long-term goals, adapt to novel environments, and be certified as safe before deployment. Through this approach, the project aims to improve both the efficiency and reliability of real-world robotic systems. The main contributions of this project are new algorithms for the synthesis and verification of robot-control programs, grounded in formal methods, to support transparent and trustworthy robot learning. The proposed approach synthesizes high-level symbolic programs from low-level reward functions or task specifications in continuous, high-dimensional environments. At its core is abstraction refinement, which automatically generates and iteratively improves symbolic representations of environment states and robot capabilities. These abstractions guide the synthesis of recursive, compositional control programs that generalize to long-horizon and multi-object tasks. Verification is achieved through compositional reasoning, enabling the correctness of a control program to be inferred from modular analyses of its components. This significantly reduces the computational burden of verification in complex environments. The research will be validated on real-world robotic platforms, such as packing and assembly tasks in warehouses, manufacturing, and supply-chain settings, to evaluate the efficiency, scalability, and generality of the proposed synthesis and verification techniques. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.