어떤 오류가 사소한 실수인가

요약

1. 어떤 정의나 증명에 있는 오류가 고치기 쉽더라도 알아차리기 어렵다면, 그 실수는 사소하지 않습니다.
2. 어떤 오류는 증명 보조기의 도움을 받아야 찾아낼 수 있습니다.
3. 미래에 제가 수학적 개념을 새로 정의할 때는 증명 보조기로 그 개념의 주요 성질을 꼭 증명할 것입니다.

본문

지난해에 린(Lean) 정리 증명기의 수학 라이브러리 매스리브(Mathlib)를 린 3에서 린 4로 포팅[이식] 하는 작업에 저도 조금 참여했는데, 어쩌다 보니 제가 린 표준 라이브러리 Std에 있는 문자열 보조 정리 파일의 공저자가 됐습니다.

마리오 카네이로(Mario Carneiro) 박사 후 연구원님이 이 파일에 많은 보조 정리를 추가하셨고, 그중 열한 가지에는 진술과 증명 없이 "TODO(나중에 할 일)"라는 주석만 달렸습니다. 이 정리들을 증명하고자 할 사람은 저와 카네이로 연구원님 말고는 없을 테고, 카네이로 연구원님은 늘 바쁘시니 결국 제가 지난해 12월부터 작업을 시작했습니다.

첫째 문자열 정리 String.splitOn_of_valid는 문자열 연산 String.splitOn의 명세를 밝히기 위한 보조 정리입니다. 이 함수는 주어진 문자열에서 특정 부분이 나올 때마다 그 문자열을 가릅니다. 그 특정 부분을 제외한, 갈라진 문자열 조각들의 목록이 원래의 문자열에 대한 함숫값입니다.

예를 들어, 문자열 "abcabc"에서 "bc"가 나올 때마다 그 문자열을 가른 결과는 "a", "a", ""입니다. splitOn 함수는 이 조각들의 목록인 ["a", "a", ""]을 산출합니다.

이 첫째 문자열 정리를 증명하는 데 170시간 정도가 걸릴 줄은 저도 전혀 예상하지 못했습니다. 지난해 12월에 증명을 작성하기 시작해서 올해 4월 16일에 완성했습니다. 아쉽게도, 170시간 가운데 67시간 정도는 제가 정리를 잘못 진술해서 헛고생했습니다. 올해 1월 3일에 마리오 카네이로 연구원님의 도움을 받아 제대로 된 진술을 작성할 수 있었고, 그 뒤로 93시간 정도 증명을 시도한 결과 splitOn 함수의 정의에 버그가 있다는 사실을 깨달았습니다. 카네이로 연구원님이 버그를 고치신 뒤에 제가 증명을 완성하는 데는 10시간 남짓 걸렸습니다.

저는 이 오류가 너무 섬뜩했어요. splitOn 함수는 대개 똑바로 작동했기 때문입니다. 그래서 정리 splitOn_of_valid를 증명하려고 시도할 때마다 증명의 대부분은 작성할 수 있었지만, 마지막 경우의 부분 증명은 자꾸 실패했습니다. 나중에야 특정 부분 증명의 목표가 거짓인 것 같다는 생각이 들었습니다. 제가 진술한 정리는 참이라는 확신이 있었기 때문에 splitOn 함수의 정의가 잘못됐을 수도 있다는 의심을 품었죠.

digama0 said:

The code change here is very small, replacing a i with i - j, but it makes termination more complex so that's where the rest of the line count goes.

이 버그를 고치는 일은 그리 어렵지 않았습니다. 해당 정의에서 i를 i - j로 바꾸기만 하면 됐어요. 그렇다고 해서 이 오류가 사소한 실수였다고 생각하지는 않습니다. 이 정의에 따르면 splitOn 함수가 대개 올바로 작동하지만, 특수한 경우에는 잘못된 결과를 산출하니까요.

린 같은 증명 보조기를 이용하지 않았다면, 이렇게 미묘한 오류를 저는 절대로 못 찾아냈을 것입니다. 린으로 어떤 함수를 정의하고 나서 그 함수의 성질을 형식적으로 증명할 수 있었기 때문에 그 정의가 정확한지를 제가 판단할 수 있었습니다. 덧붙여 말하면, 마우리치오 콜라레스(Maurício Collares) 님이 splitOn 함수의 이런 작동 방식을 지난해 6월에 이미 알고 있었지만, 그분은 이 작동 방식을 버그라고 생각하지 않았어요.

미래에 제가 수학 이론을 본격적으로 형식화할 때는 이번처럼 정의상의 오류를 또 발견할 가능성이 작을 듯합니다. 수학자들은 보통 어떤 개념을 정의하고 나서 그 개념의 주요 성질을 증명하기 때문이죠. 하지만 저는 새로운 수학적 개념을 정의할 때마다 꼭 증명 보조기를 이용해 그 개념에 대한 여러 보조 정리를 증명할 것입니다. 미묘하지만 사소하지 않은 실수를 제가 저질렀을 때, 제 주변의 수학 전공자보다 증명 보조기가 제 실수를 더 뚜렷이 드러낼 테니까요.

재밌는 논제인 것 같아요. 수정하기 쉬운 오류보다 알아차리기 어려운 오류가 보다 사소하지 않은 오류라는 것인데… 제가 전혀 모르는 분야라 무식한 질문을 좀 해보자면 그 증명 보조기는 형식적인 오류를 다 잡아내는 건가요?
갑자기 잠이 안 와 누워서 생각해본 건데,
만일 완벽한 증명 보조기라는 것이 있어서 그것이 모든 형식적인 오류를 잡아낼 수 있다면, 그리고 알아차리기 어렵다는 개념이 순전히 주관적인 것이 아니라면 이것은 해당 코드가 오답을 내는 경우의 수가 상대적으로 적을 때를 뜻할까요, 아니면 다른 코드와의 연계(?)성이 큰 것이어야 할까요? 아마 두 가지 다 중요하니 둘을 곱한 값이어야 할까요? 그러니까 오류없는 결과값을 도출하는 경우의 수를 오류 결과값을 도출하는 경우의 수로 나누고 여기에 다른 코드와의 연계성(그런 게 있다 친다면)을 곱해주면 아마 작성자님이 느끼신 섬뜩함의 정도를 구할 수 있지 않을까요? ㅋㅋ

증명의 오류는 증명 보조기가 알아서 다 잡아냅니다. 증명 보조기를 얼마나 믿을 수 있냐는 문제가 있긴 하지만요. 그런데 정의는 애초에 사람이 자기가 원하는 대로 내리는 것이기 때문에, 무엇이 '올바른' 정의인지는 결국 사람이 판단해야 합니다.

정의상의 오류는 보통 사람이 자신이 의도한 바와 다르게 정의를 내릴 때 생깁니다.

어떤 함수가 대개 잘못된 결과를 낸다면 그 함수의 정의에 오류가 있음을 쉽게 알아차릴 수 있겠죠. 그리고 그 함수가 다른 코드에 자주 쓰인다면 거기서 정의상의 오류를 찾아낼 가능성이 큽니다. 바꿔 말하면, 그 함수가 특수한 경우에만 잘못된 결과를 내거나 그 함수가 쓰인 적이 별로 없을수록 거기서 정의상의 오류를 찾을 가능성이 작아집니다.

실무에 적합한 기준을 하나 더 제안해 보자면, 해당 오류가 발견돼서 고쳐지기까지 소스 코드나 원문에 머물러 있던 기간으로 그 오류의 발견 난이도를 대략 측정할 수 있겠군요. String.splitOnAux 함수가 처음 정의된 시기를 확인해 보니 2019년 3월 23일입니다. 이 오류가 고쳐지기까지 거의 5년이 걸렸네요.

물론 문자열 연산에 관한 린 소스 코드를 열심히 들여다보는 사람이나 린으로 프로그래밍을 하는 사람이 너무 적어서 이 오류가 뒤늦게 고쳐졌다고 볼 필요도 있습니다. String.splitOn 함수는 수학을 형식화할 때보다는 함수형 프로그래밍을 할 때 더 자주 쓰일 거예요.

@alektryon 님이 든 두 가지 요인과 제가 추가한 것 하나 말고도 고려해야 할 요인이 아마 또 있을 듯해요. 그리고 저 함수가 정확한 값을 내는 경우와 잘못된 값을 내는 경우 모두 무한히 많습니다. 그래서 '오류 발견 난이도'를 어떻게 정량화할 수 있을지는 저도 잘 모르겠네요. 이건 아마 확률론과 관련 있지 않을까요?

하긴 무한히 많겠네요 ㅋㅋ
어떤 이론이 자주 쓰이거나 적용되는 영역을 설정하는 건 아무래도 아직은 인간일테니.. 수학적인 기준을 세울 수 있는 논리가 있을지 궁금하네요.
예컨대 뉴턴 역학이 이론상 무한히 많은 오류를 도출하겠지만 자동차 차 사고 역학 계산 때는 오류가 거의 없이 답을 낼 수 있자나요?
뉴턴 역학을 차 사고에만 쓰고 항성 간 운동에는 쓰지말자는 등의 영역 설정에 대한 판단이 가능케 되는 논리가 궁금해지네요. 어디까지 대머리인가 하는 문제와도 일맥 상통하는 걸까요? ㅋㅋ 이런 건 확률론으로 접근해야 하는 건가.. 여하튼 공상에 정성스럽게 답해주셔서 감사합니다. :)

시간이 괜찮으시다면, <증명보조기>가 정확히 무엇이고 또 어떤 방식으로 굴러가는지, 대표적인 보조기가 무엇이고 또 그것이 기존 철학에 기여할 수 있는 것이 무엇인지 한번 글을 통해 듣고 싶습니다.
딴죽을 거는게 아니라, 저는 글쓴이 님이 올리시는 글들을 보기 전에 <증명보조기>라는게 있는지도 모르고 살았습니다. 저 뿐만 아니라 일반적인 방식으로 철학을 쭉 공부하신 분들에겐 생소한 것이라는 생각이 듭니다. 한번 얘기를 들어보고 싶습니다.

네, 나중에 새 글을 써서 증명 보조기의 작동 원리와 이것이 철학 연구에 어떻게 이바지할 수 있는지를 더 자세히 설명하겠습니다.