Lean4가 테렌스 타오의 최근 논문에서 작은 버그를 발견하는 데 도움을 줌

 (mathstodon.xyz/@tao)
3P by GN⁺ | ★ favorite | 댓글 1개
  • Terence Tao는 Lean4 형식화 프로젝트를 진행하다가 논문 속 작지만 사소하지 않은 오류를 발견함
  • 오류는 arXiv 논문 2310.05328의 6페이지 논증에서 드러났으며, 1/2 log((n - 1)/(n - k - 1))가 n = 3, k = 2에서 발산함
  • 문제는 작은 n 값에 한정되어, n >= 8에서는 기존 논증이 작동하고 작은 n은 더 거친 방법으로 직접 처리 가능함
  • Lean은 0 < n - 3 증명을 요구했지만 가정은 n > 2뿐이어서, linarith 전술이 필요한 모순을 얻지 못함
  • Tao는 일부 수치 상수를 조정해 논증을 고치고, Lean 형식화 시도 중 이전 논증의 부정확성이 발견됐다는 각주를 새 버전에 넣을 예정임

Lean4 형식화가 드러낸 오류

  • Terence Tao는 자신의 Lean4 형식화 프로젝트 과정에서 논문에 작지만 사소하지 않은 버그가 있음을 발견함
  • 형식화 대상은 arXiv 논문 2310.05328의 6페이지 논증이었음
  • 문제가 된 식은 다음 형태임
    • 1/2 log((n - 1)/(n - k - 1))
  • 이 식은 n = 3, k = 2인 경우 발산함

오류의 범위와 수정 방식

  • 이 문제는 작은 n 값에서만 발생함
    • n >= 8에서는 해당 논증이 여전히 작동함
    • 작은 n은 더 거친 방법으로 직접 처리할 수 있지만, 상수는 더 나빠짐
  • Tao는 해당 페이지의 일부 수치 상수를 바꿔 논증을 고칠 수 있다고 봄
  • 새 논문 버전에는 이전 논증이 약간 부정확했으며, Lean으로 형식화하려다 발견됐다는 각주를 추가할 예정임

Lean이 막힌 구체적 지점

  • 형식화가 실패한 지점에서 Lean은 0 < n - 3을 증명하라고 요구함
    • 사용 가능한 가정은 n > 2뿐이었음
    • linarith 전술은 0 < n - 3의 부정으로부터 모순을 도출하지 못함

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 그는 이달 초에 GPT-4의 도움으로 Lean4를 배우기 시작했음: https://mathstodon.xyz/@tao/111208692505811257
    이번 달 그의 Mastodon 글 상당수가 학습 진행에 관한 것이었고, 대형 언어 모델이 최상위권 성취자들의 작업까지 얼마나 가속할 수 있는지 보여주는 흥미로운 사례임

    • 코딩을 못 해도 소통 능력이 좋은 사람은 대형 언어 모델로 동작하는 자동화를 빠르게 만들 수 있더라
      흥미롭게도 이런 도구는 고숙련자만 효과적으로 활용한다면 불평등을 더 키울 수도 있음
    • GPT-4는 놀라움. 요즘 프로그래밍 관련 질문을 시작할 때 Google을 거의 쓰지 않게 됨
    • 어느 정도 동의하지만 Terry는 너무 예외적인 인물이라, 이 사례를 일반화하기는 어렵다고 봄. 물론 그는 관대하고 겸손한 사람이기도 함
    • 엘리트에게는 쉽게 100배 도구가 됨. 이제 최상위 엔지니어는 10000배 생산성을 내는 사람들임

  • Lean4를 쉽게 접하고 싶다면 Natural Number Game이 좋음: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
    게임 없이 읽기만 하고 싶다면 여기: https://lean-lang.org/theorem_proving_in_lean4/introduction.html

    • 초보라서 궁금한데, Lean4는 TLA+나 Alloy와 어떻게 다른가? 애초에 비교할 만한 대상인지도 궁금함
      처음엔 Alloy를 Allow라고 썼었음

  • 몇 년 전, 내가 작성하는 프로그램의 실수를 줄이는 방법을 찾다가 Lamport의 TLA+ 를 알게 됐고, 상태 기계로 프로그램 동작을 생각하며 형식 명세를 작성하는 법을 배웠음
    TLA+는 추상화를 명확하게 이해하게 해줬고, 이후 Coq 증명 보조기를 사용해 형식적으로 올바른 소프트웨어를 만드는 Software Foundations 시리즈도 발견함. 연습문제가 작은 게임처럼 되어 있어 꽤 즐겁게 풀었음: https://softwarefoundations.cis.upenn.edu/

    • 코드 정확성은 잃어버린 기술이 됐음. 추상적으로 생각해야 한다는 요구가 많은 개발자를 겁먹게 만듦
      고수준 추상화인 형식 명세는 코드를 설명하기 위한 전용 언어에 집중하고, 저수준 추상화인 코드 계약은 검증 로직을 더 나은 모델로 대체하는 쪽에 가까움. C#에는 한때 Code Contracts[1]가 있었고, Z3 SMT 솔버[2]로 컴파일 시점에 계약을 검사하는 단순하지만 강력한 방식이었지만 몇 년 뒤 폐기됐고[3], .NET Runtime에서 제거되며 사실상 끝났음. 지금 C#에서 가장 가까운 것은 아마 Dafny[4]이고, C# 개발 쪽은 여전히 이를 언어에 직접 넣는 방법을 고민 중임[5]
      [1] https://www.microsoft.com/en-us/research/project/code-contracts/
      [2] https://github.com/Z3Prover/z3
      [3] https://github.com/microsoft/CodeContracts
      [4] https://github.com/dafny-lang/dafny
      [5] https://github.com/dotnet/csharplang/issues/105
    • Idris2도 살펴봤는지 궁금함. 이런 정리 증명기를 볼 때마다 일반 프로그래밍과 임피던스 불일치가 있는 느낌이었음
      Idris2는 범용 언어를 지향하면서도 정리 증명을 위한 더 발전된 타입 시스템을 제공하는 것처럼 보임: https://github.com/idris-lang/Idris2
    • 나도 Software Foundations에서 같은 긍정적인 경험을 했음
      Coq 대신 Agda를 쓰는, 어느 정도 파생된 책도 있음: https://plfa.github.io/
      아직 읽어보진 못했지만 목록에 올려뒀고, Agda나 Idris는 Coq보다 프로그래밍 언어처럼 느껴질 가능성이 크다고 봄

  • 의존 타입이 정말 기대됨. 다만 당분간은 나오기 어려울 듯함
    Dependent Haskell은 진행 중이지만 기존 언어에 나중에 끼워 넣기가 어렵다고 하고, Idris 제작자도 Idris가 다른 언어의 모델이 되길 기대한다고 했지 주류 채택은 어려워 보임. Coq, Agda, F*도 범용 언어로 설계된 것은 아님. 컴파일러 구현은 복잡하고 문법도 장황해질 수 있지만, 내가 원하는 것은 단순함. 입력과 출력에 대해 알고 있는 모든 것을 인코딩하고 싶음. 지금 주류 언어에서는 인자나 출력에 대해 타입 시스템이 표현하게 해주는 것보다 더 많은 것을 알고 있는 경우가 많음

    • 의존 타입에 대한 기대에는 완전히 공감하지만, 우리가 익숙한 타입 시스템과 달리 의존 타입에 대한 정리는 증명하기 훨씬 어려워서 전체 프로그램에 쓰기에는 편하지 않아 보임
      TypeScript처럼 점진적인 방식으로, 모든 곳에서 전부 증명하지 않아도 임의의 위치에 타입 수준의 값 제한 정보를 추가할 수 있으면 좋겠음
    • 의존 타입을 쉽게 설명하면, 변수의 타입이 다른 변수의 값에 의존할 수 있는 개념임
      예를 들어 숫자 목록과 그 길이를 함께 알고 있다면, 의존 타입으로 길이를 명시적으로 포함한 목록 타입을 만들 수 있고, 컴파일 시점에 연산이 그 길이를 지키는지 보장할 수 있음. 길이 3짜리 목록만 받는 함수를 지정했는데 길이 4짜리를 넘기면 컴파일되지 않아서 실행 전에 실수를 잡을 수 있음. 타입이 더 표현력 있어지고 변수들 사이의 복잡한 관계까지 인코딩하는 추가 안전 검사층 같은 느낌임

  • 우리 세대의 가장 뛰어난 지성 중 한 명이 대형 언어 모델과 자동 증명의 조합으로 작업 폭을 넓힐 수 있다면, 이 기술 조합의 미래가 매우 낙관적으로 보임
    시작은 버그 수정이고, 이어서 검증을 돕다가, 결국 새로운 발견을 밀어붙이고 한계를 넓히게 될 것 같음. 무어의 법칙 같은 동역학이 원래 그런 누적 성질이 없던 분야를 “감염”시키는 현상을 부르는 용어가 필요함. 추가 맥락으로 Terence Tao가 Lean을 배우는 데 Copilot을 쓰고 있음: https://mathstodon.xyz/@tao/111271244206606941
    Copilot 없이도 할 수 있었겠지만, 새 도구를 받아들이는 마찰 때문에 시작하지 않았을 수도 있음. 대형 언어 모델은 이런 “생각의 자전거” 같은 상황에서 큰 잠재력이 있음

    • Lean 4는 프로그래밍 언어이자 정리 증명기이고, 내가 알기로는 대형 언어 모델과는 관련이 없음
    • 대형 언어 모델은 영어 같은 자연어를 위한 컴파일러임

  • 몇 년 전에 Terence Tao의 수학 블로그 글에서도 버그를 하나 찾은 적이 있음. 알려줬더니 고쳤고 감사 인사도 받았음
    물론 Hacker News 첫 페이지에 오르진 못했음

  • Lean4가 또 다른 대형 언어 모델인 줄 알고 걱정했는데, 실제로는 꽤 견고하고 신뢰할 만한 도구였음

    • Terence Tao가 논문에서 버그를 찾는 데 도움이 되는 것이라면, 내 기준에서는 충분히 견고하고 신뢰할 만함
    • Lean 4 커뮤니티는 증명 보조와 형식화를 위해 대형 언어 모델과 정리 증명기를 결합하는 데 꽤 낙관적임
    • “Terry Tao가 ChatGPT를 새 정리 증명에 매우 유용하게 쓴다”였다면, 개인적으로는 이 소식보다 더 큰 뉴스였을 듯함
    • 그는 형식화 작업에 Copilot이 유용하다고 보고 있음: https://mathstodon.xyz/@tao/111271244206606941

  • Lean 증명 검사기 같은 형식 증명 검사기와, Lean 같은 형식 언어로 합성 추측-증명 쌍을 생성하는 언어 모델을 결합할 수 있을지 궁금함
    Lean 증명 검사기로 언어 모델이 쓴 합성 증명이 올바른지 자동 검증하고, 그 정보를 원래 언어 모델에 적용할 강화학습 보상 신호로 쓰면 더 나은 증명을 쓰게 만들 수 있음. 또는 이전 라운드의 올바른 합성 증명을 학습 데이터로 삼아 새 모델을 훈련할 수도 있음. 더 적대적으로 만들 수도 있음. 추측 생성 모델과 증명/반증 모델로 나누고, 합성 증명이 Lean 증명 검사기에서 검증될지를 예측하는 모델을 추가함. 정답 확률이 낮다고 예측될수록, 실제로 올바른 증명을 냈을 때 증명 생성 모델이 더 큰 보상을 받는 식임. 마지막으로 특정 합성 추측에 대해 증명 생성 모델이 받을 보상을 예측하는 모델을 추가하면, 추측 생성 모델은 증명 생성 모델에 너무 어렵지도 쉽지도 않은 높은 보상 예상 추측을 만들도록 보상받음. 전체 시스템이 점점 더 어려운 합성 증명을 만들어내고, 이것이 증명 생성 모델의 더 나은 자기 학습으로 이어질 수 있음. 원리적으로는 증명 생성에서 초인적 능력까지 확장될 수 있고, GAN이나 AlphaGo Zero의 자기 대국과 비슷함. 어려운 부분은 초기 부트스트래핑으로, 생성 모델의 최초 학습에는 사람이 제공한 Lean 증명 데이터가 필요함. 하지만 합성 증명이 충분히 좋아지면 시스템이 자동으로 자기 학습을 이어갈 수 있음

  • Tao가 이 여정에서 GPT-4를 포함한 대형 언어 모델 도구를 어떻게 썼는지에 대한 이전 맥락은 여기 있음: https://mathstodon.xyz/@tao/111233986893287137

  • 그의 진행 상황은 GitHub에서도 따라볼 수 있음: https://github.com/teorth/symmetric_project/

답변달기