프로그램이 맞다는 걸 증명하는 일은 왜 이렇게 어려운가
Why Writing Correct Software Is Hard
소프트웨어 정확성을 보장하는 일이 도구만 잘 갖추면 쉽게 해결될 수 있다는 주장에 반박하며, 계산 가능성 이론과 복잡성 이론의 결과들을 종합해 정확성의 근본적인 어려움을 설명한다. Halting theorem, Rice's theorem, Busy Beaver 함수 등은 프로그램의 행동을 완전히 이해하는 것이 원리적으로 불가능함을 보여준다. 특히 ZFC 공리계로 종료를 증명할 수 없는 1919개 상태의 Turing machine이 존재한다는 사실은 작은 프로그램조차 수학적으로 결정할 수 없음을 시사한다.
정확성의 비용은 엔트로피를 줄이는 데 드는 에너지 비용과 마찬가지로, 결코 피할 수 없는 계산의 ‘자연 법칙’의 결과다.
HN 토론
143- turbobutton
저는 소프트웨어의 추상적이고 수학적인 정확성과 실제 세계에서의 작동 사이에는 엄격한 구분이 있다고 생각합니다. 입력을 처리하고 인간에게 복잡한 워크플로를 제공하는 모든 소프트웨어는 필연적으로 현실의 끝없는 변덕스러움을 다뤄야 합니다.
형식적 정확성에 가치가 없다는 말은 아닙니다. 하지만 중요한 것은 그것이 언제 유용하고 언제 문제보다 더 큰 골칫거리가 되는지 식별하는 것입니다...
- mpweiher
먼저 '정확하다'는 것이 도대체 무엇인지부터 파악해야 한다고 생각합니다.
형식 명세에 대해 정확하다는 것인가요?
그 명세가 '정확하다'는 것은 어떻게 알 수 있나요? 정의상 그런 건가요?
- johnbender
제가 알기로는 이 기사는 라이스 정리(Rice's Theorem)를, 예디디야와 애런슨이 생성한 작은 프로그램에 대해 무언가를 증명할 수 없다는 개념과 잘못 혼동하고 있습니다. 하지만 라이스 정리가 말하는 것은 그게 아닙니다. 대신, 라이스 정리는 모든 프로그램에 대해 프로그램이 주어진 지점에 도달하는지 여부를 예/아니오로 올바르게 결정하는 일반적인 방법을 고안할 수 없다는 것을 말합니다.
특정 프로그램과 일회성 증명의 경우, 많은 것을 증명할 수 있습니다. 또는 루프가 종료된다고 가정하여 과대 근사하면, 때때로 올바른 프로그램을 거부할 위험을 감수하면서도 많은 것을 건전하게 증명할 수 있습니다(예: 타입 시스템).
다만 이는 언어의 특성이나 제 해석의 문제였을 수도 있습니다.
- kodoman
저는 항상 형식 검증에 관심이 있었지만 장난감 수준의 증명과 유도된 프로그램만 작성해 왔습니다.
'AI가 Lean을 한다'는 논의나, 형식 검증이 쉽거나 AI에게 쉬울 것이며 그저 뇌를 꺼버리면 된다는 가정 밖에서 이 주제에 대한 오래된 논의를 보니 좋네요.
애초에 검증 가능한 프로그램을 구축하는 것은 진정한 사고와 문제에 대한 깊은 통찰을 요구하는 어려운 설계 문제입니다.
- tromp
> 종료를 증명할 수 없는(즉, 'ZFC로부터 독립적인') 1919개의 제어 상태를 가진 튜링 기계. 이 기계는 너무 작아서 4K 챌린지에 편안히 들어갑니다.
작은 지적 하나:
4K 챌린지는 보통 4KB에 들어가는 코드를 말하지만, 1919 상태 TM을 단순하게 인코딩하면 19192(2+11) = 49894 비트, 즉 6237 바이트로 6KB를 넘습니다.
최근 AI 기반 최적화로 상태 수가 최대 215개로 줄어들었고, 이는 1KB에 편안히 들어갑니다...
- nirinor
부정적 주장에서 가장 중요한 부분은 암묵적입니다: 어떤 합리적인 가정이 그 주장을 무효화할 수 있을까요?
물론 라이스 정리에 따르면, 어떤 프로그램도 임의의 함수가 항상 두 입력의 합을 계산하는지 결정할 수 없습니다. 하지만 그것은 우리가 합 함수의 분석하기 임의로 어려운 구현을 허용하기 때문입니다. 따라서 이 정리는 합의 단순한 구현이 올바르다는 것을 증명할 수 있다는 사실과 공존합니다.
이런 관점에서 가장 좋은 결론은 "합리적인 시간 내에 올바른 소프트웨어를 작성하려면 분석하기 쉬운 언어와 프로그래밍 스타일을 사용해야 한다"는 것입니다.
- bluGill
진짜 질문은 이것입니다: 증명할 수 없는 프로그램이 있다는 것을 알면서도, 일반적인 프로그램에 대해 증명할 수 있는가?
저는 제시된 예시에는 관심 없고, 제 워드 프로세서, 웹 브라우저 같은 것에 관심이 있습니다. 스크립팅 언어에 제한을 두고 그것들을 증명할 수 있을까요?
- myrmidon
BB(6) 챔피언(2-심볼 6-상태 바쁜 비버)의 하한이 기사의 연대를 보여준다는 점이 흥미로웠습니다. 기사에서는 >10^36534를 제시하지만, 현재 챔피언(mxdys 2025)은 >10↑↑10↑↑10↑↑8입니다(10↑↑8은 10^10^10^10... 8단 높이의 거듭제곱 탑이고, 식은 오른쪽에서 왼쪽으로 계산되므로 10↑↑10↑↑8은 이미 완전히 상상할 수 없을 만큼 큽니다).