LLM 기반 에이전트 프레임워크를 사용하여 자율 응용 프로그램의 안전성을 보장하는 데 필수적인 동적 시스템의 안전성 검증을 위한 장벽 인증서를 합성합니다. 이 프레임워크는 자연어 추론을 사용하여 후보 인증서를 제안, 개선 및 검증하고, LLM 기반 템플릿 검색과 SMT 기반 검증을 통합하며, 안전 인증서와 컨트롤러 간의 일관성을 보장하기 위해 장벽-컨트롤러 공동 합성을 지원합니다. BarrierBench 벤치마크를 통해 프레임워크의 효과를 평가하고, 검색 증강 생성 및 에이전트 조정 전략의 유용성을 평가합니다.