수치해석 라이브러리의 정확성을 각잡고 증명할 DSL의 필요성 - 이원열 교수님 (포항공대)

06 Feb, 2025 [seminar] 3 min read

[분류] SRC-ERC STAAR (소프트웨어재난연구센터) 계절학교 강연

연구 소개: 연속적인 값 (Continuous Computation)의 정확성

저는 프로그램과 계산의 수학적인 성질에 관심이 많습니다. 특히 프로그램이 수학적으로 정확한지 (Correctness), 그리고 효율적인지, 이론적 한계는 무엇인지 등을 연구합니다.

제가 주로 다루는 프로그램은 여기 계신 많은 분들과 달리, 연속적인 (continuous) 값을 다룹니다. (예: 2.8, 3/7, \(\sqrt{5}\)) 이런 값들에 더하기, 곱하기, \(\sin\) 등의 연산을 적용하는 계산이죠.

이러한 연속적인 계산은 머신러닝, 최적화, 컴퓨터 그래픽스, 과학 컴퓨팅 등 사실상 CS 전반에서 엄청나게 많이 사용되고 있습니다.

이론과 실제의 간극 (Gap)

오늘날에는 다양한 수치해석 라이브러리가 있습니다. NumPy, SciPy, TensorFlow, PyTorch, Intel Math Library 등.. 각각의 목적 (함수값 계산, 샘플링, 미분, 적분, 근사.. )에 맞게 존재합니다.

하지만 저는 이 라이브러리들이 “수학적으로 정확한가?” 라는 질문을 던집니다.

알고리즘의 가정: 실수 연산이 정확하다고, 함수가 미분 가능하다고 가정합니다.
실제: 하지만 실제 구현은 ‘부동 소수점 (Floating Point)’ 위에서 이루어집니다. 또한 if 문, 브랜치 (branch), ReLU 함수 등 미분 불가능한 지점도 많습니다.

이론과 실제 사이에 이런 간극이 존재하고, 구현체 자체가 복잡한 상황에서 이 라이브러리들은 과연 정확할까요?

구현의 복잡성과 정확성 (Correctness) 문제

이론은 깔끔하지만, 이걸 플로팅 포인트로 구현하는 것은 지옥입니다. (CR-LibM 라이브러리의 sin_fast.c 예시)

문제 1: \(\pi\)의 근사: \(\pi\) 자체가 무리수라 부동 소수점으로 정확히 표현이 안 됩니다.
- 나이브하게 \(\pi\)를 64비트 DOUBLE로 근사해서 쓰면, \(x\)값이 클 때 (e.g., \(10^{18}\)) 라운딩 에러가 누적되어 \(\sin(x)\) 결과값이 터무니없이 나옵니다.
- 해결: 라이브러리는 \(\pi\) 값을 1280비트까지 미리 계산해 테이블로 저장해두고, 이 값의 일부 비트 (bit)만 떼어내기 위해 알 수 없는 정수 연산과 비트 쉬프트 (bit shift)를 수행합니다. (부동 소수점 연산이 아님)
문제 2: 알 수 없는 상수: 테일러 급수의 계수나 테이블 값들이 사람이 이해할 수 없는 16진수 상수 (hard-coded constant)로 저장되어 있습니다.
문제 3: 복잡한 트릭: 정확도를 높이기 위해 숫자 하나를 DOUBLE 2개 (상위 비트 + 하위 비트)로 쪼개어 표현하거나 (double-double arithmetic), 라운딩 에러 자체를 계산하는(fast_sum 트릭) 등 매우 복잡한 기법을 씁니다.

이렇게 복잡한데, 과연 이 코드는 정확할까요?

새로운 방향: 정확성을 보장하는 라이브러리 설계

기존 라이브러리는 너무 복잡해서 검증이 어렵습니다. (제가 박사 때 Intel \(\sin\) 함수를 검증하려 64코어로 2주를 돌린 적도 있습니다.)

그래서 저는 “아예 처음부터 정확성 (correctness)을 염두에 두고” 새로운 라이브러리를 만들자는 방향을 생각하고 있습니다.

DSL (Domain-Specific Language) 개발: low-level 트릭 (정수 연산 등)을 잘 감싸고 (abstraction), high-level 구조 (범위 축소, 다항식 근사 등)를 명확히 드러내는 작은 언어를 만듭니다.
검증 기술 개발: 이 DSL에 최적화된 검증 도구를 만듭니다.
라이브러리 생성: 이 DSL로 라이브러리를 작성하고 검증합니다.
자동 최적화: DSL이 high-level 구조를 가지므로, 컴파일러 최적화나 자동 프로그램 탐색을 통해 “정확성이 보장되면서 가장 효율적인” 코드를 자동으로 생성할 수 있습니다.

5~10년 안에는 가능하지 않을까 생각합니다.

결론

수치 라이브러리와 연속적인 계산은 100년 가까이 연구되었지만, 엄밀한 정확성 보장 (rigorous correctness guarantee)은 아직도 부족합니다.

프로그래밍 언어 (PL) 기술을 현명하게 이용하면 이 문제들을 풀어낼 수 있을 것이라 생각합니다.

Q&A

Q: 퍼포먼스 기준은 무엇인가? (정확도만 쫓으면 MPFR처럼 너무 느려지지 않나?)
- A: 통용되는 기준은 없고, 그냥 “기존 라이브러리만큼 빠르거나 더 빠르게"가 목표입니다. MPFR은 100배 이상 느릴 수 있으므로, 실용적인 시간 안에 계산하는 것이 중요합니다.
Q: 이런 라이브러리 에러 때문에 발생한 실제 문제가 있나?
- A: 부동 소수점 에러로 로켓이 폭발한 사례가 있습니다. 또 CERN에서 힉스 보존 입자를 검출할 때, 계산 속도를 높이려 수학 라이브러리를 바꿨더니 원래 검출되던 입자 몇 개가 검출이 안 되는 문제가 발생했습니다.
Q: 테이블에 저장되는 상수 값들은 어떻게 정확하게 계산하나?
- A: MPFR, Mathematica 같은 고정밀 라이브러리를 씁니다. (Q: 그럼 그 라이브러리들은 정확한가?) 그것들도 에러가 종종 나옵니다. 궁극적으로는 Lean이나 Coq 같은 증명 도구로 모든 것을 각잡고 검증해야 (formal verification) 한다고 생각합니다. 10~20년 안에는 가능하지 않을까요.

참고 강연

[[(강연 요약) What Does Automatic Differentiation Compute for Non-Differentiable Functions - 이원열 교수님 (포항공대)|(강연 요약) What Does Automatic Differentiation Compute for Non-Differentiable Functions - 이원열 교수님 (포항공대)]] - 여기서는 미분불가능점 회피 이야기!