AI가 수학 증명을 대신 짜준다고요?
요즘 AI가 코드 짜주는 건 다들 익숙하죠. 그런데 이번에 미스트랄(Mistral)이 내놓은 소식은 결이 좀 달라요. 'Leanstral 1.5'라는 모델을 공개했는데, 이건 코드가 아니라 수학 증명(proof)을 자동으로 만들어주는 데 특화된 AI거든요. 이름부터가 힌트예요. 'Lean'이라는 도구에다 미스트랄 이름을 합친 거니까요.
여기서 잠깐, Lean이 뭐냐면요. 우리가 학교에서 '이 명제가 참이다'를 손으로 증명하잖아요. 근데 사람이 쓴 증명은 중간에 살짝 논리 비약이 있어도 검토하는 사람이 놓치기 쉬워요. Lean은 이런 증명을 컴퓨터가 한 줄도 빠짐없이 검사할 수 있는 형식(형식 증명, formal proof)으로 쓰게 해주는 프로그래밍 언어이자 도구예요. 논리가 한 군데라도 어긋나면 코드 컴파일 에러처럼 딱 걸리거든요. 그래서 'Lean이 통과시켰다 = 이건 진짜 100% 맞다'가 되는 거예요.
그럼 뭐가 문제였길래
좋은 도구인데 왜 다들 안 썼을까요? Lean으로 증명 하나 짜는 게 정말 손이 많이 가고 어렵거든요. 사람 머릿속에선 '당연히 그렇지' 싶은 단계도 기계한테는 하나하나 다 증명해서 먹여줘야 해요. 수학자나 전공자가 아니면 접근하기가 부담스러웠죠.
Leanstral이 노리는 지점이 바로 여기예요. 슬로건이 'Proof Abundance for All', 우리말로 하면 '증명을 누구나 풍족하게' 정도인데요. 사람이 '이걸 증명하고 싶어'라고 목표만 던지면, AI가 Lean 문법에 맞는 증명 코드를 초안으로 쭉 뽑아주는 거예요. 그리고 이게 진짜 맞는지는 Lean이 기계적으로 검사해주니까, AI가 헛소리(환각, hallucination)를 해도 걸러지죠. 'AI가 만들고 → 기계가 검증한다'는 이 조합이 핵심이에요. 일반적인 코드 생성 AI는 틀린 코드를 그럴듯하게 내놔도 사람이 일일이 확인해야 하는데, 수학 증명 쪽은 검증기가 자동으로 참/거짓을 판정해주니까 궁합이 훨씬 좋은 거죠.
이게 처음은 아니에요
사실 'AI로 수학 증명하기'는 요즘 글로벌 연구소들이 다들 뛰어든 뜨거운 판이에요. 구글 딥마인드는 AlphaProof로 국제수학올림피아드 문제를 은메달 수준으로 풀어냈고, Goedel-Prover 같은 오픈 프로젝트, Harmonic 같은 스타트업도 형식 증명 AI를 밀고 있어요. 이 흐름에서 미스트랄의 색깔은 늘 그렇듯 오픈 웨이트(open weight, 모델 가중치를 공개해서 누구나 받아 쓸 수 있게 하는 것) 전략이에요. 소수 거대 기업만 쓰는 비싼 API가 아니라, 연구자나 학생이 직접 받아 돌려볼 수 있게 풀어주는 방향인 거죠. 'for All'이라는 이름값을 이걸로 하는 셈이에요.
한국 개발자에게는 어떤 의미일까
'나는 수학자도 아닌데 이게 나랑 무슨 상관이지?' 싶을 수 있어요. 근데 형식 증명은 생각보다 실무에 가까워요. 예를 들어 항공·의료처럼 버그가 사람 목숨과 직결되는 소프트웨어, 은행 거래나 암호 프로토콜, 블록체인 스마트 컨트랙트처럼 '한 번 틀리면 돈이 날아가는' 코드는 '테스트로 대충 맞겠지'가 아니라 '수학적으로 절대 안 틀린다'를 증명하고 싶어 하거든요. 이걸 형식 검증(formal verification)이라고 해요.
지금까지는 이 작업이 너무 비싸고 어려워서 극소수 팀만 했는데, Leanstral 같은 도구가 성숙하면 문턱이 확 낮아질 수 있어요. AI가 증명 초안을 잡아주고 엔지니어는 다듬기만 하면 되니까요. 당장 실무에 넣긴 이르지만, '검증기가 자동으로 정답을 채점해주는 분야일수록 AI와 궁합이 좋다'는 원리는 지금 알아둘 가치가 충분해요. 코드 리뷰, 타입 시스템, 테스트 자동화 같은 우리 일상 도구에도 비슷한 아이디어가 스며들 거거든요.
한줄 정리: AI가 내놓은 답을 기계가 자동으로 채점해주는 분야(수학 증명)는 AI가 헛소리를 해도 걸러지니, 오히려 코드 생성보다 신뢰도가 높아질 수 있다.
여러분은 어떻게 보세요? AI가 짠 증명을 기계가 통과시켰다면, 그 과정을 사람이 다 이해하지 못해도 '믿고 써도 된다'고 할 수 있을까요?
🔗 출처: Hacker News