클로드도 ETH 반증 주장…논문⁠·⁠증명 코드 함께 공개

앤트로픽이 내부 클로드 연구 모델로 지수시간가설(ETH)의 반증을 찾았다고 주장하고 27일 논문과 Lean 증명 코드를 공개했다. 계산 문제의 이론적 난도를 다루는 연구자에게 자연어 원고와 기계 검사 자료가 함께 제공됐다. 두 핵심 명제는 Lean의 표준 공리 세 가지만 쓴다는 검사 안내도 공개했다.

논문은 성과를 문제가 극도로 커질 때의 이론적 결과로 규정한다. P 대 NP 문제를 직접 해결하거나 실용적인 계산 속도를 높이는 알고리즘은 제시하지 않는다. 부록은 집필 시점에 증명 전체를 확인한 사람은 알려지지 않았다고 적었다.

26일자 원고에 따르면 핵심 알고리즘은 16일 내부 클로드 모델이 사람 입력 없이 출력 토큰 1,400만 개를 쓰며 찾았다. 이후 앤트로픽 연구진이 클로드와 함께 서술을 다듬었다.

3-SAT는 참·거짓 값을 변수에 배정해 모든 조건을 만족시킬 수 있는지 묻는 문제다. 조건 하나는 변수나 부정형 최대 세 개로 이뤄진다. ETH는 변수 수에 비례하는 지수를 가진 시간이 필요하다는 가정이다. 공개 명제는 답의 존재와 개수를 따로 정의했다.

알고리즘은 조건을 점으로, 공유 변수를 연결로 나타내 계산을 작은 문제로 나눈다. 논문은 합을 여러 텐서 네트워크 계산으로 재구성하고 항의 상쇄를 이용해 답의 수를 세는 접근을 설명했다.

기계 검사에 쓰인 명제는 유한한 기호를 쓰는 결정적 튜링 기계와 그 실행 단계 수로 계산량을 표현한다. 일반화한 계수 알고리즘의 입력에는 같은 조건을 중복 기재하지 않고 모든 변수가 등장해야 한다. 변수 네 개 이상·조건 두 개 이상이라는 적용 범위도 명시돼 있다. 정해진 한 기계와 상수로 여러 크기의 입력을 다루는 명제다. 변수 이름과 조건 목록을 이진 기호로 기록하는 방식도 정의했다.

기계가 확인한 명제와 논문 해석

공개 검토 색인은 논문의 번호가 붙은 명제마다 대응하는 Lean 선언을 연결한다. 각 연결은 실제 선언을 가리키도록 작성돼 검사기가 그 존재를 확인한다. 독자는 논문 속 결과에서 해당 코드의 수학적 주장으로 이동해 대조할 수 있다. 이 색인은 부록의 증명까지 포함한다. 논문의 문장과 코드가 같은 표현이라고 읽지 않도록 원문 설명과 실제 선언을 나눠 표시했다.

색인은 원고와 형식화의 차이도 기록했다. 예컨대 두 계산을 번갈아 실행하는 비용은 원고에서 상수 배지만 형식화에서는 입력 길이를 더한 뒤 일정한 거듭제곱으로 다룬다. 연산을 세는 방식과 증명 경로의 차이를 숨기지 않고 항목별로 적어 놓았다. 일부 중간 명제는 해의 존재 여부를 다루고, 계수 결과는 별도 증명으로 연결했다.

검증에는 목표 명제와 제출된 증명을 대조하는 Comparator가 사용된다. 이 도구는 같은 명제를 증명했는지, 허용한 공리만 썼는지, Lean의 핵심 검사기가 받아들이는지를 확인한다. 독립적으로 구현한 추가 검사기도 선택할 수 있어 한 구현에만 기대는 범위를 줄인다.

검사 도구가 내세우는 보장에는 전제가 붙는다. 비교 기준인 목표 명제와 그 의존 파일을 신뢰할 수 있어야 하며, 실행 격리와 검사기 자체가 올바르게 작동해야 한다. 문서가 보장하는 것은 이런 조건 아래 제출된 형식 증명의 일치와 수용 여부다. 추가 검사기 사용은 도구 자체의 선택 사항이다. 제출 코드와 비교 기준을 미리 함께 컴파일하지 않았다는 조건도 안내에 포함된다.

앞서 오픈AI도 26일 ETH 반증 주장을 공개했다. 오픈AI는 16일 자연어 반증을 얻고 17일 Lean으로 형식화했다고 밝혔다. 러셀 임팔리아초·라모한 파투리·라이언 윌리엄스가 이끄는 외부 검토는 오픈AI 자료를 대상으로 하며, 참여자들은 자발적·무보수로 독립된 결론을 내리는 방식이다. 회사는 ETH를 조건으로 삼은 연구 분야에 그래프 이론·계산생물학·데이터베이스·계산기하학 등을 들었다. 누구나 원자료를 살펴보고 의미를 토론하도록 검토를 조직하겠다고 설명했다. 외부 연구자에게 비밀유지계약을 요구하지 않고 중간 결과와 결론을 공개할 수 있게 한다는 원칙도 밝혔다.

앤트로픽 저장소는 공개물을 유지보수·외부 기여 접수가 없는 연구 산출물로 표시했다. 안내문은 기계의 증명 검사와 명제가 논문의 뜻에 맞는지 판단하는 일을 구별하고, 후자의 대조를 원고와 명제를 읽는 사람에게 맡겼다.