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

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · Rutgers University New Brunswick (NJ) · $899,109

## Abstract

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 symbo

## Key facts

- **NSF award ID:** 2525293
- **Awardee organization:** Rutgers University New Brunswick (NJ)
- **SAM.gov UEI:** M1LVPE5GLSD9
- **PI:** He Zhu
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** FMitF-Formal Methods in the Field
- **Estimated total:** $899,109
- **Funds obligated:** $899,109
- **Transaction type:** Standard Grant
- **Period:** 09/01/2025 → 08/31/2028

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2525293

## Citation

> US National Science Foundation, Award 2525293, FMitF: Track I: Abstraction Refinement-guided Program Synthesis for Verifiable Robot Learning. Retrieved via AI Analytics 2026-06-06 from https://api.ai-analytics.org/grant/nsf/2525293. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*