AI 기반 형식 증명 탐색을 통한 수학 연구의 발전

대규모 언어 모델 (LLMs)은 수학적 추론 (mathematical reasoning) 분야에서 점점 더 뛰어난 능력을 보여주고 있지만, 그 신뢰성 문제로 인해 수학 연구에서의 활용에는 한계가 있습니다. 이에 대한 완화 방안으로 Lean과 같은 언어를 사용하여 LLMs가 형식 증명 (formal proofs)을 생성하도록 하는 방법이 있습니다. 본 연구에서는 미해결 문제 (open problems)를 해결하는 이 방법의 능력을 최초로 대규모 평가합니다. 당사의 가장 유능한 에이전트 (agent)는 문제당 수백 달러의 비용으로 353개의 미해결 Erdős 문제 중 9개를 자율적으로 해결하였고, 492개의 OEIS 추측 (conjectures) 중 44개를 증명하였으며, 현재 조합론 (combinatorics), 최적화 (optimization), 그래프 이론 (graph theory), 대수 기하학 (algebraic geometry), 양자 광학 (quantum optics) 연구에 배치되어 활용되고 있습니다. LLM 기반 생성과 Lean 기반 검증을 교대로 수행하는 기본 에이전트는 Erdős 문제에서의 성공을 재현했으나, 가장 어려운 문제들에 대해서는 더 많은 비용이 소요되었습니다. 이러한 발견은 AI 지원 형식 증명 탐색 (AI-aided formal proof search)의 위력을 입증하며, 이를 가능하게 하는 에이전트 설계에 대한 통찰을 제공합니다.