잘 아는 분야는 아니지만, 그냥 생각나서 다소 무책임하게 썰을 풀어봅니다.

깊게 파보진 않았지만, 온라인에서 흘려들은 뉴스들 중에 관심을 끄는 것이 두 가지 있었습니다.

하나는, 새로운 버전의 클로드가 소프트웨어들의 버그를 엄청난 속도로 찾아낼 수 있는 능력이 있다는 것. 이게 아직까지는 심각한 단계까지는 아니라는 이야기도 있습니다만, 언젠가는 이것이 정말로 현실적인 위협이 될 날이 그리 멀지 않았다는 것은 분명해 보입니다. 제로데이 버그들이 무한정 발견되는 상황이면, 그게 죄다 패치되고 이런 문제가 더 생기지 않는 정말로 안전한 소프트웨어 공학적 방법론이 자리잡기 전에는 보안은 물건너 가는 거죠.

다른 하나는, LLM이 이제 어느 정도 자명하지 않은 수학적 증명을 할 능력이 있다는 것. 아직은 초기단계이긴 하지만, 미해결 문제를 새로운 접근 방식으로 공략해서 성공시킨 결과들이 나오기 시작하는 것 같습니다. 얼마 전까지만 해도 그냥 올림피아드 문제 정도 푸는 수준이었는데, 이제 연구 수준의 결과도 낼 수 있는 단계가 되려는 모양입니다.

그렇다면, 이 시점에서 소프트웨어 보안을 확보할 수 있는 현실적인 방법으로, 형식 검증을 진지하게 고려해야 하지 않나 싶습니다. 형식 검증(formal verification)이란, 코드를 작성할 때 그냥 코드를 작성할 뿐만 아니라, 그 코드의 입력이 이러이러한 조건을 만족하면 그 코드의 출력은 저러저러한 조건을 반드시 만족한다라는 것의 증명 자체를 컴퓨터 언어로 작성하고 (수학적 팩트를 코딩할 수 있는, 표현력이 좋은 특별한 언어들이 동원됩니다. 대표적으로는 Lean이나 Coq 등...), 컴파일 시에 그 증명이 맞는지를 함께 컴퓨터가 검증하는 것을 말합니다. 이런 과정을 거친 코드는, 말하자면 버그가 없다는 것이 증명된 코드이므로, 공격당하지 않습니다.

형식 검증이 좋기는 한데, 우리가 사용하는 소프트웨어는 버그가 가득하고, 사실 모두들 이 상황에 익숙해져 있습니다. 그러한 이유는 대강 두 가지 정도가 있지 않나 싶습니다.

첫번째: 증명을 위해서는 정확한 스펙이 필요합니다. 즉, 이 코드는 정확히 이런 일을 해야 하고, 그를 위해 입력은 이런 전제를 만족해야 하고, 그러면 출력은 저런 성질을 만족해야 한다는 규칙이 정확히 정해져 있어야 합니다. 그러한 정교한 스펙의 기술이 가능한 소프트웨어도 있을 수 있지만, 또한 많은 소프트웨어는 그렇게 수학적인 정교한 요구조건의 기술이 어려울 수 있습니다. 현실 세계는 애매하고, 소프트웨어는 현실 세계에서 돌아야 하니까요. 그리고, 고객님도 정확히 고객님이 뭘 원하는지 모르십니다. 그러니, 어쩌면 모든 코드를 형식 검증의 대상으로 삼는 것은 영원히 불가능할지도 모르겠습니다.

두번째: 증명은 어렵습니다. 형식적 증명은 더 어렵습니다. 그리고 노동력이 많이 필요합니다. 코딩 자체가 노동력이 많이 필요한 작업입니다. 증명을 코딩하는 것은 그 코드 자체를 코딩하는 것 이상으로 피곤한 일입니다. 그러니, 모든 곳에서 형식 검증을 요구하는 것은 현실적으로 무리였습니다. 그러다 보니, 학계가 아닌 현실 세계의 형식 검증은 정말 절대로 버그가 생기면 안 되는 핵심적인 분야로 한정되는 경향이 있었다고 알고 있습니다.

그렇긴 한데, 지금은 코딩의 방법론 자체가 바뀌고 있는 시점입니다. 이전까지는 코딩이란 기본적으로 수작업이었는데, 이제는 컴퓨터가 알아서 하고, 인간은 감독하는 작업으로 바뀌고 있습니다. 그리고 AI의 코딩 능력은 점점 더 향상될 것이고, 사람의 개입은 갈수록 줄어들어도 될 것입니다.

그렇다면, 머지 않아 형식 검증을 위한 증명의 코딩 또한 컴퓨터가 알아서 하는 것도 충분히 가능한 시대가 올 것입니다. 사실 수학 자체에서도 형식 검증이 가능합니다. 이 경우 어려운 점 중 하나는, 아직까지는 그러한 형식 체계가 형식 검증된 고등 수학에 대한 '지식'이 많이 부족하다는 것이었습니다. 즉, 예를 들어 수학과 대학원생이면 알 만한 수학적 지식들이 형식 검증을 마친 상태로 구축되어 있어야, 그러한 '이미 다들 아는 결과들'을 매번 다시 증명하지 않고 다음 단계의 연구에 활용할 수 있을 것입니다. 말하자면, 일종의 소프트웨어 라이브러리 구축과 비슷한 일을 수학적 증명에 대해 해야 합니다. 수학이, 소프트웨어 공학적인 문제들을 고민해야 하는 시점이 되었습니다. 유지보수 용이성, 확장성, 리팩토링, 캡슐화, 뭐 이런 소프트웨어 공학의 상식적인 문제들이, 수학의 형식 검증에서 정확히 고민해야 하는 문제들이 됩니다.

하지만 역시 이는 노동력이 많이 필요한 일이고, 얼마 전까지만 해도 사람들이 일일이 손으로 이런 라이브러리 구축을 해왔습니다. 근데 얼마 전에 역시 인터넷에서 얼핏 본 바에 따르면, 위상수학 교과서로 유명한 Munkres의 Topology 책의 결과들을 어떤 사람이 그냥 자기 컴퓨터에서 AI 돌려서 한두달 만에 거의 다 형식화할 수 있었다고 합니다. 사람이 손으로 하기에는 매우 힘든 작업인데, 이제 이 정도는 컴퓨터가 할 수 있는 것 같습니다. 새로운 영감이 필요한 수학적 발견을 하는 것에 비해, 이미 사람의 언어로 작성된 수학적 증명을 형식 증명으로 '번역'하는 것은 최소한 더 쉬운 일이고, 이제 이 정도는 AI가 잘 하는 모양입니다.

대충 이런 분위기라면, 비록 형식 검증이라는 방법론이 여태까지는 노동력이 워낙 많이 들다 보니, 학계에서야 진지하게 연구되기는 하지만 학계를 벗어나 현실에서 널리 사용되지는 않았었는데, 어쩌면 그게 충분히 가능해질 지도 모르겠습니다. 그리고, 이 방법의 좋은 점은, AI의 환각으로부터 자유롭다는 것입니다. 증명은, 일단 만들어지면, 객관적으로 검증될 수 있습니다. AI가 환각을 일으키든 실수를 하든, 뭔가 실수가 있으면 실수가 있다는 것이 객관적으로 드러납니다. 올바른 증명이 만들어지면, 역시 증명이 되었고 실수가 없다는 사실이 판명됩니다.

소프트웨어의 모든 부분을 형식 검증을 거치지 않는다 하더라도, 정말 어려운 부분만 남기고 상당수의 코드를 형식 검증을 거치게 작성하는 것이 가능한 시대가 온다면, 최소한 '공격 표면(attack surface)'를 최대한 줄이는 효과를 얻을 수는 있을 겁니다. 어쩌면 이게 소프트웨어 보안에 대한 AI의 위협을 막는 현실적인 방법이 될 수 있지 않을까요.