네 가지 정리 증명기의 이야기 — Isabelle/HOL, Lean, HOL4, Agda 비교

AI 요약

저자는 Isabelle/HOL, Lean, HOL4, Agda에서 각각 소수가 무한히 많다는 정리를 증명한 뒤, 증명기별 사용 경험과 증명 구조를 비교합니다. 증명은 모두 유클리드의 구성법을 따릅니다. 주어진 목록에 있는 수를 전부 곱하고 1을 더한 수를 살펴봅니다. 그 수 자체가 소수라면 목록 밖의 소수를 찾은 셈입니다. 합성수라면 소인수를 찾고, 그 소인수가 목록에 들어 있다고 가정했을 때 모순이 생김을 보입니다. 저자는 Isabelle/HOL과 Agda에 더 익숙한 상태에서 시작했고, HOL4와 Lean은 비교 과정에서 배웠다고 밝힙니다. 따라서 순위와 평가는 공정성을 엄격히 따지지 않은 개인 의견입니다.

기반 논리와 증명 확인

Lean과 Agda는 종속 타입(dependent types)을 기반으로 하며, Curry–Howard 대응을 이용해 타입이 명제를, 프로그램이 증명을 나타내도록 합니다. Isabelle/HOL과 HOL4는 LCF 계열입니다. 작은 증명 커널이 기본 추론 규칙을 검사하고, 증명은 그 규칙에 맞춰 구성합니다.

저자는 Isabelle/HOL과 Lean에서 편집 중 증명 상태가 갱신되고, 구조화된 증명을 단계별로 확인할 수 있다고 설명합니다. HOL4와 Agda는 완성된 증명에서 중간 과정을 살피려면 증명 항을 직접 따라가야 합니다. 다만 두 도구에서도 현재 상태와 관련 정보는 확인할 수 있습니다.

자동화와 논리의 선택

Isabelle/HOL에는 SAT·SMT 풀이기와 일차 논리(FOL) 풀이기 등을 호출하는 sledgehammer가 있습니다. 번거롭지만 풀릴 법한 목표를 대신 해결하는 경우가 많지만, 생성된 증명은 이해하기 어렵다고 평가합니다. HOL4에도 HolyHammer가 있지만, 저자는 글을 쓰고 난 뒤에야 이를 알았다고 덧붙입니다. Isabelle/HOL과 HOL4는 복잡한 가정을 정리하는 자동 단순화와 증명 방법도 강합니다.

Lean의 자동화는 괜찮지만 두 HOL 계열만큼 생산적이지 않다고 봅니다. grind는 때로 sledgehammer에 맞먹지만, 어떤 목표에서는 효과가 없고 이유를 파악하기 어렵다고 합니다. sledgehammer와 grind는 목표를 풀지 못하면 진전을 만들지 않는 반면, simp나 Isabelle/HOL의 auto, HOL4의 gvs는 일부를 처리한 뒤 목표 상태를 개선할 수 있습니다. 저자는 실제 작업에서 이런 부분 자동화가 특히 유용하다고 봅니다. Lean과 Isabelle/HOL에는 현재 목표를 여러 방법으로 시도하는 try 계열 명령도 있습니다. 저자는 HOL4에서 이에 해당하는 기능을 찾지 못했다고 적습니다.

Agda는 자동화가 거의 없습니다. 함수 입력으로 계산할 수 있는 단순화 외에는 증명자가 직접 처리해야 합니다. 저자는 이 점 때문에 증명 과정에서 수작업이 크게 늘었다고 평가합니다. 반면 Agda는 기본 설정이 구성적(constructive)입니다. 증명으로 소수의 무한성을 보이는 데 그치지 않고, 주어진 수보다 큰 소수를 실제로 생성하는 프로그램을 얻을 수 있습니다. 다만 예시 증명은 (n + 1)! + 1 부근의 수를 검사하므로 실행이 매우 느립니다.

Isabelle/HOL과 HOL4는 배중률(LEM)과 선택 공리로 이어지는 힐베르트의 엡실론을 공리로 받아들입니다. 저자는 이런 고전 논리가 자동 풀이기에 도움이 된다고 봅니다. Lean은 이론상 구성적이지만, 좋은 자동화 일부가 배중률을 요구하고 실제 사용에서도 고전 논리를 쓰는 경우가 많아 저자도 그렇게 진행했습니다. Agda는 구성적 방식을 유지했습니다.

편집기, 검색, 증명 코드

Lean은 VS Code 사용을 강하게 권장하고, Isabelle/HOL은 자체 편집기인 jEdit를 사실상 요구합니다. HOL4는 Emacs나 Vim 모드에서 실행 중인 REPL과 텍스트를 주고받습니다. 저자는 낯선 방식이지만 잘 작동한다고 말합니다. Agda도 Emacs 모드로 작업하며, 파일 안에서 상태를 갱신하고 증명 목표를 추가합니다.

정리 검색에서는 Isabelle/HOL의 편집기 패널과 find_theorems, HOL4의 DB.find와 DB.match를 높게 평가합니다. 이름뿐 아니라 원하는 형태에 맞는 정리를 검색할 수 있어 유용하다고 합니다. Lean의 leansearch, loogle도 소개하지만, Isabelle/HOL·HOL4만큼 유연하지 않다고 봅니다. Agda에는 이에 해당하는 기능이 없어 표준 라이브러리를 직접 찾아야 합니다.

예시 증명은 나눗셈 관계, 목록 원소가 목록의 곱을 나눈다는 보조정리, 소인수 존재, 목록 밖의 소수 존재를 차례로 다룹니다. Isabelle/HOL 증명은 짧고 자동화 비중이 크지만, 무슨 일이 일어나는지 코드를 읽기만 해서는 파악하기 어렵습니다. HOL4도 metis_tac 같은 일차 논리 풀이기가 많은 일을 처리합니다. Agda는 패턴 매칭과 증명 항을 직접 써야 하는 대신 구조가 눈에 잘 보입니다. Lean은 자동화와 명시적 단계를 섞지만, 저자는 보조정리를 찾고 문법을 익히는 과정에서 예상보다 애를 먹었다고 합니다.

저자의 종합 평가

저자는 정리 검색과 자동화에서는 Isabelle/HOL·HOL4가 앞서고 Lean이 그 뒤를 잇는다고 평가합니다. Agda는 증명 항이 지시한 내용 그대로라는 장점이 있지만, 수동 증명 탐색 부담이 큽니다. HOL4는 REPL 중심 작업 방식과 강력한 기능이 인상적이었고, Lean은 즐거운 점도 있었지만 자동화 동작이 때때로 예측하기 어렵다고 말합니다. Isabelle/HOL은 익숙함 때문에 평가에 편향이 있을 수 있다고 덧붙입니다. 한 종류의 증명기만 써 봤다면 다른 기반의 도구도 직접 시도해 보라고 권합니다.

Lobsters 반응

• @ettolrach — 저는 Agda만 배웠는데, 다른 인기 있는 증명기도 배워야 할 것 같으면서도 다른 증명기의 증명을 이해하지 못하겠습니다. 증명을 이해하기보다 컴파일러가 검사했다는 사실을 믿는 게 목적일까요? Agda는 전술(tactic)이 거의 없어서 증명을 마치면 읽기 쉬운 프로그램이 남습니다. 글에 나온 2가 소수라는 증명을 예로 들면, Agda에서는 gt1과 div 필드가 요구하는 내용을 찾아보고 각 인자가 무엇을 나타내는지, 어떤 값을 반환해야 하는지 따라갈 수 있습니다. 하지만 Lean 증명은 첫 simp가 왜 필요한지, grind가 실제로 무엇을 하는지 모르겠습니다. 수학적 증명으로 옮겨 이해하기 어렵다는 점이 개인적으로 불편합니다.
  • @k749gtnc9l3w — 코드를 쓰기 좋은 형태, 읽기 좋은 형태, 수정하기 좋은 형태가 서로 다르다는 사실이 또 드러난 사례입니다. 증명을 작성할 때는 옆 화면에 목표 목록이 있어서 simp가 무엇을 했는지 볼 수 있습니다. 단계별 목표 화면이 없는 증명 코드만 보면 그 정보를 알 수 없습니다. 각 단계 뒤의 목표 목록을 내보내는 기능이 보편화되면 좋겠지만, 아직 거기까지는 이르지 못했습니다.
  • @danilafe — 전술을 쓰는 힘 가운데 하나는 어느 시점에서든 증명 상태를 살펴볼 수 있다는 점이라고 생각합니다. HTML로 렌더링한 증명에서도 이를 가능하게 하는 도구가 있습니다. 이름은 기억나지 않지만 찾기 어렵지는 않을 겁니다. 그러니 증명 단계를 머릿속에서 전부 계산할 필요는 없고, 전체적인 흐름을 따라가면 됩니다. Lean 증명은 그 흐름을 꽤 잘 보여준다고 생각합니다.
  • @ahelwer — ‘증명 언어의 패러다임’이라고 부를 만한 현상입니다. 어딘가에 이미 쓰인 말일 것 같지만 어디인지는 모르겠습니다. 지금까지 나온 증명 언어에는 증명을 쓰기 쉬운 정도와 읽기 쉬운 정도 사이에 절충이 있습니다. 선언적인 증명은 비형식적인 수학 증명처럼 읽히지만, 작성 중 증명기가 막힌 이유를 이해하기는 더 어렵습니다. TLA+의 증명 언어가 제가 아는 가장 극단적인 선언형 사례입니다. 증명 의무를 처리하지 못한 이유를 찾는 데 도움은 많지 않지만, 긴 하위 증명을 접으면 읽기 쉽습니다. 전술은 전혀 지원하지 않습니다. Lean은 그 반대입니다. 가정과 목표 상태를 직접 조작하는 단계로 증명을 작성하며, 자동화 전술도 자주 씁니다. 작성 중 증명 의무를 해결하지 못한 이유를 파악하기는 쉽지만, Lean 개발 환경에서 단계를 따라가지 않고 증명을 읽기는 어렵습니다.
• @ashikun — 구성적 성격과 자동화 기능을 함께 갖춘 Rocq는 이 비교에서 어디쯤인지 궁금합니다. Lean을 써 보려다 실패한 Rocq 사용자 관점에서 보면 비슷한 순위일 것 같지만, 확신은 없습니다. Rocq 사용자로서 Lean이 더 잘하는 점이 무엇인지, 반대의 경우는 무엇인지 제대로 파악하지 못했습니다.
  • @ahelwer — 증명기를 배우는 사람은 대개 10년에 하나 정도 새로 익히는 것 같습니다. 비교 사례를 모으기 어려운 이유도 큰 투자 비용 때문입니다.

원문: blueberrywren.dev / 번역·요약: Trawling