형식 철학과 증명 보조기

형식 철학

• 전통적인 철학 문제를 연구하고자 수학의 엄밀한 도구에 의지하는 연구 전통. (Dolgorukov and Shumilina 2021, 235)
• 논리학, 수학, 컴퓨터 과학, 언어학, 물리학, 생물학, 경제학, 게임 이론, 정치론, 심리학 등의 연구 방법을 활용함.

형식 철학의 주제

• 논리학: 비단조 논리, 양상 논리 등
• 형식 인식론: 인식 논리, 신념 변화, 베이즈 인식론 등
• 계산 형이상학: Computational Metaphysics
• 추상적 대상 이론: GitHub - ekpyron/AOT: Embedding of The Theory of Abstract Objects in Isabelle/HOL
• 과학 철학: 과학 이론 발전에 대한 모형, 일반 상대성 이론이 허용하는 가능 세계의 성질 (Hansson and Hendricks 2018, chap. 26)
• 가치론과 도덕 철학: 가치론, 선호와 선택, 선호 변화, 규범 논리
• 결정 이론과 사회 철학: 동적 결정 이론, 인과 결정 이론, 사회 선택 이론

증명 보조기를 철학 연구에 활용할 수 있는가

이저벨 증명 보조기의 활용 사례

이저벨(Isabelle) 증명 보조기로 다음 이론이 형식화됐습니다.

• 신 존재 증명
• 추상적 대상 이론
• 포괄적 일관성 원리
• 아리스토텔레스의 주장적 삼단 논법
• 부분 전체론
• 조지 불로스(George Boolos)의 기묘한 추론
• 조건부 규범 추리

'기존 철학'을 연구하는 데 활용할 수 있는가

"증명 보조기가 기존 철학의 연구에 활용될 수 있는가?"라는 물음의 답은 어디부터 어디까지가 '기존 철학'의 범위에 들어가는지에 따라 달라질 듯합니다. 하지만 세계에 널리 알려진 중요한 철학 이론 중에서 많은 것이 형식화하기 어려워 보인다고 저는 생각합니다. 형식화하기 어려운 이론은 증명 보조기로 재서술하기도 어렵습니다.

제가 보건대, 그런 철학 이론에서 영감을 받아 새로운 형식 철학 이론을 만드는 편이 차라리 더 쉬울 듯해요. 물론 이것도 그리 쉬운 일이 절대 아닙니다. 해당 철학 분야를 잘 이해해야 할 뿐만 아니라 증명 보조기를 잘 다룰 수 있어야 하니까요. 저는 "린 4로 하는 정리 증명"과 린 라이브러리의 몇몇 코드를 읽는 데 대략 373시간을 들였어요. 제가 원래 학습 속도가 느린 편이긴 하지만요.

참고 문헌

• Dolgorukov, Vitaly V., and Vera A. Shumilina. 2021. “What Is Formal Philosophy?” Epistemology & Philosophy of Science 58, no. 1. https://www.pdcnet.org/eps/content/eps_2021_0058_0001_0235_0241.
• Hansson, Sven Ove, and Vincent F. Hendricks, ed. 2018. Introduction to formal philosophy. New York: Springer. https://doi.org/10.1007/978-3-319-77434-3.

글 잘 읽어보았습니다. 저도 철학적 물음을 해결하기 위해 수학이나 컴퓨터를 도구로서 활용하는 것에 관심이 있는데요. 제가 알기로는 증명 보조기는 연역 논증의 타당성을 검증하는 데 도움을 주는 것으로 알고 있습니다. 그렇다면,

(1) 귀납 논증을 중점적으로 활용하는 철학에서 증명 보조기가 그 힘을 발휘할 수 있을까요?
(2) 연역 논증을 검증하기 위해 증명 보조기를 활용한다면, 굳이 증명 보조기가 없어도 사람의 이성만으로 그 타당성을 보일 수 있지 않을까요? 증명 보조기를 활용하기 위해서는 쉽지 않은 코드 작성이 필요한데, 이것이 사람이 직접 검증하는 것에 비해 수고를 더 들여도 가치 있을만한 활동인지 의문이 드네요.

"형식 철학 입문" 학부 교과서의 5장 '귀납'을 보니, 귀납 논증에 관한 이론은 증명 보조기로 서술할 수 있을 듯합니다. (Hansson and Hendricks 2018, chap. 5)

사람의 이성만으로 그 논증의 타당성을 보일 수는 있습니다. 그런데 사람의 착오가 문제입니다. 사람은 정의를 잘못 내리고, 정리를 잘못 진술하고, 정리를 증명하면서 오류를 범합니다. 증명 보조기를 활용하면 증명 안의 오류를 제거할 수 있습니다. 가끔 증명 보조기의 신뢰성 문제가 생기기는 하지만, 증명 보조기는 사람보다 더 믿을 만합니다.

저는 증명 보조기를 쓸 줄 알기 전에도 자꾸 수학 증명을 형식적으로 쓰려고 해서 고생했습니다. 이런 경우에는 증명 보조기를 쓰는 편이 고생을 훨씬 덜어 줍니다. 현재 대부분의 수학 전공자는 지나치게 엄밀하게 수학 증명을 작성하지 말라고 조언하겠지만요. 저는 형식 증명을 읽고 쓸 때 이론을 더 잘 이해한다고 느꼈습니다.

어떤 이론을 만든 사람이 증명 보조기로 그 이론을 이미 검증하면, 그 사람을 뺀 나머지 모두는 고생을 덜 하게 됩니다. 그 이론을 검토하고 싶은 사람들은 정의와 정리 진술이 올바른지만 확인해도 되니까요. 증명 보조기가 검증한 증명이 실제로 틀릴 가능성은 작습니다.

어떻게 해야 증명 검증기를 신뢰할 수 있는지는 마리오 카네이로 박사 후 연구원님이 자신의 박사 논문 도입부에서 설명하셨습니다.

증명 보조기를 활용해 자신의 이론을 아주 엄밀하게 검증하다 보면 새로운 깨달음을 얻기도 합니다. 예를 들어, 저는 린 표준 라이브러리의 문자열 정리 String.splitOn_of_valid를 증명하려고 여러 보조 정리를 만들다가 String.splitOn 함수를 정의하는 새로운 방법을 생각해 냈어요. 제가 만든 보조 정리가 사실상 제게 새 정의를 알려 준 셈이었습니다.

기호 논리에 관심이 있어서 이제 막 공부를 시작한 일반인 입니다. 이맥스 텍스트 편집기를 애용하다 보니 기호 논리를 코드로 학습하는 게 여러모로 재미있을 것 같아서 찾아보다 LEAN을 알게 되었습니다. 관련 언어가 많이 있는데 LEAN을 선택하신 이유가 궁금합니다.

간단한게 AI 한테 물어보니 아래와 같이 대답해주는군요. 저도 Coq는 (컴공과에서) 들어봤습니다.

정확한 점유율 정보는 명시되기 어렵지만 Coq와 Lean이 비교적 널리 사용되며, Isabelle/HOL도 많은 사용자가 있는 편입니다.

LEAN의 장단점:

장점:

1. 직관적 문법:

   • Lean은 비교적 친숙한 문법을 사용하여 사용자가 쉽게 익힐 수 있습니다.

2. 강력한 자동화:

   • Lean은 다양한 자동화 도구를 제공하여 증명을 더 효율적으로 할 수 있도록 도와줍니다.

3. 활발한 커뮤니티:

   • Lean의 사용자 커뮤니티가 활발하여 정보와 자료를 쉽게 찾을 수 있습니다.

4. 호환성:

   • 다양한 수학 라이브러리와 통합되어 있어 수학 증명을 직관적으로 할 수 있습니다.

5. 표현력:

   • 강력한 타입 시스템과 추상화를 통해 복잡한 개념도 깔끔하게 표현할 수 있습니다.

단점:

1. 학습 곡선:

   • 처음 Lean을 접할 때 타입 이론과 프레임워크를 이해하는 데 시간이 걸릴 수 있습니다.

2. 한정된 문서와 자료:

   • 다른 오래된 proof assistant 언어들에 비해 문서나 자료가 덜 풍부할 수 있습니다.

3. 실행 속도:

   • 복잡한 증명을 수행할 때 실행 속도가 느려질 수 있습니다.

4. 관용성 부족:

   • 특화된 구조나 컨벤션이 있어 이를 따르지 않으면 코드 작성에 어려움을 느낄 수 있습니다.

아, 저도 지난해 여름부터 둠 이맥스를 쓰고 있어요. 수학 기초론 밖의 수학 분야를 연구하는 수학자들이 현재 가장 활발히 이용하고 있는 증명 보조기가 린이라고 생각해서 저는 린을 골랐습니다. 현재로서는 사람들이 린을 이용할 가장 큰 동기가 린의 수학 라이브러리인 매스리브(Mathlib)뿐인 듯해요.

인공 지능의 대답을 검토해 보자면, 린은 구문이 깔끔한 편이고 커뮤니티가 활발하지만, 자동화 도구와 공식 문서가 아직은 부족합니다. 이 두 가지는 앞으로 개선될 여지가 있어요.

그런데 제가 요즘 린 핵심[코어] 개발진에 대한 불만이 쌓이고 있기 때문에, 린보다는 그 밖의 증명 보조기 중 하나를 더 자주 이용할 계획입니다.

제 불만은 다음과 같습니다. 린 핵심 개발진이 린의 개발 방향을 확정하기 전에 린 커뮤니티에 속한 다른 인원들이 자신의 의견을 핵심 개발진에게 전달할 방법이 없습니다. 따라서 린의 개발에 관한 논의는 린 핵심 개발진 내부에서만 일어납니다. 개발진 외부에서 일어나는 것은 논의가 아니라 반응입니다. 핵심 개발진은 이미 결정을 다 내린 상태에서 그 결정을 린 커뮤니티에 통보할 뿐이고, 그 통보도 그리 자세하거나 빠르지 않습니다.

Mario Carneiro said:

I was indeed notified that some tactics were going to move, not really in a way which invited discussion but more of a "heads up this is happening". I have to admit that the scale turned out to be much bigger than I expected and now there isn't much left within the original purview of Std from what I can tell. Most of the things on Joe's original Std roadmap are now in an uncertain position and I don't know what will remain. Perhaps future announcements will clarify matters here, but I certainly haven't gotten the impression that I have any say over the contents of those announcements.

위의 인용문에서 언급된 일은 올해 4월쯤에 있었습니다. 다음 인용문은 어제 제가 통보받은 내용에 대한 제 반응입니다.

Bulhwi Cha said:

Kim Morrison said:

There will be more news coming about this later, and when a design document is available we will post it, but it is possible there will be a radical overhaul of the String library (indeed, even the definition of String), so I would hesitate to encourage significant work on String at the moment as it may become obsolete (even to the point of not being able to meaningfully migrate results).

I'm glad that there may be a substantial overhaul of definitions and theorems about strings in the future. But it also means that I don't have to prove the ten specification theorems and review Batteries#809.

지난 4월에 제가 서강올빼미에 게시한 글 '어떤 오류가 사소한 실수인가'에서도 밝혔다시피, 문자열 연산 String.splitOn의 명세에 관한 정리 String.splitOn_of_valid를 제가 증명하는 데 170시간 정도가 걸렸습니다. 이 증명을 린 배터리(Batteries, 옛 표준 라이브러리) 관리자가 검토하기를 제가 두 달 동안 기다리고 있었는데, 린 핵심 개발진이 문자열에 관한 라이브러리를 미래에 대폭 수정할 수 있다는 소식을 어제 제게 알렸습니다.

현재 몇몇 문자열 연산은 그에 관한 정리를 작성하기가 어렵게 정의돼 있다고 제가 이전에 린 줄립 챗에서 밝힌 바 있기 때문에 저도 이 변화를 환영합니다. 하지만 이제 제가 고생해서 작성한 증명은 검토받지도 못하게 됐어요. 문자열 연산의 정의가 크게 바뀔수록 그에 관한 정리의 증명도 크게 바뀔 수 있기 때문입니다.

제 증명이 쓸모없어질 가능성이 꽤 커졌다는 사실은 저도 받아들일 수 있어요. 하지만 문자열에 관한 라이브러리를 대규모로 재정비할지를 린 핵심 개발진이 논의했을 동안 저는 그 논의에 참여할 수 없었다는 점이 불만스럽습니다. 그분들이 어떤 결정을 내리기 전에 일반 린 이용자들의 의견을 들어 보기만 해도 좋았을 것입니다.

공개 소스 소프트웨어의 관리자가 어떤 결정을 내리기 전에 이용자의 의견을 듣지 않아도 되기는 합니다. 관리자는 자신이 원하는 대로 소프트웨어를 개발할 수 있어요. 그 대신에 이용자는 그 소프트웨어의 대용품을 찾든가 그것을 분할[포크]해서 자신만의 버전을 개발할 수 있습니다.

제가 매스리브를 참고해 수학을 형식화하고 싶기 때문에 린을 그만 이용할 수는 없지만, 앞으로는 메타매스 제로(논문 링크) 검증 시스템과 다프니(Dafny) 프로그래밍 언어를 다루는 데 시간을 더 들이려고 합니다.