라이라: 자동 정리 증명에서 이중 보정을 조율하기

대규모 언어 모델(Large Language Models, LLMs)은 형식적 정리 증명 분야에서 탐구할 만한 매력적인 방향성을 제시하고 있다. 그러나 특히 환각(hallucination) 완화 및 증명기(prover) 오류 메시지를 통한 정교화 측면에서 LLMs의 잠재력을 충분히 탐구하지 못한 상태이다. 이를 개선하기 위해, 우리는 두 가지 독립적인 보정 메커니즘—도구 보정(Tool Correction, TC)과 추측 보정(Conjecture Correction, CC)—을 도입한 새로운 프레임워크인 Lyra를 제안한다. 형식적 증명의 후처리 과정에서 도구 보정을 구현하기 위해, 사전 지식을 활용하여 미리 정의된 증명기 도구(예: Sledgehammer)를 사용하여 잘못된 도구를 대체하도록 유도한다. 도구 보정은 환각 현상을 효과적으로 완화함으로써 증명의 전반적인 정확도를 크게 향상시킨다. 또한, 증명기로부터 제공되는 오류 메시지를 활용하여 형식적 증명의 추측을 정교화하는 오류 피드백 메커니즘인 추측 보정을 도입하였다. 기존의 정교화 프레임워크와 달리, 제안하는 추측 보정은 지시(instruction)를 기반으로 생성물을 정교화하지만, 쌍(생성물, 오류 및 보정)을 수집하지 않는다. 제안된 방법은 miniF2F 검증 세트(48.0% → 55.3%) 및 테스트 세트(45.5% → 51.2%)에서 최신 기준(SOTA) 성능을 달성하였다. 또한 Lyra가 해결한 3개의 국제 수학 올림피아드(IMO) 문제도 제시한다. 우리는 도구 보정(환각 완화를 위한 후처리)과 추측 보정(환경과의 상호작용을 통한 하위 목표 조정)이 이 분야의 미래 연구에 유망한 방향성을 제공할 것이라고 믿는다.