Palomar: Lean 검증 수학 레지스트리

최근 AI가 생성한 수학적 증명이 급증함에 따라, 해당 증명이 실제로 의도한 바를 정확히 증명하는지 검증하는 것이 중요해졌습니다. 이를 위해 Lean FRO와 ICARM이 주도하는 Palomar 레지스트리가 공식 출시되었습니다.

Palomar는 외부 GitHub 저장소의 특정 커밋(snapshot)을 등록하는 방식으로 운영되며, 등록을 위해 다음 세 가지 요소를 요구합니다:

• Challenge file: 결과에 대한 인간이 읽을 수 있는 짧은 설명
• Solution module: 결과에 대한 증명 코드
• formalization.yaml: 결과에 대한 비형식적 설명 및 메타데이터

등록된 저장소는 두 단계의 검증 과정을 거칩니다:

1. 기계적 검증: Lean 도구인 Comparator를 사용하여 솔루션 모듈이 챌린지 파일의 결과를 정확히 증명하는지 확인합니다.
2. 비결정적 검증: **대규모 언어 모델(LLM)**을 활용하여 formalization.yaml의 비형식적 설명이 챌린지 파일의 내용과 일치하는지 확인합니다.

Palomar는 학술적 신규성을 검토하는 피어 리뷰 저널은 아니지만, AI 및 인간이 생성한 수학적 증명의 신뢰성을 확보하기 위한 인프라 역할을 수행합니다.