AI 보조 형식 증명, 2027년의 진짜 질문

2027년 말까지 clang·gcc의 정확성, Linux의 메모리 오류 부재, 주요 하드웨어 회사의 칩 정확성을 형식 증명할 수 있다는 전망이 나왔다.¹ 흥미로운 지점은 예측 자체보다 그 전제다. AI가 코드를 더 잘 쓰는가가 아니라, AI가 사람이 감당하기 어려웠던 형식 증명의 비용을 낮출 수 있는가다.

형식 검증은 테스트의 더 강한 버전이 아니다

형식 검증은 어떤 명제가 참임을 컴퓨터가 자동으로 검사할 수 있는 증명으로 작성하는 일이다.² Lean은 이런 수학 증명을 쓰고 검증하는 데 자주 사용되는 언어다.²

테스트는 선택한 사례를 실행해 결과를 확인한다. 반면 형식 증명은 명시된 조건 전체에 대해 주장이 성립하는지 다룬다. 컴퓨터 프로그램도 수학적 객체로 볼 수 있기 때문에, “이 프로그램은 이런 조건에서 이런 동작을 한다”는 주장 역시 정리처럼 증명할 수 있다.²

그동안 형식 검증이 널리 쓰이지 못한 이유는 개념이 없어서가 아니었다. 기계 검증 가능한 증명은 약 60년 전부터 존재했지만, 사람이 작성하기에는 직관적이지 않고 지루한 작업이 많았다.² AI 보조 형식 증명이 주목받는 이유는 바로 이 병목을 줄일 가능성 때문이다.

AI의 역할은 ‘정답 선언’이 아니라 증명 작성 보조다

AI가 만든 답을 그대로 믿는다면 환각 문제가 남는다. 하지만 Lean 같은 증명 보조기를 통과해야 한다면 이야기가 달라진다. AI는 증명 후보를 만들고, 형식 검증기는 그 후보가 실제로 맞는지 엄격하게 검사한다. 생성과 검증의 역할이 분리되는 것이다.

최근 연구도 이런 방향의 가능성을 보여준다. LLM이 만든 증명을 Lean으로 검증하는 방식으로 공개된 Erdős 문제 353개 중 9개, OEIS 추측 492개 중 44개를 증명했다고 보고했다.³ 핵심은 AI가 수학자를 대체했다는 결론이 아니라, 반복적이고 까다로운 증명 탐색 작업을 줄일 수 있다는 신호다.

소프트웨어 보안에서는 이 변화가 더 실용적으로 다가온다. 종단 간 형식 검증은 프로토콜 설명만 검증하는 데서 멈추지 않고, 사용자가 실제 실행하는 코드의 보안 속성까지 증명하는 것을 목표로 한다.² 예를 들어 Signal의 X3DH 보안 성질을 DDH 가정으로 환원하는 Lean 정리 예시가 제시됐다.² 여기에 AES 구현의 정확성 증명과 프로토콜 보안 증명이 결합되면, 수동 공격자에 대한 Signal 암호화 보안 증명으로 이어질 수 있다.²

“증명됐다”보다 먼저 봐야 할 것들

형식 증명은 강력하지만, 모든 것을 자동으로 보장하지는 않는다. 증명은 어디까지나 명시한 명제에 대해 성립한다. 중요한 성질을 명세하지 않았다면, 증명 자체는 맞더라도 실제 시스템의 위험은 남을 수 있다.

따라서 AI 보조 형식 증명을 볼 때는 “증명됐는가”보다 다음 질문이 더 중요하다.

• 무엇을 명세했는가?

• 실제 코드의 어느 범위까지 포함했는가?

• 어떤 수학적·시스템적 가정을 두었는가?

• 증명된 성질이 사용자가 걱정하는 위험과 직접 연결되는가?

2027년 전망 역시 이 기준으로 읽어야 한다. clang·gcc, Linux, Intel·Apple·Nvidia 같은 주요 하드웨어 회사의 칩에 대한 형식 증명 예측은 대담하다.¹ 다만 그것이 실제 정확성 전체를 의미하는지, 특정 명세에 대한 정확성을 의미하는지는 구분해야 한다. 특히 명세 일부가 AI로 작성된다면, 증명이 통과했더라도 그 명세가 충분한지에 대한 판단은 별도의 문제다.¹

앞으로의 신뢰는 “코드”가 아니라 “검증 가능한 주장”으로 이동한다

AI 보조 형식 증명은 개발을 자동화하는 유행어라기보다, 신뢰를 쌓는 방식의 변화에 가깝다. 전체 코드를 사람이 모두 읽고 확신하는 대신, 어떤 성질이 어떤 가정 아래 증명됐는지 확인하는 방식이 가능해진다.²

2027년 예측이 그대로 맞을지는 알 수 없다. 그러나 방향은 분명하다. 고위험 소프트웨어와 하드웨어에서는 테스트 결과만으로 충분하지 않다는 압력이 커질 것이다. 앞으로 중요한 질문은 “AI가 만들었는가”가 아니라 “그 주장을 기계가 검증할 수 있는가”가 될 가능성이 크다.

참고

¹AI to Enable Formal Proofs for Compilers, Linux, and Chips by 2027

²A shallow dive into formal verification

³Advancing Mathematics Research with AI-Driven Formal Proof Search