이중 반올림(Double Rounding)이 올바른 경우

소프트웨어에서 숫자 형식과 그 산술 연산을 구현하는 넘버 라이브러리(Number libraries)는 하드웨어를 시뮬레이션하는 데 사용되어, 하드웨어 동작을 재현 가능하고 따라서 검증 가능하며 설계하기 쉽게 만듭니다. 하지만 현대 머신러닝 가속기(accelerators)는 기존의 넘버 라이브러리가 지원하지 않는 특수화된 숫자 형식을 점점 많이 사용하기 때문에 시뮬레이션하기 어렵습니다. 이러한 라이브러리를 전통적인 방법으로 확장하는 것은 비용이 많이 듭니다. 왜냐하면 연산, 형식, 반올림 모드의 각 조합마다 맞춤형 구현(bespoke implementation)이 필요하기 때문입니다. 더 쉬운 방법은 이중 반올림(double round)을 사용하는 것입니다. 즉, 더 높은 정밀도로 계산한 다음 다시 반올림하는 방식입니다. 이렇게 하면 하나의 고정밀도 커널로 많은 형식을 처리할 수 있지만, 이중 반올림이 올바르다는 것은 선택적인 경우에만 알려져 있습니다. 우리는 여러 형식과 반올림 모드 전반에 걸쳐 이중 반올림이 언제 올바른지에 대한 정확하고 효율적으로 검사 가능한 특성화를 제시합니다. 우리의 결과는 고정 소수점(fixed-point) 및 부동 소수점(floating-point) 표현을 통합하는 새로운 추상 숫자 형식(abstract number format)에 기반하며, 이로써 이중 반올림의 정확성을 '형식 포함성(format containment)'이라는 문제로 축소시킵니다. 즉, 한 형식의 모든 값이 다른 형식으로 표현 가능한지 여부입니다. 우리는 이러한 결과를 Lean 4에서 기계화했습니다. 또한, 연산 시퀀스가 주어졌을 때 각 식을 그 결과값을 반드시 포함하는 넘버 형식으로 경계짓는(bounds) 형식 추론 알고리즘(format inference algorithm)을 소개합니다. 우리는 이 통찰력을 두 가지 방식으로 적용합니다. 첫째, 올바르게 반올림된 다중 정밀도 넘버 라이브러리인 MPFX를 제시하며, 이는 정확한 이중 반올림을 활용하여 많은 숫자 형식을 효율적으로 시뮬레이션합니다. MPFX의 올바르게 반올림된 연산은 MPFR보다 최대 11배(평균: 6.05배) 빠르며, 동일한 정밀도에서 SoftFloat와 경쟁할 만합니다(0.46배~1.63배 사이로 빠름; 평균: 0.94배). 둘째, 사례 연구에서 SoftFloat와 MPFX의 기본 요소(primitives)를 모두 사용하여 하드웨어 사양에 대한 소프트웨어 시뮬레이션을 구현했습니다. 이 경우 MPFX 버전이 최대 13.5배 더 빠릅니다.