본 논문은 대규모 언어 모델(LLM)이 Lean과 같은 증명 보조기를 사용하여 형식 정리를 증명하는 데 유망함을 보이지만, 최신 LLM이 증명의 다음 단계를 예측하는 데 어려움을 겪고, 실무자들이 LLM의 기능을 향상시키기 위해 다양한 샘플링 기법을 사용하는 현실을 다룹니다. LLM이 올바른 전략을 예측할 수 있지만, 후보 전략 집합 내에서 적절하게 순위를 매기는 데 어려움을 겪어 전반적인 선택 과정에 영향을 미치는 것을 관찰했습니다. 이러한 문제를 해결하기 위해, 활성화 조향(activation steering)을 사용하여 추론 시 LLM의 응답을 안내하여 생성을 개선합니다. 연구 결과는 활성화 조향이 특히 자원이 제한된 환경에서 LLM의 정리 증명 기능을 향상시키기 위한 특수 미세 조정에 대한 경량의 유망한 대안을 제공함을 시사합니다.
