LLM 기반 자동 정리 증명의 혁신: BFS-Prover의 등장

Ran Xin 등 연구진이 개발한 BFS-Prover는 LLM 기반 자동 정리 증명에 BFS 알고리즘을 적용하여 기존 MCTS 방식에 비해 효율성과 확장성을 높였으며, MiniF2F 테스트 세트에서 71.31점을 기록하며 주목할 만한 성과를 거두었습니다.

최근 대규모 언어 모델(LLM)의 발전은 Lean4를 이용한 자동 정리 증명 분야에 큰 관심을 불러일으켰습니다. 효과적인 트리 탐색 기법은 방대한 증명 공간을 탐색하는 데 매우 중요한데, 기존 접근 방식은 주로 가치 함수와 몬테카를로 트리 탐색(MCTS)에 의존해 왔습니다. 하지만, Ran Xin 등 9명의 연구진은 더 간단한 최적우선탐색(BFS) 알고리즘의 가능성에 주목했습니다.

그 결과, BFS-Prover 라는 확장 가능한 전문가 반복 프레임워크를 개발하여 놀라운 결과를 얻었습니다. BFS-Prover는 세 가지 핵심 혁신을 통해 기존 방식의 한계를 극복합니다.

첫째, 전략적 데이터 필터링을 통해 각 전문가 반복 라운드에서 빔 서치 노드 확장을 통해 해결 가능한 문제를 제외하고, 더 어려운 문제에 집중합니다. 이는 컴퓨팅 자원의 효율적인 사용을 가능하게 합니다.

둘째, 컴파일러 오류 피드백으로 자동 주석이 달린 상태-전략 쌍에 직접적 선호도 최적화(DPO)를 적용하여 BFS의 샘플 효율성을 향상시켰습니다. 이는 LLM의 정책을 개선하여 생산적인 확장을 우선시함으로써 탐색의 효율을 높입니다.

셋째, BFS에서 길이 정규화를 사용하여 더 깊은 증명 경로 탐색을 장려합니다. 이를 통해 단순히 짧은 증명만 찾는 것이 아니라, 더 복잡하고 심오한 증명을 발견할 가능성을 높입니다.

결과적으로 BFS-Prover는 MiniF2F 테스트 세트에서 71.31점을 달성했습니다. 이는 복잡한 트리 탐색 방법의 필요성에 대한 기존의 인식에 도전하는 결과이며, 적절히 확장된 BFS가 경쟁력 있는 성능을 달성할 수 있음을 보여줍니다. 이 연구는 LLM 기반 자동 정리 증명 분야에 새로운 가능성을 열었을 뿐 아니라, 더욱 단순하고 효율적인 알고리즘의 잠재력을 보여주는 중요한 사례입니다. 앞으로 BFS-Prover의 발전과 다른 분야로의 응용 가능성에 대한 연구가 기대됩니다.