본 논문은 블랙박스 컴포넌트와 복잡한 실제 환경으로 인해 어려움을 겪는 학습 기반 사이버-물리 시스템(CPS)의 완전한 검증 문제를 해결하기 위해 ScenicProver라는 새로운 검증 프레임워크를 제시한다. ScenicProbabilistic 프로그래밍 언어를 기반으로, 해석 가능한 코드에서 블랙박스에 이르기까지 컴포넌트 간의 명확한 인터페이스를 갖춘 구성 가능한 시스템 설명을 지원한다. 또한, 임의의 Scenic 표현식을 포함하는 확장된 선형 시간 논리(LTL)를 사용하여 이러한 컴포넌트에 대한 가정-보증 계약을 지원한다. 테스트, Lean 4 통합을 통한 형식적 증명 및 외부 가정 가져오기를 통해 증거를 생성하며, 계약 연산자를 사용하여 생성된 증거를 체계적으로 결합한다. 마지막으로, 시스템 수준 보증의 출처를 추적하는 보증 사례를 자동으로 생성한다. 자율 주행 차량의 센서 융합을 통한 자동 비상 제동 시스템에 대한 사례 연구를 통해 프레임워크의 효과를 입증하였다. 레이더 및 레이저 센서에 대한 제조업체 보증을 활용하고, 불확실한 조건에 테스트 노력을 집중함으로써, 이 접근 방식은 동일한 계산 예산으로 모놀리식 테스트보다 강력한 확률적 보증을 가능하게 한다.
