모든 글

형식검증

수학이 '버그 없음'을 보증했는데, 버그가 나왔습니다

Lean 같은 정리 증명기로 프로그램의 정확성을 수학적으로 증명했는데도 버그가 발견되는 일이 실제로 일어납니다. 형식 검증의 맹점과 AI 시대에 이것이 의미하는 바를 짚어봅니다.

형식검증 Lean 소프트웨어품질