LLM을 활용해 Lean에서 공식 증명을 생성하는 워크플로우의 비용 효율성을 높이는 방법을 연구했어요. 데이터 평면은 자연어 분해, 공식화, 증명 시도를 담당하고, 제어 평면은 실패한 시도를 분석하여 성공 가능성과 비용을 예측하고 다음 단계를 결정해요.
실패한 Lean 시도에서 얻은 정보를 활용해 비용을 줄이는 에이전트 기반 시스템을 개발했어요. PutnamBench의 일부 문제에서 기존 방식보다 평균 **25.8%** 비용을 절감하면서도 성능은 유지했어요.
연구 결과, 실패한 Lean 시도는 비용 효율적인 자원 할당을 위한 중요한 정보를 제공하며, 에이전트 기반 정리 증명 시스템의 효율성을 높일 수 있음을 시사해요.