LEGO-Prover: 확장 가능한 라이브러리를 활용한 신경망 정리 증명

대규모 언어모델(LLM)의 성공에도 불구하고, 정리 증명은 여전히 해결되지 않은 가장 어려운 추론 과제 중 하나로 남아 있다. 언어모델을 활용한 기존의 방법들은 유망한 결과를 보여주었지만, 여전히 중학교 수준의 정리조차 증명하는 데 어려움을 겪고 있다. 이러한 방법들의 일반적인 한계는 정리 증명 전 과정 동안 고정된 정리 라이브러리를 가정한다는 점이다. 그러나 누구나 알고 있듯이, 새로운 유용한 정리나 심지어 새로운 이론을 창출하는 것은 수학의 발전과 더 깊고 어려운 결과를 도출하는 데 단순히 도움이 되는 것을 넘어 필수적이고 절대적으로 필요하다. 본 연구에서는, 검증된 보조정리(lemmas)를 기술(skill)로 포함하는 확장 가능한 기술 라이브러리를 활용하여 LLM의 정리 증명 능력을 강화하는 LEGO-Prover를 제안한다. LEGO-Prover는 증명을 모듈화된 방식으로 구성함으로써, LLM이 라이브러리에서 기존 기술을 검색하여 활용할 수 있을 뿐만 아니라, 증명 과정 중에 새로운 기술을 생성할 수 있도록 한다. 이러한 기술들은 이후 LLM을 활용한 프롬프팅을 통해 더욱 진화하여 라이브러리의 질적·양적 확장이 가능해진다. 재사용 가능하고 모듈화된 기술들이 지속적으로 라이브러리에 추가됨으로써 점점 더 복잡한 수학 문제에 대응할 수 있게 된다. 또한, 학습된 라이브러리는 인간이 작성한 증명과 형식적 증명 사이의 격차를 좁히는 데 기여하여 누락된 증명 단계를 보완하는 것을 더 쉽게 만든다. LEGO-Prover는 miniF2F-valid의 정상률을 기존 최고 수준인 48.0%에서 57.0%로, miniF2F-test에서는 45.5%에서 47.1%로 향상시켰다. 증명 과정 동안 LEGO-Prover는 20,000개 이상의 기술(정리/보조정리)을 생성하여 점진적으로 확장되는 라이브러리에 추가하였다. 제거 실험(ablation study) 결과, 새로 추가된 기술들이 실제로 정리 증명에 기여함을 확인하였으며, 성공률이 47.1%에서 50.4%로 개선됨을 보였다. 또한 본 연구에서는 코드와 생성된 모든 기술을 공개한다.