Reddit

Internal Claude research model also independently refuted the Exponential Time Hypothesis on October 16, with 14M output tokens and no human input.

Anthropic 내부 Claude 연구 모델도 10월 16일 지수 시간 가설을 독자적으로 반박했습니다. 출력 토큰 1,400만 개, 인간 개입은 없었습니다

Anthropic의 내부 Claude 연구 모델이 3-SAT의 지수 시간 가설(ETH)을 반박하는 결과를 냈으며, 더 어려운 #3-SAT 계수 문제도 준지수 시간에 푸는 알고리즘을 제시합니다. Lean 4 형식화와 별도 커널 검증 절차도 공개했지만, 결과는 점근적이며 실제 문제 풀이 성능을 뜻하지 않습니다.

에디터 노트

ETH가 거짓이라는 결과와 P=NP 증명은 서로 다른 주장입니다. 저장소도 ETH 반박만 말하며 P와 NP의 관계를 해결했다고 주장하지 않습니다. 알고리즘의 점근적 시간 경계는 제시하지만 실제 SAT solver나 암호 해독에 쓸 수 있는 성능은 보장하지 않습니다. Reddit에서 나온 암호 영향 우려와 SAT solver 개선 기대는 모두 가능성을 묻는 의견이며, 저장소가 확인한 결과와 구분해야 합니다. 검증 자료에서는 Lean의 정리 검사가 증명 항목을 확인하고 Comparator와 nanoda가 정리 문장 및 증명을 추가로 검사합니다. 반면 Lean 파일의 정리 문장이 논문 문장과 일치하는지는 기계가 자동으로 확인하지 않는다고 저장소가 밝힙니다. 그래서 짧은 정리 파일과 논문 부록의 대조표를 제공하고 있습니다. 형식화는 증명 검증의 근거를 강화하지만 알고리즘의 실용성을 입증하지는 않습니다. 이 결과에서 가장 분명하게 확인되는 범위는 ETH를 반박하는 이론적 알고리즘과 그 증명 검증 절차입니다.

AI 요약

Anthropic의 연구 모델 Claude가 지수 시간 가설(Exponential Time Hypothesis, ETH)을 반박하는 알고리즘을 발견했다고 공개했습니다. 저장소에는 논문과 Lean 4 형식화가 함께 실렸습니다. 저장소 설명에 따르면 결과는 3-SAT를 변수 수 n에 대해 2^{o(n)} 시간에 푼다는 내용이며, 더 어려운 문제인 #3-SAT, 즉 만족하는 할당의 수를 세는 문제도 2^{O(n log log n / √log n)} 시간에 풉니다. 이 결과는 점근적 분석입니다. 실제 입력 크기에서 빠르게 동작한다는 뜻은 아닙니다.

알고리즘 개요

논문은 임의의 노드 텐서를 가진 K_K 위의 텐서 네트워크를 수축하는 시간을 2^{e(K)·K²λ}·poly(λ)로 나타냅니다. 여기서 λ는 각 간선의 비트 수입니다. 격자에 노드를 배치하고 각 직사각형의 두 대각선을 SWAP 연산으로 봅니다. 비트마다 SWAP을 I − 2·singlet으로 분해하고 singlet 개수에 따라 묶으면 λ+1개의 연산자를 얻으며, 각 연산자의 행 순위와 열 순위 곱은 12^λ 이하입니다. 각 연산자 선택마다 행이나 열 중 비용이 낮은 쪽을 하나의 노드로 합친 뒤 K개의 균형 잡힌 부류로 다시 묶습니다. 이 구성으로 e(9K^16) ≤ 0.9·e(K) + O(1/K)라는 관계를 증명합니다. 저장소는 Claude Opus 5.5가 높은 추론 노력 설정에서 이 요약을 바탕으로 ETH 반박을 다시 유도할 수 있다고 설명합니다. 다만 이 재유도 결과는 임의의 δ>0에 대해 3-SAT를 O(2^{δn}) 시간에 결정한다는 내용이며, 저장소 첫머리에 적힌 더 날카로운 경계와 같지는 않습니다.

Lean 4 검증

MainResults.lean에는 ETH가 거짓이라는 명제와 논문의 주 정리 문장만 적혀 있고 증명은 없습니다. Mathlib 외의 항목을 가져오지 않는 짧은 파일이라 독자가 논문 문장과 대조하기 쉽게 했다는 설명입니다. 논문 각 명제와 Lean 대응 항목 및 차이는 PaperIndex.lean에 정리되어 있습니다. 실제 증명은 저장소에서 빌드하며, 안내된 환경에서는 24개 가상 CPU로 약 8분이 걸리고 가장 큰 프로세스가 메모리 약 7GB를 사용했습니다. Lean이 확인한 두 정리는 propext, Classical.choice, Quot.sound 세 표준 공리에만 의존한다고 출력됩니다. 저장소의 CI는 Comparator로 정리 문장을 Challenge.lean과 비교하고, 별도로 작성된 커널 nanoda로 증명을 다시 검사합니다.

Reddit 반응

  • @jkpatches — 현실 세계에는 어떤 결과가 있나요? 이 가설이 맞다고 가정하는 분야가 실제로 있나요?
  • @bachmensch — 인용하자면, AI 에이전트들은 ETH가 참임을 증명하는 방식으로 P 대 NP를 풀려고 했습니다. ETH가 참임을 증명하면 P≠NP가 되기 때문입니다. 에이전트는 실패했고 대신 ETH가 거짓임을 증명했습니다. 많은 사람이 ETH가 참이라고 믿었으니 꽤 놀라운 일입니다. P 대 NP를 푸는 데 실패한 일이 어떤 의미에서는 성공이 됐습니다.
  • @RemusShepherd — ETH는 P=NP보다 더 강한 제약입니다. 알고리즘이 얼마나 빨라질 수 있는지 제한합니다. ETH가 반박되어도 현실 세계에 큰 결과는 많지 않을 것입니다. 암호화나 다른 복잡한 수학 알고리즘에 작은 최적화가 생길 수는 있습니다. 흥미롭거나 두려운 부분은 P=NP 증명의 발판이 될 수 있다는 점입니다.
  • @Mrp1Plays — P=NP가 증명되더라도 지수나 상수가 너무 커서 단기적으로는 모든 것이 괜찮을 가능성이 큽니다. 일반 알고리즘도 실행하기 쉬운 경우라면 문제가 되겠지만 그런 일은 거의 일어나지 않을 것 같습니다.
  • @alozq — 3-SAT 같은 NP-난해 문제의 알고리즘이 있으면 NP 문제를 3-SAT 사례로 다시 표현하면 됩니다. 문제는 다항 알고리즘의 지수와 상수, 그리고 그 변환에도 있습니다. 가장 빠른 다항 해법의 지수와 상수가 천문학적으로 커서 현실적으로 쓸 수 없을 수도 있습니다.
  • @aturtledude — 이 결과가 결국 SAT solver 개선으로 이어질 수 있지 않을까요? 영향이 클 것 같습니다.
    • @cscottnet — SAT solver는 이미 꽤 잘 작동합니다. 이론상 풀기 어려운 문제가 있어도 실용적인 알고리즘은 잘 작동하는 분야 중 하나입니다. 지금까지 이런 증명은 상수가 엄청나게 컸습니다. 자세한 내용은 모르지만 이 결과도 실용적 개선보다는 이론적 개선일 것 같습니다.
  • @tip2663 — ETH는 어느 쪽이든 P 대 NP 문제의 결론을 증명하지 않습니다.
    • @TieBackground453 — ETH의 부정이 P 대 NP 문제를 증명하지 않는다는 뜻인 것 같습니다.
  • @Hodr — 출력 토큰에 사고 토큰도 포함되나요?
    • @huffalump1 — 아마 그럴 겁니다.

원문: Anthropic formal-math GitHub 저장소 / 번역·요약: Trawling

원문 보기 ↗토론 보기 ↗