Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

기술적 요약: 아리스토텔레스 API 를 활용한 개미 문제의 형식화 사례 연구

문제 진술
본 논문은 제 50 회 국제 수학 올림피아드 (IMO 2009) 의 문제 6 으로 처음 제기된 "개미 문제"의 형식화 사례 연구를 제시한다. 이 정리는 임의의 $n$개의 서로 다른 양의 정수 집합 $\{a_1, \dots, a_n\}$과 $n-1$개의 양의 정수 집합 $M$ (단, 전체 합 $\sum a_i \notin M$) 에 대하여, 어떤 중간 부분합 $S_k = \sum_{i=1}^k a_{\sigma(i)}$도 $M$에 속하지 않도록 하는 점프 순열 $\sigma$가 존재함을 주장한다. 이 문제는 2009 년 IMO 전체 문제 중 평균 점수가 가장 낮았던 역사적 난이도로 유명하며, 순열과 금지 집합을 포함하는 비자명한 조합론적 추론을 요구한다.

방법론
본 연구는 언어 모델 기반 탐색, 비공식 보조정리 생성, 그리고 Lean 4 증명 도우미 (Mathlib 사용) 내 형식화를 결합한 자동 증명 시스템인 아리스토텔레스 API를 활용한다. 저자들은 아리스토텔레스 API 에 개미 문제에 대한 엄격하고 완전한 증명을 요청하는 특정 프롬프트를 제공하였으며, 이를 통해 해당 문제를 알려진 정리로 인용하는 것을 명시적으로 금지하고 유효한 순열의 구성을 요구하였다.

그 결과물인 산출물은 $|M| < n$ (엄격히 $n-1$이 아닌) 을 허용하고 $0 \in M$을 허용하는 일반화된 정리를 포함하는 Lean 4 프로젝트이다. 저자들은 생성된 코드를 세밀하게 검사하여 완전히 기계 검증된 선언과 해결되지 않은 증명 자리 (sorry) 를 포함하는 선언을 구분하였다.

주요 결과 및 검증된 구성 요소
생성된 Lean 개발은 주 정리의 완전한 증명을 산출하지 못하였다. 대신, 네 개의 완전히 검증된 보조 도우미 정리와 하나의 해결되지 않은 주 정리로 구성된 하이브리드 산출물이 도출되었다:

1. 검증된 로컬 구성 요소:

   • PS last: 최종 부분합이 점프의 전체 합과 같음을 검증함.
   • PS swap: 인접한 점프의 교환이 해당 위치의 특정 중간 부분합에만 영향을 미치고 나머지는 변경되지 않음을 검증함.
   • PS swap eq: 교환 후 변경된 부분합의 대수적 형태 ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$) 를 검증함.
   • maximizer swap in M: 국소적 최대성 논증을 검증함. 이는 특정 점수 함수 $G(\sigma)$를 최대화하는 순열이 존재하고, 교환 가능한 위치에서의 부분합이 $M$에 속할 경우, 교환으로 인해 도출된 값 역시 $M$에 속함을 확립함.

2. 해결되지 않은 글로벌 구성 요소:

   • 주 정리인 grasshopper는 단일 sorry로 직접 종료됨.
   • 아리스토텔레스 출력 요약은 결여된 단계를 글로벌 카운팅 논증으로 식별함. 로컬 보조정리들은 특정 교환이 $M$에의 소속을 강제함을 확립하지만, 시스템은 이러한 사실들을 조율하여 적어도 $n$개의 서로 다른 금지된 값을 생성함을 증명하는 데 실패함. 이는 $|M| < n$이라는 가정에 모순을 초래할 것이나, Lean 소스는 주 정리를 별도의 인코딩된 카운팅 보조정리로 환원하지 않음. 그 간극은 증명되지 않은 의무로 남음.

기여
본 논문은 두 가지 주요 기여를 함:

1. 재현 가능한 산출물: 아리스토텔레스 API 를 사용하여 어려운 올림피아드 조합론 문제의 검증 가능한 재현 가능한 Lean 4 형식화 시도를 제공하며, 전체 소스 코드와 실행 로그를 포함함.
2. AI 한계의 정밀 분석: AI 생성 증명의 "증거적 지위"에 대한 상세한 해부를 제공함. 본 연구는 AI 시스템이 로컬, 대수적, 그리고 교환 기반 추론 단계를 성공적으로 검증할 수 있는 반면, 주 정리를 닫기 위해 필요한 글로벌 조합론적 장부 관리 (bookkeeping) 를 수행하는 데는 실패함을 보여줌.

의의 및 주장
본 논문은 "검증된 선언"과 "sorry로 종료된 선언" 사이의 구분이 AI 지원 증명 해석에 있어 결정적이라고 주장함. 이 사례 연구의 의의는 로컬 증명 탐색은 성공할 수 있으나 글로벌 추론은 해결되지 않은 채 남을 수 있음을 보여준 데 있음.

저자들은 sorry를 포함하는 Lean 파일의 성공적인 컴파일만으로는 완성된 증명의 충분한 증거가 되지 못함을 강조함. 이 산출물은 경계 사례로서 기능함: AI 도구는 네 개의 보조 도우미 정리와 같은 방대한 검증된 수학적 개발을 생성할 수 있지만, 증명의 핵심 논리 엔진 (글로벌 모순) 을 여전히 구현하지 않은 채 남길 수 있음. 본 논문은 신뢰할 수 있는 AI 지원 형식화를 위해서는 생성된 코드의 단순한 존재에 의존하기보다 증명 의무와 의존성에 대한 엄격한 검사가 필요하다고 결론 내림.