반례 하나면 추측이 무너지거든요
수학에는 “추측(conjecture)”이라는 개념이 있어요. 아직 증명되지는 않았지만 아마 참일 것 같다고 수학자들이 오랫동안 믿어온 명제인데요. 이걸 참으로 확정하려면 빈틈없는 증명을 완성해야 하지만, 거짓으로 확정하는 건 훨씬 간단해요. 성립하지 않는 사례, 그러니까 반례(counterexample)를 딱 하나만 찾으면 끝이거든요. “모든 경우에 성립한다”는 주장은 안 되는 경우 하나만 보여주면 그 자리에서 무너지니까요.
그런데 최근 수학계에서 의미심장한 흐름이 나타나고 있어요. 이 “반례 찾기” 영역에서 인간 수학자들이 컴퓨터와 AI에게 밀리기 시작했다는 건데요. 정리 증명 보조 도구인 Lean을 수학계에 퍼뜨려온 Xena Project 블로그가 이 현상을 “인간 수학자들이 반례 찾기에서 추월당하고 있다(outcounterexampled)”라는 도발적인 표현으로 짚었어요.
왜 하필 반례 찾기에서 밀릴까요
이유를 뜯어보면 꽤 자연스러워요. 증명과 반례 찾기는 문제의 구조 자체가 다르거든요. 증명은 무한히 많은 경우를 한 번에 커버하는 논리를 세워야 해서 깊은 통찰이 필요해요. 반면 반례 찾기는 본질적으로 탐색 문제예요. 후보를 잔뜩 만들어보고, 조건에 어긋나는 놈이 하나라도 나오는지 확인하면 되죠.
이 구조가 정확히 컴퓨터가 잘하는 “생성하고 검증하기(generate-and-verify)” 루프와 맞아떨어져요. AI가 후보를 백만 개 만들었는데 그중 999,999개가 쓰레기여도 상관없어요. 검증은 기계적인 계산이라 순식간에 끝나고, 단 하나라도 진짜 반례가 걸리면 그게 곧 수학적 사실이 되니까요. AI의 고질적인 약점인 “그럴듯한 헛소리”가 문제되지 않는 영역인 거죠. 틀린 후보는 검증 단계에서 자동으로 걸러지니까요.
실제 사례도 꾸준히 쌓이고 있어요. DeepMind는 몇 년 전 강화학습으로 그래프 이론의 오래된 추측들에 대한 반례를 찾아낸 연구를 발표했고, 최근에는 AlphaEvolve처럼 LLM이 코드를 진화시키며 수학적 구성물을 탐색하는 시스템이 조합론 문제들에서 수십 년 묵은 기록을 갈아치우기도 했어요. 사람이 손으로는 도저히 뒤져볼 수 없는 크기의 탐색 공간을 GPU가 밀어붙이는 그림이에요.
Lean이 여기서 왜 중요하냐면
반례가 복잡해지면 “이게 진짜 반례 맞아?”를 확인하는 것조차 사람에게는 부담이에요. 여기서 Lean 같은 형식 검증 도구가 등장하는데요. 이게 뭐냐면, 수학 증명을 컴퓨터가 한 줄 한 줄 기계적으로 검사할 수 있는 코드로 적는 시스템이에요. AI가 찾은 반례를 Lean으로 검증해두면 사람이 일일이 안 믿어줘도 “컴파일이 통과했으니 참”이라고 말할 수 있게 돼요. 개발자 입장에서 보면 타입 체커를 통과한 코드 같은 거죠. AI가 뭘 만들어내든 최종 판정은 기계적 검증기가 내리니, 신뢰 문제가 깔끔하게 해결되는 거예요.
개발자에게 낯설지 않은 그림이에요
사실 이 구도, 우리한테 이미 익숙하거든요. 속성 기반 테스트(property-based testing)라고, Hypothesis나 fast-check 같은 도구가 하는 일이 정확히 이거예요. “이 함수는 어떤 입력에도 이 성질을 만족해야 해”라고 선언하면 도구가 무작위 입력을 퍼부어서 반례를 찾아주죠. 보안 쪽의 퍼징(fuzzing)도 마찬가지고요. 수학계에서 벌어지는 일은 이 패턴이 훨씬 큰 스케일과 훨씬 똑똑한 탐색으로 올라간 버전이라고 볼 수 있어요.
여기서 얻을 실무 교훈은 명확해요. “검증기가 존재하는 문제”에서는 AI를 최대로 굴릴 수 있다는 거예요. 테스트 스위트, 타입 시스템, 컴파일러처럼 정답 여부를 기계가 판정해주는 환경을 만들어두면, AI가 아무리 헛발질을 해도 걸러낼 수 있으니 마음 놓고 시도 횟수를 늘릴 수 있거든요. AI 코딩 도구를 잘 쓰는 팀들이 테스트 커버리지에 먼저 투자하는 이유이기도 해요.
정리하면
증명처럼 창의적 통찰이 필요한 영역은 아직 인간의 몫이 크지만, “하나만 찾으면 이기는” 탐색 게임에서는 이미 기계가 앞서기 시작했어요. 여러분의 업무에서 “검증은 쉽지만 탐색은 막막한” 문제가 있다면, 그게 바로 AI를 붙여볼 최적의 자리일지도 몰라요. 여러분이라면 어떤 문제에 이 생성-검증 루프를 적용해보고 싶으세요?
🔗 출처: Hacker News