미스트랄(Mistral)이 형식적 수학 증명으로 코드를 검증하는 모델 린스트랄 1.5(Leanstral 1.5)를 출시했다. 증명 언어 린 4(Lean 4)로 작성된 증명을 자동으로 생성하고 확인한다. 테스트 통과만으로는 안심할 수 없는 안전 필수(safety-critical) 소프트웨어가 대상이다.

기존 코드 리뷰 방식은 테스트를 통과했으니 코드가 대체로 작동할 것이라고 추정한다. 형식 검증(formal verification)은 다르다. 코드의 속성 자체를 수학적으로 증명한다. 이는 항공, 의료기기, 암호 시스템에서 요구하는 방식이다. 미스트랄은 이 증명 생성과 검증을 자동으로 처리한다고 설명했다.

이제 세계 신규 코드의 상당 부분을 AI가 작성한다. 문제는 AI가 만든 코드에 같은 맹점을 공유하는 AI 생성 테스트가 함께 붙는다는 점이다. 형식 검증은 누가 코드를 짰는지 따지지 않는 유일한 품질 기준이다. 다만 손이 많이 가는 작업이어서 그동안 항공우주급 예산에서나 감당할 수 있었다. 모델이 린 4 증명을 저렴하게 만들어낸다면, 검증된 소프트웨어가 더 이상 사치재가 아니게 된다.

이달 초 처음부터 끝까지 자동으로 작동한 AI 랜섬웨어가 보고되면서, AI가 쓴 코드를 사람이 일일이 확인하기 어려운 현실이 드러났다. 코드가 스스로를 수학적으로 증명하는 방식은 이런 위험에 대한 직접적인 대응이 된다.

미스트랄은 이러한 방식의 서비스 출시를 꾸준히 이어 왔다. 지난주에는 카메라 한 대로 로봇을 안내하는 모델을 선보이기도 했다. 대형 연구소들이 곁가지로 취급하는 어렵고 눈에 안 띄는 기능을 골라 자기 것으로 만드는 방법이다. 컴퓨팅 규모로는 이기기 어려운 프런티어 경쟁 대신, 좁지만 방어 가능한 기술 제품을 차곡차곡 쌓고 있다. 이번 출시도 같은 전략을 공유한다. 2군 연구소 가운데 가장 일관된 전략이라는 평가가 나온다.

자세한 내용은 빌드패스트위드AI(Build Fast with AI)에서 확인할 수 있다.

이미지 출처: 미스트랄