IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

이 논문은 안전성 증명과 반례 추적을 독립적으로 검증하는 '증명/증거 게이트' 메커니즘을 통해 LLM 이 제안한 패치를 안전하게 선별하고, 이를 통해 하드웨어 모델 체커 IC3 의 성능을 자동 진화시키는 'IC3-Evolve' 프레임워크를 제안합니다.

핵심

🏭 1. 배경: 거대한 미로와 검사관 (IC3)

우리가 만드는 반도체 칩은 수조 개의 방이 있는 거대한 미로와 같습니다. 이 미로에 '불꽃 (오류)'이 들어갈 수 있는 길이 있는지 찾아내는 것이 중요합니다.

기존에 이 일을 하는 **검사관 (IC3 알고리즘)**은 매우 똑똑하지만, 몇 가지 **직관적인 규칙 (휴리스틱)**을 적용해야 합니다.

• "어떤 방을 먼저 확인해야 할까?"
• "실수한 경로를 어떻게 빨리 차단할까?"

문제는 이 규칙들을 사람이 직접 손으로 조정하는 것이 너무 어렵다는 점입니다.

• 한 규칙을 고치면 다른 곳에서 실수가 나옵니다.
• 전문가가 수개월을 들여도 최적의 조합을 찾기 어렵습니다.

🤖 2. 해결책: AI 가 코드를 수정하는 'IC3-Evolve'

이 연구팀은 **"AI 가 코드를 수정하게 하되, 실수하면 바로 잡는 시스템"**을 만들었습니다.

🛠️ 비유: '수리공'과 '엄격한 감시관'

이 시스템은 두 명의 AI 에이전트로 나뉩니다.

1. 수리공 (프로그래머 AI):

   • 검사관의 규칙 중 **작은 부분 (슬롯)**만 건드릴 수 있습니다.
   • "이 부분을 이렇게 고치면 미로를 더 빨리 통과할 거예요!"라고 제안합니다.
   • 하지만 전체 코드를 마음대로 바꿀 수는 없습니다. (혼란을 막기 위함)

2. 엄격한 감시관 (평가자 AI):

   • 수리공이 고친 코드를 실행해 봅니다.
   • 가장 중요한 규칙: "고친 결과가 진짜로 맞는지 증명해야 한다."
     • 안전하다고 말하면 (SAFE): "이게 안전하다는 공인된 증명서를 보여줘야 해."
     • 위험하다고 말하면 (UNSAFE): "어디서 위험한지 **재현 가능한 증거 (트레이스)**를 보여줘야 해."
   • 만약 증명서나 증거가 없거나, 검증에 실패하면 즉시 폐기합니다. 성능이 좋아도 증명할 수 없으면 인정받지 못합니다.

🚀 3. 작동 방식: '나침반과 점프' 전략

AI 는 어떻게 규칙을 찾아낼까요?

• 나침반 (Compass): 현재 가장 잘 작동하는 부분을 조금씩 다듬습니다. (작은 수정)
• 점프 (Jump): 만약 막히면, 완전히 다른 부분으로 넘어가 새로운 시도를 합니다. (큰 변화)

이 과정을 반복하면서, 오직 검증된 성공 사례만 최종 검사관의 규칙으로 채택됩니다.

✨ 4. 결과: 왜 이것이 특별한가?

기존에 AI 를 검증 과정에 넣는 방식은 두 가지 문제가 있었습니다.

1. 실시간 의존성: 검증할 때마다 AI 가 돌아야 해서 속도가 느리고 비용이 듭니다.
2. 불안정성: AI 가 실수할 수 있습니다.

IC3-Evolve 의 혁신:

• 오프라인 학습: AI 는 **설계 단계 (오프라인)**에서만 코드를 고칩니다.
• 완전한 독립성: 최종 결과물은 AI 가 전혀 없는 순수한 검사관입니다.
  • 마치 **요리사 (AI)**가 레시피를 고치고, 그 레시피대로 만든 **요리 (검사 프로그램)**만 식당에 나가는 것과 같습니다.
  • 식당에 손님이 와도 요리사는 필요 없습니다. 오직 고쳐진 레시피대로 요리만 하면 됩니다.

📊 5. 성과

이 시스템을 통해 만든 검사관은:

• 기존 최고의 검사관들보다 훨씬 빠르고 정확하게 미로 (반도체 설계) 를 검사했습니다.
• 특히, 단순히 한 부분만 고치는 것보다는 여러 부분을 조화롭게 고치는 것이 훨씬 효과적임을 증명했습니다.

💡 요약

이 논문은 **"AI 가 코드를 고치는 것은 위험할 수 있지만, AI 가 고친 코드가 '엄격한 수학 증명'을 통과한 것이라면, 우리는 AI 없이도 더 뛰어난 검사관을 만들 수 있다"**는 것을 보여줍니다.

마치 **천재 요리사 (AI)**가 수백 번의 실험을 통해 최고의 레시피를 찾아내고, 그 레시피만 남긴 채 요리사 본인은 사라지는 것과 같습니다. 그 결과, 우리는 **더 빠르고 안전한 요리 (검증)**를 즐길 수 있게 됩니다.

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

• 하드웨어 모델 체킹의 중요성: 현대 하드웨어 검증에서 형식적 속성 확인 (Formal Property Checking) 은 필수적입니다. 특히 IC3(또는 Property-Directed Reachability, PDR) 는 하드웨어 안전성 모델 체킹을 위한 표준 알고리즘으로 널리 사용됩니다.
• IC3 의 한계: IC3 는 안전성 속성을 만족하면 'SAFE'(귀납적 불변식 증명) 를, 위반하면 'UNSAFE'(반례 추적) 를 반환합니다. 그러나 실제 성능은 알고리즘의 핵심 로직보다는 복잡한 휴리스틱 (heuristic) 과 구현 선택의 상호작용에 크게 의존합니다.
• 수동 튜닝의 문제점:
  • 휴리스틱 최적화는 비용이 크고 취약하며 재현하기 어렵습니다.
  • 작은 변경 사항도 광범위한 벤치마크 재실행을 요구하며, 한 인스턴스에서의 개선이 다른 곳에서 회귀 (regression) 를 유발할 수 있습니다.
  • 기존 머신러닝 기반 접근법 (NeuroPDR 등) 은 학습/추론 비용과 런타임 의존성으로 인해 산업계 배포에 한계가 있습니다.
• 핵심 과제: IC3 의 성능을 획기적으로 개선하면서도 정확성 (Soundness) 을 보장하고, 런타임에 ML 모델이 필요 없는 독립적인 검증기를 만드는 방법론이 필요합니다.

2. 제안 방법론: IC3-Evolve (Methodology)

논문은 오프라인 LLM 기반 코드 진화 프레임워크인 IC3-Evolve를 제안합니다. 이는 LLM 을 런타임이 아닌 오프라인에서 사용하여 코드를 수정하고, 엄격한 검증 절차를 통해 개선안을 채택합니다.

2.1 핵심 아키텍처

• 오프라인 LLM 활용: LLM 은 검증 (Runtime) 단계가 아닌, 코드 진화 (Evolution) 단계에서만 사용됩니다. 최종 배포되는 검증기는 LLM 이나 ML 모델에 의존하지 않는 독립형 (Standalone) 바이너리입니다.
• 슬롯 제한적 패치 (Slot-Restricted Patching):
  • IC3 의 주요 서브루틴 (Proof Obligations 처리, Inductive Generalization, Predecessor Generalization, Push/Propagation 등) 을 '슬롯 (Slot)'으로 정의합니다.
  • LLM 은 특정 슬롯 내에서만 제한된 코드 패치를 제안하도록 유도되어, 변경 사항의 범위를 통제하고 해석 가능성을 높입니다.
• Compass & Jump 검색 정책:
  • Compass: 현재 가장 유망한 단일 슬롯을 집중적으로 수정합니다.
  • Jump: 여러 슬롯 간의 시너지를 탐색하기 위해 여러 슬롯을 동시에 수정합니다.
  • 이 정책은 이전 평가 결과 (MoveSet) 를 기반으로 다음 수정 방향을 동적으로 조정합니다.

2.2 증명/증거 게이트 검증 (Proof-/Witness-Gated Validation) - 가장 중요한 특징

어떤 패치도 정확성 게이트를 통과하지 못하면 채택되지 않습니다.

• SAFE 실행 시: 생성된 귀납적 불변식 (Inductive Invariant) 을 독립적인 검증 도구 (CERTIFAIGER) 로 검증해야 합니다.
• UNSAFE 실행 시: 생성된 반례 추적 (Counterexample Trace) 을 시뮬레이터 (AIGSIM) 로 재연 (Replay) 하여 실제 오류 상태에 도달하는지 확인해야 합니다.
• 결과: 검증 실패 시 성능이 아무리 좋아도 패치는 즉시 폐기됩니다. 이는 LLM 이 제안한 잘못된 수정이 시스템에 유입되는 것을 원천 차단합니다.

2.3 2 에이전트 폐쇄 루프 (Two-Agent Closed-Loop)

1. Programmer Agent: 제한된 슬롯 내에서 패치, 가설, 백업 계획을 제안합니다.
2. Evaluator Agent: 패치를 적용하고 벤치마크를 실행하며, 증명/증거 게이트를 통과한 경우에만 성능 지표 (PAR2, 해결된 인스턴스 수 등) 를 평가합니다. 실패 시 진단 (Diagnosis) 을 통해 다음 수정 방향을 제안합니다.

3. 주요 기여 (Key Contributions)

1. IC3-Evolve 프레임워크: IC3 휴리스틱 엔지니어링을 제어된 코드 진화 문제로 변환하는 오프라인 LLM 프레임워크를 최초로 도입했습니다.
2. 엄격한 정확성 보장: 런타임 의존성 없이, Proof/Witness 게이트를 통해 모든 수정 사항의 논리적 무결성을 보장하는 프로토콜을 설계했습니다.
3. 지능적 검색 전략: Compass & Jump 전략을 통해 국소적 개선과 모듈 간 시너지를 균형 있게 탐색하는 휴리스틱 진화 워크플로우를 구현했습니다.
4. 실증적 성과: 공개 벤치마크 (HWMCC) 와 산업용 벤치마크에서 기존 최상위 모델 체커를 능가하는 성능을 입증했습니다.

4. 실험 결과 (Results)

• 벤치마크 설정:
  • 학습 (Evolution): HWMCC 공개 벤치마크 100 개 인스턴스.
  • 평가 (Evaluation): 학습에 사용되지 않은 HWMCC 100 개 + 산업용 302 개 인스턴스.
  • 기준점: IC3ref, IC3ref-CaDiCaL, ABC, rIC3 (최근 HWMCC 우승자) 등.
• 성능 비교:
  • HWMCC Set B (미확인 데이터): IC3-Evolve 는 94/100 인스턴스를 해결하여 rIC3-CaDiCaL(89/100) 보다 높은 해결률을 보였습니다.
  • PAR2 (평균 해결 시간): IC3-Evolve 는 464.56 초를 기록하여, 차기 2 위인 rIC3-CaDiCaL(524.35 초) 보다 약 11% 빠른 성능을 보였습니다.
  • 산업용 벤치마크: 302 개 인스턴스 중 225 개를 해결하여 기존 최상위 모델보다 월등히 높은 성능을 입증했습니다.
• Ablation Study (분석):
  • 게이트 없는 경우: 성능만 보고 선택하면 논리적 오류가 있는 '개선'이 채택될 수 있음을 보였습니다 (증거 게이트의 필수성 입증).
  • 단일 슬롯 vs 전체: 단일 슬롯만 수정하거나 단순히 최적의 패치를 합치는 방식 (Naive-Compose) 은 전체적인 교차 슬롯 진화 (Full IC3-Evolve) 에 비해 성능이 현저히 낮았습니다. 이는 IC3 휴리스틱이 서로 긴밀하게 결합되어 있음을 시사합니다.

5. 의의 및 결론 (Significance)

• 산업적 적용 가능성: IC3-Evolve 는 ML 모델을 런타임에 포함하지 않으므로, 지연 시간 (Latency) 이나 예측 불가능한 성능 변동을 초래하지 않습니다. 이는 산업용 EDA 도구 배포에 매우 적합합니다.
• 안전한 AI 코드 생성: 형식적 검증 (Formal Verification) 분야는 LLM 이 생성한 코드의 정확성을 수학적/논리적으로 검증할 수 있는 드문 분야입니다. 이 연구는 LLM 을 활용한 코드 진화가 '검증 가능한 게이트'를 통해 안전하고 신뢰할 수 있게 수행될 수 있음을 보여줍니다.
• 향후 전망: 고정된 슬롯을 넘어 더 넓은 편집 공간을 탐색하면서도 검증 게이트를 유지하는 방향으로 발전할 수 있으며, 이는 알고리즘 최적화를 위한 새로운 패러다임을 제시합니다.

요약하자면, IC3-Evolve 는 LLM 을 활용하여 하드웨어 모델 체커의 성능을 자동 최적화하되, 논리적 정확성을 엄격하게 검증하는 오프라인 프레임워크를 통해 기존 최상위 성능을 능가하는 독립형 검증기를 성공적으로 개발한 연구입니다.