🤖 machine learning

Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation

본 논문은 토큰 수준의 모방보다 의미적 정확성을 우선시함으로써 새로운 최첨단 성능을 달성하는 7B 학생 모델을 SystemVerilog 어설션 생성을 위해 유도하는 공식적 속성-동치 검증기를 활용하는 새로운 훈련 방법인 보상 가중 온-정책 증류 (RWOPD) 를 소개합니다.

원저자: Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

게시일 2026-05-14

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

재능은 있지만 경험이 부족한 견습생(70 억 파라미터 AI)에게 컴퓨터 칩을 위한 복잡한 법적 계약을 작성하는 법을 가르친다고 상상해 보세요. 이러한 계약은 **시스템버ilog 어설션 (SVA)**이라고 불립니다. 이는 칩에게 "이 사건이 발생하면 3 초 이내에 반드시 저 사건이 발생해야 한다"거나 "이 신호는 절대 높게 유지되어서는 안 된다"는 규칙을 전달합니다.

오랫동안 전문가들은 최고의 AI 모델이 이미 이 작업을 마스터하여 약 76% 의 정확도에 도달했다고 생각했습니다. 하지만 이 논문의 저자들은 숨겨진 결함을 발견했습니다. AI 는 규칙을 아는 것처럼 말하기는 잘했지만, 실제로는 몇 가지 간단한 문장 구조를 암기하고 있었을 뿐이었습니다. 복잡한 타이밍 규칙에 직면하면, 겉보기에는 맞지만 법적으로 틀린 기본적이고 일반적인 템플릿으로 "무너져 내리는" 현상이 발생했습니다.

이 논문은 다음과 같은 간단한 비유를 사용하여 이 문제를 해결합니다:

1. 문제: 모방 대 이해

이러한 AI 를 훈련시키던 기존 방식은 학생이 교사의 숙제를 단어 그대로 베끼는 것과 같았습니다. 학생은 교사의 답변과 철자 및 문법이 얼마나 일치하는지에 따라 점수를 받았습니다.

결함: 이 분야에서는 두 문장이 완전히 다르게 보일지라도 정확히 같은 의미 (동치) 일 수 있습니다. 반대로 두 문장이 거의 동일하게 보일지라도 정반대의 의미를 가질 수도 있습니다. 기존 방식은 학생이 논리를 이해한 것이 아니라 단어를 베낀 것에 대해 점수를 주었습니다.

2. 해결책: "보상 가중 온-정책 증류 (Reward-Weighted On-Policy Distillation, RWOPD)"

저자들은 RWOPD라는 새로운 훈련 방법을 고안했습니다. 이는 학생, 마스터 교사, 그리고 엄격한 심판이 관여하는 3 단계 코칭 과정으로 생각할 수 있습니다.

단계 A: 학생이 연습합니다 (On-Policy)

교사를 단순히 베끼는 대신, 학생 AI 는 프롬프트를 기반으로 자체 계약 (롤아웃이라고 함) 을 작성하도록 요청받습니다. 먼저 스스로 문제를 해결해 보려고 노력합니다.

단계 B: 엄격한 심판 (오픈 속성 동치 검사기)

이것이 이 논문의 핵심 비법입니다. 저자들은 문법만 확인하는 것이 아니라 논리를 확인하는 오픈 소스 "심판" (SymbiYosys 와 Z3 라는 도구를 사용) 을 구축했습니다.

비유: 심판이 학생의 계약과 참조 계약을 가져와 시뮬레이션을 실행하는 변호사라고 상상해 보세요.
판결: 심판은 이렇게 묻습니다. "이 두 계약은 법적으로 동치입니까?"
- 학생의 계약이 참조와 논리적으로 동치라면 심판은 **"합격"**이라고 말합니다.
- 약간 더 엄격하거나 관대하다면 심판은 **"부분 합격"**을 줍니다.
- 틀리면 심판은 **"불합격"**이라고 말합니다.
중요한 점: 심판은 논리적으로 틀린 학생의 답변은 무시합니다. 심판은 필터 역할을 하여 "좋은" 시도만 다음 단계로 진행시킵니다.

단계 C: 마스터 교사 (증류)

여기서 마법이 일어납니다. 학생은 심판의 "합격/불합격" 점수만으로 배우지 않습니다.

마스터 교사 (이미 매우 뛰어난 140 억 파라미터 AI) 는 학생의 성공적인 시도들을 살펴봅니다.
교사는 말합니다. "좋아, 논리는 맞았어. 이제 내가 그 특정 단어들을 어떻게 작성했을지 정확히 봐. 내가 선택했을 각 단어의 확률을 보여줄게."
그런 다음 학생은 심판이 승인한 시도들에 대해서만 교사의 스타일에 맞춰 뇌를 업데이트합니다.

왜 이것이 더 나은가요?

기존 방식: 학생은 나쁜 시도조차 포함해 모든 시도에서 배우며 올바른 단어를 추측하려 했습니다.
새로운 방식 (RWOPD): 학생은 "승리"한 시도들로부터만 배우며, 마스터가 그 승리한 답변들을 어떻게 표현했는지에 대한 깊은 논리를 배웁니다. 마치 학생이 상을 받은 에세이들만 공부하되, 노벨상 수상자가 왜 그 에세이들이 좋았는지에 대한 해설을 통해 배우는 것과 같습니다.

3. 결과: 거인들을 이기다

저자들은 이 방법을 70 억 파라미터 모델 (학생) 에 대해 테스트했습니다.

경쟁: 이전 최고의 전문 모델 (140 억 파라미터 AI) 과 심지어 거대한 범용 모델 (6,710 억 파라미터) 과 비교했습니다.
결과: 이 새로운 코칭 방법을 사용한 작은 70 억 파라미터 학생이 모두를 이겼습니다. 벤치마크에서 가장 높은 정확도를 달성하여 100 배 더 큰 모델들을 능가했습니다.
수정된 "숨겨진 격차": 이 논문은 학생이 특히 이전 모델들이 실패했던 시간과 지연을 포함하는 가장 어려운 유형의 규칙에 대해 훨씬 더 나아졌음을 보여줍니다.

요약

이 논문은 AI 에게 복잡한 논리를 가르치려면 단순히 답을 암기하게 해서는 안 된다고 주장합니다. 대신 다음과 같이 해야 합니다:

문제를 해결해 보게 하세요.
엄격한 논리 검사기를 사용하여 잘못된 답변을 필터링하세요.
마스터 교사가 올바른 답변을 어떻게 표현해야 하는지 학생에게 정확히 보여주세요.

논리 검사기와 마스터 교사를 결합함으로써, 작은 AI 는 거인처럼 생각하도록 배워, 이전에는 거의 "포화 상태" (해결됨) 로 여겨졌던 문제를 해결할 수 있습니다.

기술 요약: NL-to-SVA 생성을 위한 보상 가중 온-폴리시 증류

문제 제기
대규모 언어 모델 (LLM) 을 사용하여 자연어 (NL) 명세에서 시스템버릴로그 어설션 (SVA) 을 생성하는 작업은 성능 정체기에 도달했으며, 가장 강력한 전문 모델 (예: CodeV-SVA-14B) 은 NL2SVA-Human 벤치마크에서 약 76% 의 정확도를 달성했습니다. 그러나 이 집계 점수는 중요한 "시간적 격차"를 가리고 있습니다. 모델은 결합 (C1) 로직에서는 잘 수행되지만, 유한 지연 (C2) 및 활성 (C3) 명세에서는 자주 실패합니다. 지배적인 실패 양상은 "템플릿 붕괴"로, 모델은 명세의 구체적인 시간적 요구사항과 관계없이 소수의 함의 템플릿 (예: |->) 으로 default 됩니다.

확인된 근본 원인은 훈련 목적 함수입니다. 기존 시스템은 단일 참조 어설션의 토큰 수준 모방을 최적화하는 NL/SVA 쌍에 대한 지도 미세 조정 (SFT) 에 의존합니다. 이 접근법은 두 어설션이 구문적으로 멀지만 의미적으로 동등하거나, 구문적으로 유사하지만 의미적으로 대립할 수 있는 SVA 정확도의 의미론적 본질을 포착하지 못합니다. 또한, 검증자 피드백을 통한 표준 강화 학습 (RL) 은 이 설정에서 효과가 입증되지 않았습니다. 희소한 롤아웃 수준의 보상은 제한된 적응 예산 (LoRA) 을 가진 소규모 파라미터 모델 (7B) 에게 충분한 신호를 제공하지 못해, 종종 SFT 기준선을 넘지 못합니다.

방법론: 보상 가중 온-폴리시 증류 (RWOPD)
본 논문은 학생 모델을 속성 동등 행동으로 유도하기 위해 증류 과정에 형식 검증기를 통합한 **보상 가중 온-폴리시 증류 (RWOPD)**를 제안합니다. 파이프라인은 네 가지 주요 구성 요소로 이루어집니다:

계층적 커리큘럼 SFT: 증류 전에 7B 학생 모델 (Qwen2.5-Coder-7B-Instruct) 은 커리큘럼 기반 SFT 를 거칩니다. 이 단계는 재현 버퍼를 사용하여 치명적 망각을 방지하면서 세 단계 (C1, C2, C3) 로 훈련하여 더 쉬운 시간적 클래스에 대한 편향을 해결합니다. 결정적으로, 이 단계는 모델이 이러한 토큰의 구조적 중요성을 학습하도록 보장하기 위해 시간 연산자 토큰 (예: |->, s_eventually) 을 가중치 상승시키는 연산자 토큰 가중 교차 엔트로피 손실을 사용합니다.
개방형 속성 동등성 체커 (PEC): 훈련 중 Cadence JasperGold 와 같은 산업용 도구의 비용과 폐쇄 소스 성격을 피하기 위해, 저자들은 SymbiYosys 와 Z3를 기반으로 구축된 오픈 소스 검증기를 도입합니다. 이 체커는 C1 및 C2 조각에 대해 유한 모델 체킹 (BMC) 을 수행합니다. 출력 판정으로는 EQUIVALENT, IMPLIES_REF_TO_LM, IMPLIES_LM_TO_REF, NOT_EQUIVALENT, 또는 BMC 외부의 활성 사례에 대한 UNSUPPORTED 등이 있습니다. PEC 는 정합적입니다: 생성된 모든 EQUIVALENT 판정은 정확성이 보장되지만, 복잡한 활성 속성에서는 기권할 수 있습니다.
RWOPD 훈련 루프:
- 학생은 주어진 프롬프트에 대해 $K$ 개의 롤아웃을 샘플링합니다.
- 개방형 PEC 는 이러한 롤아웃을 필터링하여 구문적으로 깨지거나 의미적으로 부정확한 (NOT_EQUIVALENT) 것들을 폐기합니다.
- 남은 롤아웃은 PEC 판정에 기반한 보상 가중치를 할당받습니다 (예: EQUIVALENT 의 경우 1.0, 일방향 함의의 경우 0.6/0.4).
- 고정된 14B 교사 모델 (CodeV-SVA-14B) 은 보존된 롤아웃에 대해 밀집된 포워드-KL (Kullback-Leibler) 발산 목표를 제공합니다.
- 학생은 이러한 KL 손실의 보상 가중 평균을 사용하여 업데이트됩니다. 이는 감독이 토큰 수준에서 밀집되어 있으면서도 속성 동등 행동에 기반하도록 보장합니다.
평가 프로토콜: 훈련은 필터링 및 보상 형성을 위해 개방형 PEC 에 의존하지만, 최종 평가는 완전성과 이전 벤치마크와의 일관성을 보장하기 위해 산업 등급인 Cadence JasperGold prop_eq_checker 를 사용합니다.

주요 기여

RWOPD 알고리즘: 속성 동등성 체커를 사용하여 교사의 밀집된 감독을 제한하고 보상 가중치를 부여하는 새로운 증류 방법입니다. 이는 증류의 밀집된 토큰 수준 신호와 형식 검증의 의미론적 기반을 결합합니다.
개방형 SymbiYosys+Z3 PEC: SVA 의 유한 모델 체킹 조각에 대한 라이선스 없는 정합 검증기입니다. 이는 이전 작업에서 사용된 폐쇄 소스 오라클과 구별되는 훈련 시간 필터링을 위한 재현 가능하고 초 단위의 검증 신호를 제공합니다.
실증적 최첨단 성능: 이 방법은 NL2SVA-Human 및 NL2SVA-Machine 벤치마크에서 새로운 기록을 수립했습니다.

결과
저자들은 LoRA(학습 가능 파라미터 0.53%) 를 적용한 7B 학생 모델을 전문 14B 모델 및 671B 범용 기준선과 비교 평가했습니다.

성능: RWOPD 는 두 벤치마크에서 가장 높은 pass@1, pass@5, pass@10 점수를 달성했습니다. NL2SVA-Machine 에서 전문 이전 최첨단 (CodeV-SVA-14B) 을 pass@1 기준 2~~4 퍼센트 포인트 (pp) 더 높았고, 671B 모델 (DeepSeek-R1, GPT-5) 보다 4~~7 pp 더 높았습니다.
시간적 분해: 성장은 시간적으로 비자명한 슬라이스에 집중되었습니다. RWOPD 는 14B 교사 대비 C2(유한 지연) 를 7.5 pp, C3(활성) 을 11.5 pp 개선했으며, C1 성능은 포화 상태였습니다.
절차적 연구:
- 증류 vs. RL: 동일한 PEC 신호를 사용하는 희소 보상 최적화 (GRPO, IPO) 는 SFT 기준선을 초과하지 못해 밀집된 교사 KL 이 성능의 주요 동인임을 확인했습니다.
- 필터 vs. 교사: 교사 없이 롤아웃을 필터링하는 거부 샘플링 SFT 는 미미한 개선 (~2.5 pp) 만 제공하여 밀집된 교사 감독이 지배적인 가치 추가 요소임을 분리해냈습니다.
- 필터 정밀도: RWOPD( EQUIVALENT 와 일방향 함의 모두 사용) 는 엄격한 EQUIVALENT 전용 필터링보다 성능이 우수하여, 기울기 가용성과 의미론적 정확성 사이의 균형을 맞췄습니다.

의의 및 주장
본 논문은 7B 모델과 LoRA 적응이라는 특정 영역에서 검증기는 RL 을 위한 독립적인 보상 신호로서가 아니라 밀집된 교사 감독을 위한 보상 형식 필터로서 가장 효과적이라고 주장합니다. 저자들은 NL-to-SVA 생성의 "숨겨진 시간적 격차"가 데이터 부족이나 모델 크기 때문이 아니라 훈련 목적 함수의 불일치 (토큰 모방 vs. 속성 동등성) 에 기인한다고 논증합니다. 밀집된 증류 신호를 형식 속성 동등성에 기반하게 함으로써, RWOPD 는 작고 효율적인 모델이 의미론적으로 정확한 하드웨어 어설션을 생성하는 데 있어 더 큰 전문 모델과 거대한 범용 LLM 보다도 더 뛰어난 성과를 내도록 합니다.

이 연구는 "영역 진술"로 제시됩니다: 7B+LoRA 규모에서 정합적인 개방형 검증자와 온-폴리시 증류를 통한 강력한 교사의 결합은 희소 강화 학습보다 검증 신호를 더 효과적으로 활용하는 방법입니다. 저자들은 C3 학습을 위한 간접 메커니즘 (직접 검증기 피드백 대신 커리큘럼 시드에 의존) 과 활성 속성에 대한 개방형 PEC 의 불완전성으로 인한 최종 평가를 위한 JasperGold 의존성 등 한계를 인정합니다.