[태그:] Formal verification

AI가 수학 문제를 푸는 장면은 이제 데모 수준을 넘어 논문 생산 방식 자체를 건드리고 있다. Axiom Math가 흥미로운 이유는 단순히 “수학을 잘하는 모델”을 만들겠다는 야심 때문이 아니다. 이 회사는 자연어 문제를 Lean 형식 증명으로 바꾸고, 기계가 검증할 수 있는 증명서를 붙여 저널 논문까지 밀어 넣고 있다. 생성형 AI의 약점이 환각이라면, Axiom은 그 반대편인 “검증 가능한…