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

하드웨어 모델 검사(Hardware Model Checking) 분야에서 IC3 알고리즘은 뛰어난 성능과 확장성으로 현존하는 최고 수준(SOTA) 기법으로 자리매김하고 있습니다. 연구의 초점은 주로 이 IC3 알고리즘의 해결 효율성을 높이는 데 맞춰져 왔으며, 그중에서도 '귀납적 일반화 (inductive generalization)' 과정이 핵심적인 역할을 수행합니다.

IC3에서 귀납적 일반화란, 일반적으로 나쁜 상태(bad state)로 이어지는 카운터예제(counterexample)를 더 광범위한 상태 집합으로 확장하여 추론하는 과정을 의미합니다. 이 과정에서 생성되는 명제들(clauses)은 IC3의 전체적인 효과성을 결정짓는 주요 원천입니다.

하지만 기존 연구들은 이러한 귀납적 일반화 전략을 고정된 방식에 의존하는 경향이 있어, 실제 검증 환경에서 발생하는 임시 카운터예제(spurious counterexamples)가 요구하는 동적이고 문맥 민감적인 특성을 반영하지 못했습니다. 이러한 경직성은 생성되는 명제의 품질을 제한하고 결과적으로 IC3의 성능 저하를 초래합니다.

본 논문은 이러한 한계를 극복하기 위해, 검증 환경의 변화에 대응하여 적절한 귀납적 일반화 전략을 동적으로 선택하는 경량 머신러닝 기반 프레임워크인 A-IC3를 제안합니다. 구체적으로는 다중 팔 밴딧 (Multi-Armed Bandit, MAB) 알고리즘을 활용하여 검증 과정에서 얻는 실시간 피드백(real-time feedback)에 기반해 일반화 전략을 적응적으로 선택합니다. 이 에이전트는 일반화 결과의 품질을 평가함으로써 지속적으로 자신의 전략 선택 방식을 개선해 나갑니다.

실험 결과, 914개의 인스턴스로 구성된 벤치마크 스위트(HWMCC 컬렉션 기반)에서 A-IC3의 효과가 입증되었습니다. 최신 모델 검사기 rIC3에 구현했을 때, 제안 방법은 베이스라인 대비 26개에서 50개 이상의 케이스를 추가로 해결했으며, PAR-2 점수를 194.72점에서 최대 389.29점까지 향상시키는 놀라운 성능을 보여주었습니다.