OpenAI 수학 연구 저장소, 원고 722편·형식 증명 자료 공개

OpenAI가 내부 미공개 모델로 만든 수학 원고 722편을 372개 연구 묶음으로 정리해 저장소에 공개했다. 약 4000개 문제를 제시했으며, 대부분의 결과에 평균 3시간의 모델 연산을 썼다고 밝혔다. Lean 형식 증명은 일부 원고에만 있으며, 형식화하지 않은 결과에는 문제가 있을 수 있다고 설명했다.

앞선 공개 예고에 이어 실제 저장소의 원고 수, 생성 절차, 증명 자료 범위가 제시됐다.

372개 연구 묶음은 주된 결과와 보조 논증·파생 결과·대안 증명 등을 함께 분류한다.

저장소에는 PDF·소스 파일·인용 및 빌드 안내와 Lean 증명 목록·검증 구성이 포함된다.

일부 결과에 대해서는 모델 추론의 축약 요약도 공개했다.

OpenAI는 추가 Lean 형식 증명을 계속 올리고, 수정본을 새 버전으로 기록해 이전 공개본도 보존할 계획이라고 밝혔다.

연구자는 논문뿐 아니라 연결된 형식 증명과 추론 요약을 함께 살펴 결과를 검토할 수 있다.

앞선 소식 보기