대규모 언어 모델(Large Language Models, LLMs)은 공리적 정리 증명 분야에서 흥미로운 탐색의 길을 제시하고 있다. 그러나 이러한 모델의 활용, 특히 예시(데모) 형식과 구조화 측면에서의 전면적 활용은 여전히 탐색이 부족한 영역이다. LLM의 효과성을 향상시키기 위해, 우리는 두 가지 주요 요소로 구성된 하위목표 기반의 예시 학습 프레임워크를 제안한다. 첫째, 강화학습과 로보틱스 분야에서의 하위목표 학습( subgoal learning)에 대한 통찰을 기반으로, 각 예시 예제에 대해 독립적인 하위목표를 설정하고, 하위목표 학습의 관련 이론에 따라 이를 정교화한다. 둘째, 최근의 확산 모델(diffusion models) 기술을 활용하여 최적의 예시 구성(organization)을 예측함으로써, 예시 구성 분야에서 여전히 해결되지 않은 두 가지 복잡한 문제—부분집합 선택(subset selection)과 순서 결정(order determination)—을 동시에 해결한다. 하위목표 기반 학습 방식을 통합함으로써, 우리는 miniF2F 벤치마크에서 기존의 증명 정확도를 38.9%에서 44.3%로 성공적으로 향상시켰다. 더불어, 예시 구성에 확산 모델을 도입할 경우 정확도는 추가로 45.5%까지 상승할 수 있으며, 기존의 장기적 최고 성능 기법 대비 샘플링 효율성에서 약 5배의 개선을 달성할 수 있다. 본 연구의 코드는 다음 URL에서 공개되어 있다: \url{https://github.com/HKUNLP/subgoal-theorem-prover}.