Advancing Mathematics Research with AI-Driven Formal Proof Search

Motivation

• Known: LLM은 수학 추론 능력이 뛰어나지만 신뢰성 부족으로 실제 연구에 활용되기 어렵다. 최근 연구들은 LLM을 Lean 같은 형식 언어로 증명을 생성하도록 유도하여 컴파일러 검증을 통해 정확성을 보장하는 방식을 탐구해왔다.
• Gap: 기존 연구는 경시대회 수학(competition mathematics) 또는 자연언어 증명의 형식화에 제한되어 있었으며, 개방형 연구 문제(open research problems)에 대한 대규모 평가가 없었다. 또한 다양한 에이전트 설계의 효과를 체계적으로 비교 분석한 사례가 부족했다.
• Why: 형식 증명은 LLM의 환각(hallucination) 문제를 근본적으로 해결할 수 있는 방법이며, 실제 수학 연구에 AI를 적용 가능한지 검증하는 것은 매우 중요하다. 개방형 문제 해결은 경시대회 문제보다 훨씬 어려워 실질적인 연구 능력을 보여줄 수 있기 때문이다.
• Approach: AlphaProof Nexus 프레임워크는 기본 에이전트(A)에서 시작하여 단계적으로 복잡해진다. 기본 에이전트는 독립적인 prover subagents의 Ralph loop를 실행하고, 향상된 버전(B)은 AlphaProof를 쿼리하여 부분 증명을 채운다. 진화 에이전트(C)는 evolutionary algorithm으로 subagents를 조정하며, 완전 버전(D)은 AlphaProof와 진화 탐색을 모두 활용한다.

Achievement

Figure 2 | Design of the full-featured AlphaProof Nexus agent. The mathematician provides

주요 성과:

• Erdős 문제 353개 중 9개 자동 해결 (1개당 수백 달러 추론 비용)
• 56년 이상 미해결 문제 2개 포함
• OEIS 추측 492개 중 44개 증명
• 대수기하의 15년 미해결 문제 해결
• 볼록 최적화 경계 개선 (새로운 알고리즘 매개변수 스케줄 발견)
• 양자광학, 그래프 이론 등 다양한 연구 분야에 배포 중

How

Figure 1 | Example inputs/outputs for an AlphaProof-equipped agent (applied to Erdős

• Lean 파일 형식으로 정리된 증명 스케치 입력 (sorry 자리표시자 포함)
• EVOLVE-BLOCK, EVOLVE-VALUE 마커로 수정 가능 영역 지정
• Multi-turn LLM 추론 루프에서 chain-of-thought 기반 상향식 정제
• Lean 컴파일러의 오류 메시지를 다음 LLM 호출에 피드백
• AlphaProof를 focused proof tool로 활용하여 특정 부분 목표 해결
• Evolutionary algorithm으로 sketch 모집단을 Elo 평가 기반으로 관리

Originality

• 형식 증명으로 개방형 연구 문제를 대규모로 해결한 첫 사례
• 이진 증명 성공/실패를 graduated fitness landscape로 매핑하기 위해 rating agents와 Elo 시스템 도입
• LLM-Lean compiler의 밀접한 통합으로 자동 오류 수정 루프 구현
• AlphaProof와 evolutionary search를 하나의 에이전트로 통합한 아키텍처

Limitation & Further Study

한계:

• 높은 추론 비용 (1개 문제당 수백 달러, 가장 어려운 문제는 더 높음)
• 9/353 성공률은 절대적으로는 낮으며, 선택된 문제 세트의 난이도 분포 미상세
• Lean 형식화된 문제로 제한되어 있음
• AlphaProof 미사용 기본 에이전트도 동일한 9개 문제 해결 (에이전트 설계의 실제 기여도 불명확)
• 증명의 자동성 정도와 인간 개입 수준에 대한 상세 분석 부족

후속 연구: 비용 효율성 개선, 더 광범위한 수학 분야 확대, 형식화 자동화

Evaluation

총평: 이 논문은 LLM 기반 형식 증명이 실제 개방형 연구 문제를 해결할 수 있음을 처음 대규모로 입증한 중요한 연구이다. 혁신적인 에이전트 아키텍처와 실질적인 수학 연구 성과(Erdős 문제 해결, OEIS 추측 증명)는 AI의 수학 연구 기여를 구체적으로 보여준다. 다만 비용 효율성 개선 필요 및 기본 에이전트도 동등한 성능을 보인 점은 제한사항이나, 전반적으로 형식 증명 기반 AI 활용의 가능성을 강하게 입증하는 의미 있는 논문이다.