이 글은 유클리드 방식으로 소수가 무한히 많다는 정리를 Lean, Isabelle/HOL, HOL4, Agda에서 형식화하고, 증명 탐색과 조작의 편의성 등을 비교한 의견형 리뷰다. 비교자는 공정한 평가가 아니라고 전제하며, 최종적으로 HOL4를 가장 높게 평가한다.
네 시스템은 증명 기초와 상호작용 방식에서 차이를 보인다. Isabelle/HOL과 HOL4는 작은 증명 커널을 중심으로 하는 LCF 방식이고, Lean과 Agda는 종속 타입과 커리-하워드 대응을 활용한다. Isabelle/HOL과 Lean은 입력 중 증명의 중간 상태를 확인하기 쉽다. 반면 HOL4와 Agda는 완성된 증명 항을 살펴보려면 직접 구조를 풀어야 한다.
자동화와 정리 검색에서는 Isabelle/HOL과 HOL4가 앞선다는 평가다. Isabelle/HOL의 sledgehammer와 HOL4의 자동화 도구는 증명 작업을 줄여 주지만, 생성된 증명이 이해하기 어려울 수 있다. Lean에는 grind, simp 등의 도구가 있지만, 비교자는 부분적으로 진전을 만드는 자동화가 상대적으로 부족하다고 본다. Agda는 자동화가 거의 없어 직접 증명을 구성하는 일이 많다. 정리 검색 기능도 Isabelle/HOL과 HOL4가 편리하고, Lean의 검색 도구는 내장 기능이 아니며 유연성이 떨어진다고 평가한다. Agda에는 이에 해당하는 기능이 없다고 설명한다.
비교자는 Isabelle/HOL과 HOL4의 고전 논리가 자동화에 유리하다고 본다. Lean은 원칙적으로 구성적이지만, 이 비교에서는 고전 논리 방식으로 사용했다. Agda는 구성적 논리를 기본으로 하므로 증명에서 소수의 존재를 보이는 데 그치지 않고 실제로 값을 계산해 낼 수 있다. 다만 유클리드 증명에 쓰인 구성은 계산이 느렸다. 글에 제시된 입력값 0~8의 결과는 각각 2, 3, 7, 5, 11, 7, 71, 61, 19였으며, 입력값이 커질수록 계산 시간이 늘어 입력값 8에서는 40초가 걸렸다.
네 시스템에서 형식화한 증명은 구조적으로 대체로 비슷했지만, 코드 길이는 Isabelle/HOL 117줄, Lean 155줄, HOL4 190줄, Agda 264줄이었다. 비교자는 이 수치가 직접 비교하기 어려운 기준이라고 덧붙인다. 특히 Isabelle/HOL의 증명은 짧지만 흐름을 파악하기 어렵고, Agda는 더 명시적이지만 코드가 길어지는 사례를 든다.
비교자의 주관적 순위에서 증명 탐색은 Isabelle/HOL, HOL4, Lean, Agda 순이었다. 증명 조작은 Agda, Lean, HOL4, Isabelle/HOL 순으로 평가했다. 즐거움은 HOL4, Lean, Isabelle/HOL, Agda 순이었고, 짜증 요인은 Agda가 가장 낮은 점수, 즉 가장 큰 불편으로 꼽혔다. 예상 밖의 동작으로 당황하는 정도는 HOL4, Lean, Isabelle/HOL, Agda 순으로 낮았다.
비교자는 HOL4를 종합적으로 가장 높게 평가하면서도, 익숙한 시스템이나 개인의 선호에 따라 결과가 달라질 수 있음을 밝혔다. 특정 증명기만 써 왔다면 다른 기반의 시스템도 시험해 보라고 권한다. 예를 들어 종속 타입 기반 증명기만 사용했다면 Isabelle/HOL이나 HOL4를, 상호작용형 증명기만 사용했다면 HOL4나 Agda를 살펴볼 수 있다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요