Article Source

• Large Language Models as Copilots for Theorem Proving

Large Language Models as Copilots for Theorem Proving

• Paper

Abstract

대정리 증명을 위한 협업 파트너로서의 대규모 언어 모델

정리 증명은 핵심적인 도전 과제

대규모 언어 모델 (LLM)에게 있어 정리 증명은 중요한 도전 과제입니다. 왜냐하면 린(Lean)과 같은 정리 증명 도구를 통해 형식적인 증명을 엄격하게 검증할 수 있기 때문에 LLM이 hallucination(환각)에 빠질 여지가 없기 때문입니다. 기존의 LLM 기반 정리 증명 도구는 사람의 개입 없이 완전히 자율적인 모드에서 정리 증명을 시도합니다. 하지만 이러한 모드에서는 사람의 통찰력이 중요할 수 있는 새롭고 어려운 정리들을 다루는데 어려움을 겪습니다.

협업 파트너로서의 LLM: 린 코파일럿 소개

이 논문에서는 LLM을 사람의 정리 증명을 돕는 협업 파트너로 활용하는 것을 연구합니다. 우리는 린(Lean)에서 신경망 추론을 실행하는 프레임워크인 ‘린 코파일럿’을 소개합니다. 린 코파일럿은 프로그래머가 린 사용자의 워크플로에 완벽하게 통합되는 다양한 LLM 기반 정리 자동화 도구를 구축할 수 있도록 해줍니다. 린 코파일럿을 사용하여 우리는 LLM을 활용하여 증명 단계를 제안하고 중간 증명 목표를 완성하는 도구를 구축했습니다. 실험 결과는 기존의 린의 규칙 기반 증명 자동화 도구에 비해 우리의 방법이 사람을 보조하는 데 효과적임을 보여줍니다.