Daily Arxiv

전 세계에서 발간되는 인공지능 관련 논문을 정리하는 페이지 입니다.
본 페이지는 Google Gemini를 활용해 요약 정리하며, 비영리로 운영 됩니다.
논문에 대한 저작권은 저자 및 해당 기관에 있으며, 공유 시 출처만 명기하면 됩니다.

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

Created by
  • Haebom

저자

Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

개요

APOLLO는 Lean 컴파일러와 LLM의 추론 능력을 결합하여 수학 정리를 증명하는 자동화된 정리 증명 시스템입니다. 기존의 LLM 기반 정리 증명 방식은 많은 샘플링(수천 번)을 통해 검증 시스템을 통과하는 증명을 생성하는 반면, APOLLO는 LLM이 증명을 생성하고, 에이전트들이 증명의 구문 오류를 수정하고, Lean을 사용하여 실수를 파악하고, 실패한 부분 정리를 분리하고, 자동 솔버를 활용하며, 남은 목표에 대해 저렴한 비용으로 LLM을 호출하는 모듈식 파이프라인을 사용합니다. 수정된 부분 증명을 재결합하고 재검증하는 과정을 사용자 제어 가능한 최대 시도 횟수까지 반복합니다. miniF2F 벤치마크에서 8B 미만 매개변수 모델 중 84.9%의 정확도를 달성했으며, 샘플링 비용은 100 미만으로 유지했습니다. 또한, GoedelProverSFT의 정확도를 65.6%로 높이고, 샘플 복잡도를 25,600에서 수백으로 줄였습니다.

시사점, 한계점

시사점:
LLM 출력의 타겟팅된 컴파일러 가이드 수정을 통해 효율성과 정확성이 크게 향상됨을 보여줌.
자동 정리 증명을 위한 확장 가능한 일반적인 패러다임 제시.
저렴한 샘플링 비용으로 높은 정확도 달성 (miniF2F 벤치마크에서 84.9%, GoedelProverSFT에서 65.6%).
일반 목적 모델의 정확도를 크게 향상 (3-7%에서 40% 이상).
한계점:
현재는 특정 벤치마크(miniF2F, GoedelProverSFT)에 대한 성능만 제시되었으며, 다른 벤치마크나 더 복잡한 정리에 대한 일반화 가능성은 추가 연구가 필요함.
APOLLO의 성능은 사용된 LLM과 Lean 컴파일러에 의존적이며, 다른 시스템과의 호환성 및 이식성에 대한 추가 연구가 필요함.
사용자 제어 가능한 최대 시도 횟수 설정 등, 파라미터 최적화에 대한 추가 연구가 필요함.
👍