LLM의 수학적 오류 해결 위한 'MathKernel' 공개… 증거 기반 검증 및 MCP 서버 지원

LLM은 수학적 의도 해석에는 강하지만 정확한 산술 계산에는 취약하다는 한계를 극복하기 위해, MathKernel이 공개되었습니다. 이 프로젝트는 LLM이 파싱과 계획만 담당하고, 실제 계산과 증거 확보는 전용 커널이 수행하는 노동 분업 구조를 채택했습니다.

핵심 아키텍처 및 증거 모델

MathKernel은 단순한 계산기가 아닌 증거 인식(Evidence-aware) 멀티엔진 오케스트레이션 레이어입니다. 모든 수학적 결과는 다음과 같은 명확한 신뢰 수준(Trust Level)과 증거 번들(Evidence Bundle)을 포함합니다.

• Formal: Lean 증명 커널에 의해 검증된 형식적 증명
• Exact: 정확한 산술 연산 또는 검증된 인증서(Certificate)
• Symbolic: SymPy 등 심볼릭 엔진의 합의
• Certified Numeric: mpmath 등을 통한 엄격한 구간 포함(Interval Enclosure)
• Empirical/Numeric: 경험적 증거 또는 부동소수점 계산

단일 엔진의 일치만으로는 증명으로 간주하지 않으며, 독립적인 교차 검증이나 형식적 검증을 통해 신뢰도를 구분합니다. 특히 근사 입력(Approximate Input)의 계보(Ancestry)를 추적하여, 10진수 입력이 포함된 경우 자동으로 신뢰 수준을 'Numeric'으로 상한 설정하는 등 엄격한 증거 관리를 수행합니다.

주요 기능 및 도구

• 다양한 수학 도메인 지원: 심볼릭 대수, 미적분, 복소 해석, 유한 군, 선형 대수, 그래프 이론, 확률 통계, PDE/FEM(유한요소법) 등 광범위한 영역을 지원합니다.
• MCP(Model Context Protocol) 서버: mathkernel-mcp를 통해 LLM 에이전트가 167개의 수학 도구를 호출할 수 있습니다. 에이전트는 math_capabilities로 기능을 탐색하고, math_reason 등을 통해 계산 및 검증을 요청합니다.
• 멀티모달 아티팩트: 계산 결과를 시각화(Viz) 및 청각화(Sonification) 가능한 포터블 HTML 아티팩트로 변환하며, 이 과정에서도 원본 데이터의 증거 신뢰도를 보존합니다.
• 성능 최적화: Numba JIT 컴파일, CUDA GPU 가속, 병렬 처리 풀을 활용하여 Collatz 추측 스프레드, GF(2^m) 연산 등 대규모 계산의 성능을 확보했습니다.

설치 및 활용

Python 라이브러리(pip install mathkernel) 및 MCP 서버(pip install 'mathkernel[mcp]')로 설치 가능하며, Lean 4 및 Mathlib는 첫 실행 시 자동 설치됩니다. LLM 에이전트가 수학 문제를 다룰 때 환각(Hallucination)을 줄이고, 계산 결과의 출처와 검증 가능성을 명확히 하고자 하는 개발자에게 유용한 도구입니다.