자연어 설명을 기반으로 로봇 작업을 수행하는 프로그램을 생성하는 대규모 언어 모델의 문제점을 해결하기 위한 연구. 생성된 프로그램의 오류와 외부 작업 명세 위반 문제를 해결하기 위해, 프로그램을 오토마톤 기반 표현으로 변환하고 안전성 명세를 기준으로 검증하는 방법을 개발. 검증된 프로그램의 조합 역시 안전성 명세를 만족한다는 정리를 통해, 여러 프로그램의 조합을 검증할 필요 없이 계산 복잡성을 줄임. 또한, 검증 결과를 활용하여 안전한 하위 구성 요소를 생성하도록 모델을 훈련시키는 자동 미세 조정 절차를 도입하여 훈련 효율성을 향상시킴. 로봇 응용 프로그램에서 명세 준수 프로그램 생성 확률 30% 증가, 훈련 시간 절반 감소의 결과를 보임.