SMT 솔버

SMT 솔버는 여러 규칙과 조건을 한꺼번에 놓고 이것들이 서로 모순 없이 다 성립할 수 있는지 수학적으로 계산해주는 프로그램이다. 마치 복잡한 스도쿠 퍼즐을 손으로 하나하나 맞춰보는 대신, 규칙을 통째로 넣으면 풀리는지 안 풀리는지를 딱 잘라 답해주는 계산기 같은 존재다.

예를 들어 어떤 서비스가 「이 질문에 이렇게 답해도 되는가」를 검증하려 한다고 하자. 먼저 질문과 답을 논리식으로 바꿔 정책의 규칙 변수에 끼워 맞춘 다음, SMT 솔버가 이 논리식을 정책 규칙과 대조해 성립 여부를 판정한다. 이 과정은 「대충 비슷한 사례를 많이 봐서 그럴듯하다」는 식의 확률적 추측이 아니라, 수학 증명처럼 조건이 맞으면 결과도 반드시 맞다는 방식이라 판정의 근거가 명확하다.

이런 검증 도구는 보통 SMT-LIB이라는 표준 입력 형식으로 규칙을 적어 넣는데, 이는 여러 자동 증명 프로그램이 공통으로 쓰는 일종의 공식 언어라고 보면 된다.

기사는 「SMT(Satisfiability Modulo Theories) 솔버가 이 논리를 정책 규칙과 대조해 검증하고 판정을 내린다」고 설명한다. 여기서 SMT 솔버는 AI가 대충 답을 맞히는 도구가 아니라, 논리식이 규칙과 모순되지 않는지 수학적으로 확인하는 별도의 검증 엔진이라는 점을 주의해야 한다. AI(파운데이션 모델)는 질문과 답을 논리식으로 번역하는 역할만 하고, 실제 참/거짓 판정은 SMT 솔버가 담당한다.