수학을 '증거'로 다루는 LLM용 커널, MathKernel의 설계 철학

대규모 언어모델(LLM)은 수학 문제의 의도를 파악하는 데는 능하지만 실제 산술과 증명 과정에서는 자주 틀린다. GitHub에 공개된 MathKernel은 이 역할 분담을 뒤집는다. 모델은 파싱하고 계획하고 해석하는 일을 맡고, 커널은 계산과 함께 각 주장(claim)에 대한 근거를 기록한다. 파이썬 라이브러리(mathkernel)로도, MCP 서버(mathkernel-mcp)로도 쓸 수 있어 애플리케이션과 LLM이 가정과 유래(provenance)를 보존한 채 고급 수학을 수행하도록 하는 것이 목표다.

계산 결과에 '신뢰 등급'을 붙이다

MathKernel의 핵심은 모든 수학 결과가 명시적인 신뢰 등급, 엔진 태그, 유도 이력을 함께 지닌다는 점이다. 정확 산술, 검증된 인증서, 기호적 결과, 인증된 구간 포함(certified enclosure), 경험적 증거, 형식 증명은 서로 다른 종류의 주장으로 구분된다. 정확한 산술이라고 해서 그것이 곧 형식 증명은 아니며, 근사값에서 비롯된 계산의 이력이 조용히 사라져서도 안 된다는 원칙이다. 여러 엔진이 같은 답을 냈다는 사실('엔진 합의')만으로는 증명이 되지 않고, 하나의 신뢰 라벨이 증거 묶음 전체를 대체하지도 못한다.

이 철학은 구조에도 반영돼 있다. MathKernel은 단일 솔버가 아니라 타입이 부여된 오케스트레이션 계층이다. 공개 파사드가 파싱, 컨텍스트, 객체 동일성, 영속성, 증거 합성, 자원 정책, 유도 추적을 담당하고, 실제 수학은 도메인 어댑터가 맡는다. 그림이나 오디오 같은 표현 계층은 하위에 위치하며, 보기 좋은 플롯을 만들어냈다고 해서 더 강한 수학적 증거가 생기지는 않는다. 렌더러는 증거를 '보여줄' 뿐 '만들지'는 못한다.

소수점 하나가 신뢰 등급을 바꾼다

실무자 관점에서 가장 흥미로운 규칙은 소수 리터럴의 처리 방식이다. MathKernel은 십진 소수를 '근사 관측값'으로 간주한다. 식 어딘가에 소수(RealNode)가 들어가면 파싱 시점부터 그 식의 신뢰도는 numeric으로 상한이 걸린다. 즉 0.1 + x는 numeric으로, 1/2 + x는 symbolic으로 파싱된다. 근사 입력에 대해서는 Lean 기반 형식 인증서나 정확 SMT 반례 생성이 거부되는데, 백엔드가 소수 문법을 정확한 유리수로 인코딩해 결과적으로 '다른 명제'를 증명하게 되는 것을 막기 위해서다. 증명급 근거가 필요하면 정확 유리수나 구간 인증을 쓰라는 것이다.

전체 신뢰도는 어떤 노드가 낸 최대 신뢰도가 아니라, 주장을 성립시키는 데 필요한 가장 약한 증거에 의해 제한된다. 백엔드끼리 결과가 어긋나면 평균으로 뭉개지 않고 명시적 충돌로 보존된다. 각 MathResult는 계산·증명·인증서·수치·모델·경험적 증거를 분리해 담은 evidence_bundle을 지니며, 결론별로 이 묶음을 유지하는 claim_evidence를 통해 서로 다른 성격의 주장이 하나의 점수로 뭉개지지 않도록 한다. does_not_exist(존재하지 않음), undefined, infeasible, unsupported 같은 의미론적 상태는 '증명 강도'와 '수학적 결과'를 구분해 주며, MCP 직렬화와 비동기 작업 조회, 유도 재생 과정에서도 살아남는다.

난수생성기 분석부터 미분기하까지

적용 범위는 넓다. MCP 서버는 stdio 위에서 FastMCP 3로 동작하며 math_ 접두어가 붙은 162개 도구를 제공하고, 첫 실행 시 Lean 4와 Mathlib을 기본 설치한다(CI용으로는 환경변수로 건너뛸 수 있다). GPU는 CuPy로 시도하되 스택이 깨지면 실제 행렬곱으로 가용성을 확인한 뒤 CPU로 자연스럽게 강등된다. 신호·제어·최적화 같은 공학 수학도 동일한 증거·영속성 계약 아래 다룬다. 선형·이차 계획법은 검증 가능한 최적성 증거를 반환할 수 있고, 실행 불가능한 LP는 Farkas 인증서를, 무계 문제는 후퇴 방향(recession ray)을 노출하며, MILP는 결괏값만이 아니라 재생 가능한 증명 트리를 남긴다.

특히 눈에 띄는 것은 유한 동역학계(X, μ, T, O)의 정확한 스펙트럼 분석 기능으로, 의사난수생성기(PRNG) 구조 분석을 위해 만들어지고 검증됐다. scripts 트리에는 xorshift/xoroshiro 계열, MT19937, PCG, LXM, SplitMix64, Philox 등 25종 이상의 생성기를 처음부터 재현할 수 있는 스크립트와 참조 데이터가 함께 들어 있어 외부 픽스처 없이 재현 가능하다. 여기에 다양체·차트·계량 객체를 통한 크리스토펠 기호, 리만·리치·스칼라 곡률, 측지선 방정식 계산과 비틀림 없음·비앙키 항등식 같은 기호적 검증까지 포함한다.

한계와 실무적 의미

MathKernel의 문서는 한계를 감추지 않는다는 점에서 오히려 신뢰를 준다. 비곱(non-product) 결합 지지집합, 명시적 겹침 소스 도메인이 없는 해석적 연속, ROC를 SymPy가 확정하지 못하는 변환, 역분기나 야코비안이 제공되지 않은 일반 다변수 변수변환 등은 알려진 제약으로 명시돼 있다. 기호적 가용성은 '후보 증거'일 뿐 독립적 증명이 아니며, 같은 엔진에서 나온 항등식은 symbolic로 상한이 걸린다. 결국 이 프로젝트가 던지는 메시지는 분명하다. LLM 시대에 계산 도구가 갖춰야 할 덕목은 정답을 빨리 내는 것이 아니라, 그 답이 어떤 종류의 근거 위에 서 있는지를 정직하게 라벨링하고 보존하는 규율이라는 것이다. AI가 수학적 주장을 대신 생성하는 워크플로를 설계하는 실무자라면, '증거의 종류를 구분하고 가장 약한 고리에 신뢰를 맞춘다'는 이 설계 원칙 자체를 참고할 만하다.