나만의 모델을 증류(distill)하려면 어떻게 해야 할까?

사실 Rocq 말이야, Lean 모델은 많이 보이는데 의외로 Rocq 모델은 거의 안 보이네.

아직도 Coq 이름 바뀐 거 아쉽네. 뭐 어쨌든 다른 사람들 말이 맞음. 그래도 logit distilling은 쉬우니까 다른 사람들 스크립트 참고해서 시작하면 됨.

더 알아볼게요, 감사합니다!

정리 증명(theorem proving)을 하려면, 뭘 학습시키기 전에 정확히 어떤 유형의 실패가 발생하는지부터 기록해 봐: 잘못된 전술(tactic), 잘못된 형식화(formalization), 보조 정리(lemma) 검색 누락, 아니면 증명 상태에 대한 오해 같은 것들 말이야. 그런 것들이 평가 기준(eval buckets)이 되는 거지. 그런 구분 없이 증류(distillation)만 하면, 작은 모델이 똑같은 증명 단계에서 계속 틀리면서도 자신감 있게 말하는 법만 배우게 될 수도 있어.

그럼 Anthropic한테 밴 안 당하려면 말도 안 되는 수준의 LLM 예산이 필요할걸.

대화 데이터는 얼마나 가지고 있음? 내가 알기로는 distillation을 하려면 최소 몇 GB 단위의 학습 데이터가 필요함. 그리고 증류하려는 로컬 LLM은 어느 정도 크기로 생각함? 추론 능력이 중요하다면 최소 100B 정도는 필요할 것 같은데... (내가 틀렸길 바라지만, Qwen 27b 코딩 성능 보고 나니 작은 모델로 가능할지 회의적이네...)

Deepseek가 Lean용 정리 증명 모델을 7b로 파인튜닝해낸 걸 보면 27b~35b 정도면 충분할 것 같음. 아직 대화 데이터는 없지만, 데이터셋 생성 비용은 학술 연구비로 충당해 볼 생각임. 아직 구체적인 진전은 없고 그냥 해볼 만한 프로젝트 구상 중인 단계임.

언어 모델을 숫자에 쓴다고? 세상에, 진짜 어이가 없네.