A-IC3: 하드웨어 모델 검증을 위한 적응형 귀납적 일반화 학습

요약

본 논문은 최신 하드웨어 모델 검증 기법인 IC3의 성능 향상을 목표로 합니다. 특히, 카운터예제(counterexample)를 더 넓은 상태 집합으로 일반화하는 '귀납적 일반화 (inductive generalization)' 과정에 초점을 맞춥니다. 기존 방식들이 고정된 전략을 사용해 검증 환경 변화에 취약했던 문제를 해결하기 위해, 본 연구는 다중 팔 밴딧 (Multi-Armed Bandit, MAB) 알고리즘 기반의 경량 머신러닝 프레임워크를 제안합니다. 이 프레임워크는 실시간 피드백을 바탕으로 최적의 일반화 전략을 동적으로

핵심 포인트

• 다중 팔 밴딧 (MAB) 알고리즘을 활용하여 검증 과정의 변화에 맞춰 귀납적 일반화 전략을 적응적으로 선택합니다.
• 제안된 A-IC3 방법은 기존 SOTA 모델 검사기 rIC3에 적용되었으며, 베이스라인 대비 26~50개 이상의 케이스를 추가로 해결했습니다.
• PAR-2 점수를 194.72점에서 최대 389.29점까지 향상시키는 성능을 입증했습니다.