초안, 스케치, 그리고 증명하기: 비형식적 증명을 통한 형식적 정리 증명기 안내

기존 수학적 증명의 형식화는 오랫동안 매우 어려운 과정으로 알려져 왔다. 자동화 및 증명 보조 도구에 대한 수십 년에 걸친 연구에도 불구하고, 형식화된 증명을 작성하는 일은 여전히 번거롭고 전문가들만이 접근 가능한 영역이다. 이전의 형식화 자동화 연구들은 강력한 탐색 알고리즘에 주목해 왔지만, 존재하는 비형식적 증명을 활용하려는 시도는 이루어지지 않았다. 본 연구에서는 비형식적 증명을 형식적 증명 스케치로 매핑하는 ‘드래프트, 스케치, 프루브(Draft, Sketch, and Prove, DSP)’라는 새로운 방법을 제안한다. 이 방법은 비형식적 증명을 기반으로 형식적 증명의 구조적 요약을 생성하고, 이를 통해 자동 증명기의 탐색 방향을 더 쉬운 하위 문제로 유도함으로써 증명 성능을 향상시킨다. 본 연구에서는 비형식적 증명이 인간에 의해 작성되거나 언어 모델에 의해 생성되는 두 가지 상황을 고려한다. 실험 및 아블레이션 연구 결과, 대규모 언어 모델이 비형식적 증명과 동일한 추론 단계를 따르는 잘 구조화된 형식적 스케치를 생성할 수 있음을 확인하였다. 이러한 스케치를 기반으로 자동 증명기를 안내함으로써, 수학 경시대회 문제 집합에서 증명 성능이 20.9%에서 39.3%로 향상됨을 입증하였다.