연구진은 대규모 언어 모델(LLM)을 활용한 형식적 정리 증명 분야에서 자기 학습 알고리즘의 자기 개선 능력을 이해하기 위한 이론적 프레임워크를 제시했어요.
정리 집합을 의미적으로 유사한 정리 쌍 간의 연결을 가진 그래프로 형식화하고, 자기 학습 알고리즘의 보장과 쟁점을 생성하는 알고리즘이 그래프 구조에 접근하는 방식을 특징짓는 기본 가정을 도입했어요.
이론적 프레임워크에 따르면, 정리 그래프가 잘 연결되어 있다면 가역적 무작위 워크 기반 쟁점 생성 알고리즘을 사용하는 증명자-쟁점 생성자 시스템은 증명된 정리 집합을 지수적으로 확장하는 데 충분해요.
쟁점 생성자가 인위적으로 복잡하고 근본적이지 않은 정리를 생성하는 경향이 있는 경험적 문제를 해결하기 위해, 쟁점 생성자가 생성하는 훈련 분포의 다양성을 측정하고 이 다양성 측정값을 지역적으로 최대화하는 개선된 쟁점 생성 알고리즘을 제안했어요.