본 논문은 고수준 로봇 컨트롤러의 수정 과정을 가속화하기 위해 대규모 언어 모델(LLM)과 형식적 방법을 결합한 자동 프레임워크인 INPROVF를 제시한다. 기존의 형식적 방법에만 의존하는 접근 방식은 계산 비용이 많이 들고 큰 상태 공간으로 확장할 수 없다는 한계가 있다. 반면 INPROVF는 LLM을 사용하여 수정 후보를 생성하고 형식적 방법을 사용하여 그 정확성을 검증한다. 후보의 품질을 향상시키기 위해, 본 프레임워크는 먼저 환경과 컨트롤러의 기호적 표현을 자연어 설명으로 변환한다. 후보가 검증에 실패하면 INPROVF는 잠재적인 안전하지 않은 동작이나 충족되지 않은 작업에 대한 피드백을 제공하고, 반복적으로 LLM에 개선된 솔루션을 생성하도록 프롬프트한다. 다양한 작업 공간, 작업 및 상태 공간 크기를 가진 12가지 위반 사례를 통해 INPROVF의 효과를 보여준다.
