기술 요약: CircuitProver

문제 정의

현대 집적 회로(IC) 설계는 증가하는 복잡도로 인해 기능 검증 단계에서 심각한 병목 현상에 직면해 있습니다. 지배적인 방법론인 **모델 체킹(model checking)**은 각 설계 인스턴스를 개별적으로 검증하며, 통과/실패 결과나 반례(counterexample)만을 노출합니다. 결과적으로, 증명의 근거는 솔버의 휴리스틱 내부에 갇히게 되며, 유사한 설계들에 대해 동일한 추론 과정을 반복해서 재구축해야 합니다. **대화형 정리 증명(ITP)**은 명시적이고 재사용 가능한 증명 산출물을 제공하지만, 하드웨어 분야에서의 적용은 공식화, 불변량 발견, 증명 구축을 위한 상당한 전문가의 노력을 요구하므로 여전히 수동적인 작업에 머물러 있습니다.

기존 도구들은 재사용 가능한 지식이 부족합니다. 모델 체킹은 추론 과정을 숨기고, 현재의 ITP 프레임워크(예: Coq, ACL2)는 인간 전문가에 과도하게 의존합니다. 자율 에이전트가 하드웨어 생성 및 최적화에 참여하는 데 도래한 "에이전트 시대"에서, 검증 도구는 단순히 정확성을 확인하는 것을 넘어 명시적인 증명 산출물과 추론 전략을 축적하고 보존하여 미래의 에이전트를 가이드할 수 있어야 합니다.

방법론: CircuitProver

본 논문은 증명 축적형 하드웨어 검증을 위해 설계된 에이전트 기반의 Lean 4 기반 검증 프레임워크인 CircuitProver를 제시합니다. 이 프레임워크는 매개변수화된 하드웨어 설계(특히 Chisel)를 대상으로 하며, 이를 통해 단일 증명이 개별 인스턴스를 각각 검증하는 대신 전체 하드웨어 제품군(family)의 정당성을 확립할 수 있게 합니다.

프레임워크는 세 가지 별도의 단계로 작동합니다:

단계 I: 하드웨어 자동 공식화 (Hardware Auto-Formalization)

CircuitProver는 매개변수화된 하드웨어 구현과 자연어 명세(specification)를 실행 가능한 Lean 4 모델로 자동 변환합니다.

• 변환: 결정론적인 Chisel-to-Lean 변환기($\mathcal{T}_{impl}$)가 하드웨어 설계를 통합된 Lean 4 의미 모델($L_D$)로 변환합니다. 이 모델은 폭(width)을 인식하는 비트 벡터 타입을 사용하여 설계 파라미터, I/O 인터페이스, 레지스터 상태 및 전이 동작을 보존합니다.
• 검증: 변환된 모델은 작은 비트 폭에서의 전수 코-시뮬레이션(co-simulation)을 통해 검증되며, 이를 통해 Lean 모델이 원래의 Chisel 설계와 동일하게 동작함을 보장합니다.
• 명세 정식화: 추론 에이전트($\mathcal{F}_{spec}$)는 하드웨어 문맥 내에서 자연어 명세($S$)를 해석하여 파라미터를 기호적으로 보존하는 공식적인 Lean 4 속성($L_S$)을 생성합니다.

단계 II: 에이전트 기반 하드웨어 정리 증명 (Agentic Hardware Theorem Proving)

하드웨어 지향 추론 에이전트는 Lean 4 정리 증명기와의 상호작作用을 통해 기계가 확인 가능한 증명을 반복적으로 구축합니다. 워크플로우는 다음과 같습니다:

1. 증명 계획 및 스캐폴드 구축: 직접적인 택틱(tactic) 탐색 대신, 에이전트는 정당성 증명을 구조화된 중간 의무(obligations)로 분해합니다.
   • 조합 논리(Combinational) 설계의 경우, 1사이클 계산의 정확성에 집중하며 산술 및 비트 벡터 로직을 위한 렘마(lemma)를 생성합니다.
   • 순차(Sequential) 설계의 경우, 로컬 1단계 전이 증명을 구축하고, 단계별 정확성과 전역적 동작을 연결하기 위한 귀납적 불변량(inductive invariants)을 발견합니다.
2. 반복적 증명: 에이전트($\mathcal{F}_{proof}$)는 증명 스크립트를 생성하고, Lean을 호출하며, 피드백(증명 상태 및 에러 메시지)을 분석합니다. 모든 의무가 해소될 때까지 Lean의 피드백을 바탕으로 추론을 정교화하거나, 렘마를 도입하거나, 불변량을 강화합니다.

단계 III: 재사용 가능한 증명 라이브러리 (Reusable Proof Library)

성공적인 증명 궤적은 향후 작업을 지원하기 위해 두 가지 상호 보완적인 라이브러리로 추출됩니다:

• 증명 가이드 라이브リ (Proof Guidance Library): 증명이 어떻게 분해되었는지, 왜 특정 렘마가 선택되었는지, 그리고 피드백에 따라 계획을 어떻게 조정했는지 설명하는 자연어 전략을 저장합니다. 이는 증명 구축을 위한 "경로(route)"를 포착합니다.
• Lean-Checked 정리 라이브러리 (Lean-Checked Theorem Library): 모듈 독립적인 기계 확인 사실을 저장합니다. 증명은 특정 모듈 정의로부터 분리되어 기호적 파라미터 및 일반화된 인터페이스 상에서 재정식화되며, 이를 통해 검증된 렘마(예: 캐리-스킵 로직)가 서로 다른 하드웨어 설계 전반에 걸쳐 재사용될 수 있습니다.

주요 기여

1. 에이전트 네이티브 하드웨어 검증: 자동 공식화, 에이전트 기반 정리 증명, 재사용 가능한 증명 라이브러리를 통합한 프레임워크인 CircuitProver를 도입했습니다.
2. 하드웨어 자동 공식화: Chisel 구현과 자연어 명세를 통합된 기계 확인 가능 Lean 4 표현으로 변환하는 파이프라인을 제공합니다.
3. 에이전트 기반 정리 증명 워크플로우: 에이전트가 피드백을 사용하여 반복적으로 증명을 구축하는 하드웨어 지향적 워크플로우를 제공하며, 특히 매개변수화된 설계와 고정 폭 세만틱스를 다룹니다.
4. 재사용 가능한 증명 라이브러리: 증명 트레이스를 자연어 전략과 공식적 산출물로 추출하여 검증 작업 간의 지식 전달을 가능하게 하는 메커니즘을 제공합니다.
5. 벤치마크 스위트: 산술, 제어, 메모리, 기타 등 다양한 범주의 63개 매개변수화된 Chisel 태스크와 프로세서 수준 모듈을 포함하여 에이전트 기반 하드웨어 정리 증명을 평가하기 위한 최초의 벤치마크 스위트입니다.

실험 결과

저자들은 CircuitProver를 바닐라 에이전트(동일한 LLM과 설정이지만 재사용 가능한 라이브러리나 하드웨어 가이드가 없는 모델) 및 Chicala/Stainless와 비교 평가했습니다.

• 성공률: CircuitProment는 벤치마크 태스크의 **100% (63/63)**를 성공적으로 증명했습니다. 바닐라 에이전트는 **92.1% (58/63)**를 해결했으며, Chicala/Stainless는 프런트엔드 견고성 문제로 인해 많은 설계를 컴파일하는 데 실패했습니다.
• 효율성: 바닐라 에이전트와 비교했을 때, CircuitProver는 다음을 감소시켰습니다:
  • 평균 증명 라운드 수 50.0%.
  • 검증 시간 23.2%.
  • 증명 코드 라인 수(LoC) 16.3%.
• 확장성: 더 큰 규모의 프로세서 수준 모듈(XiangShan 및 Rocket 곱셈기/나눗셈기)에서 CircuitProver는 바닐라 에이전트 대비 검증 시간을 56.8%, 증명 LoC를 54.4% 줄였습니다.
• 절제 연구 (Ablation Studies):
  • **정리 라이브러리(Theorem Library)**를 제거하면 성공률이 100%에서 95.2%(60/63)로 감소하여, 라이브러리가 어려운 케이스를 해결하는 데 도움이 됨을 보여주었습니다.
  • **증명 가이드(Proof Guidance)**를 제거하면 전체 커버리지를 위한 라운드 수가 18에서 29로 증가하여, 가이드가 탐색 과정을 가속화함을 보여주었습니다.
• 모델 스케일링: 성능은 LLM의 능력에 따라 확장되었습니다. 가장 강력한 모델(Opus 4.8)은 100% 성공률을 달enc한 반면, 더 약한 모델(Haiku 4.5)은 31/63개의 태스크만 해결했습니다.

의의 및 주장

본 논문은 재사용 가능한 증명 지식이 에이전트 시대의 자동화된 하드웨어 검증을 위한 핵심 동력이라고 주장합니다. 격리되고 암묵적인 검증 출력에서 축적되고 명시적인 증명 산출물로 전환함으로써, CircuitProver는 다음을 입증합니다:

1. 증명 축적은 관련 검증 작업에 대한 중복 노력을 크게 줄입니다.
2. 하드웨어 지향적 가이드는 특히 매개변수화된 설계 및 순차 설계에서 효율적인 증명 탐색을 위해 필수적입니다.
3. 에이전트 기반 정리 증명은 전통적인 모델 체킹이 재사용 가능한 추론을 제공하지 못하고 수동 ITP가 너무 노동 집약적인 다양한 하드웨어 벤치마크에서 완전한 커버리지를 달성할 수 있습니다.

저자들은 CircuitProver를 단순한 검증 도구를 넘어, 성공적인 추론 패턴을 재사용 가능한 라이브러리로 추출함으로써 시간이 지남에 따라 학습하고 개선되는 검증 도구로 향하는 단계로 위치시킵니다.