Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

기술 요약: 비선형 실수 산술을 위한 프로그램 합성: 실현 가능성을 넘어선 접근

문제 정의
본 논문은 비선형 실수 산술 (NRA) 의 양화 자유 이론에서 명세로부터 프로그램을 합성하는 문제를 다룹니다. 전통적인 문법 유도 합성 (SyGuS) 은 명세가 "실현 불가능"한 경우 (즉, 명세를 만족하는 출력이 존재하지 않는 입력 값이 존재하는 경우) 에 실패하는 반면, 본 연구는 새로운 합성 목표를 제안합니다. 목표는 임의의 유리수 입력에 대해 명세를 만족하는 유리수 출력을 생성하거나, 그러한 출력이 존재하지 않음을 명시적으로 보고 ($\bot$로 표시) 하는 프로그램을 합성하는 것입니다.

고정 정밀도 부동 소수점 산술에 내재된 반올림 오차로 인해 근사치로 평가할 때 유효한 실수 해가 실패할 수 있으므로, 저자들은 도메인을 유리수 입력과 출력으로 제한합니다. 이는 RPSQ(유리수 입력 및 출력을 갖는 실수 프로그램 합성) 라는 문제 클래스를 정의합니다. 합성된 프로그램은 유리수 수를 연산하는 루프, 조건문, 대입문을 포함할 수 있습니다.

이론적 난이도와 한계
저자들은 이 문제에 대한 중요한 이론적 경계를 설정합니다:

1. 힐베르트 제 10 문제와의 상호 환원성: RPSQ 가 유리수 위의 힐베르트 제 10 문제 ($HTP_{\mathbb{Q}}$) 와 상호 환원 가능함을 증명합니다. $HTP_{\mathbb{Q}}$는 수론에서 오랫동안 해결되지 않은 문제이므로, RPSQ 를 위한 일반적인 완전하고 건전한 합성 알고리즘이 존재할 가능성은 낮습니다.
2. 루프 없는 합성의 불가능성: 본 논문은 RPSQ 가 루프 없는 프로그램만을 사용하여 해결될 수 없음을 보여줍니다. 루프 없는 해가 존재한다면, 유리수 산술 이론이 양화 소거를 허용한다는 것을 의미하게 되며, 이는 이미 결정 불가능한 것으로 알려진 결과 (Robinson, 1959) 입니다.

방법론 및 알고리즘
일반적인 결정 불가능성으로 인해, 저자들은 계층적 접근 방식을 제안합니다:

1. 실수 대 유리수에서의 실현 가능성: 명세가 실수 위에서 실현 가능하다면, 기존 SyGuS 도구들 (실수 위에서 작동) 에 의해 합성된 어떤 프로그램도 입력과 출력이 유리수라면 유리수 경우에 대한 유효한 해가 됩니다. 그러나 그 역은 성립하지 않습니다. 즉, 유리수에 대한 해가 반드시 실수에 대한 해를 의미하는 것은 아닙니다.

2. 단일 출력 ($|Y|=1$) 을 위한 건전하고 완전한 알고리즘: 단일 출력 변수를 갖는 명세에 대해, 저자들은 건전하고 완전한 알고리즘 (알고리즘 1) 을 제시합니다. 이 접근법은 문제를 두 가지 경우로 나눕니다:

   • 부등식: 부등식의 부호가 불변인 구간을 찾기 위해 실근 분리 (RRI) 를 활용합니다. 이러한 구간 내에서 유리수 점을 샘플링하여 (실수 내 유리수의 조밀성을 활용) 엄격한 제약 조건에 대한 해를 찾습니다.
   • 비엄격한 부등식: 경계선 (비엄격한 부등식이 등식이 되는 곳) 에 위치한 해의 경우, 알고리즘은 유리근 정리 (RRT) 를 사용합니다. 이를 통해 경계 조건에서 유도된 다항식 방정식에 대한 유한한 후보 유리근 집합을 열거할 수 있습니다.
     이 알고리즘은 해의 존재를 위한 가장 약한 전제조건을 결정하기 위해 양화 소거 (QEPCAD 사용) 와 결합됩니다.

3. 일반적인 경우 ($|Y|>1$) 를 위한 건전하지만 불완전한 알고리즘: 여러 출력 변수의 경우, 저자들은 알고리즘 2(도구 NQSynth에 구현됨) 를 제안합니다. 이는 다중 출력 문제를 단일 출력 하위 문제로 반복적으로 분해하는 건전하지만 불완전한 절차입니다:

   • NRA 오라클 (Z3) 에 쿼리를 보내 유리수 만족 할당 (모델) 을 찾습니다.
   • 이 모델을 기반으로 하나의 출력 변수를 제외한 모든 출력 변수를 고정하여, 위에서 설명한 완전한 알고리즘으로 해결 가능한 단일 출력 합성 인스턴스로 문제를 축소합니다.
   • 양화 소거를 통해 유도된 특정 전제조건에 해당하는 각 분기를 갖는 결정 목록 (일련의 if-then-else 분기) 을 구성합니다.
   • 찾은 해의 전제조건을 부정하여 명세를 정제하는 과정을 반복하여, 명세가 만족 불가능해지거나 시간 초과가 발생할 때까지 진행합니다.

구현 및 실험 결과
저자들은 NQSynth라는 프로토타입 도구로 접근 방식을 구현했습니다. 이를 두 가지 경쟁 접근법과 비교 평가했습니다:

• QEPCAD+CVC5: 실수 위에서 가장 약한 전제조건을 먼저 계산한 후 프로그램을 합성하는 수정된 SyGuS 파이프라인.
• ModEnum: 선형 산술에 대한 Monniaux 의 작업에서 영감을 받은 모델 열거 기반 접근법.

평가에는 두 가지 벤치마크 세트가 사용되었습니다:

1. NRA 벤치마크: SMT-LIB 2024 저장소에서 가져온 83 개의 적응형 벤치마크 (meti-tarski/Arthan, asin, zankl 계열).
2. 기하학적 벤치마크: 2 차원 및 3 차원 기하학적 관계 (원, 고리 영역, 쌍곡선) 를 모델링한 51 개의 명세.

주요 결과:

• NQSynth는 120 초 시간 제한 내에 83 개의 NRA 벤치마크 중 59 개와 51 개의 기하학적 벤치마크 중 33 개를 해결했습니다.
• 반면, QEPCAD+CVC5는 26 개의 NRA 및 16 개의 기하학적 벤치마크를 해결했고, ModEnum은 23 개의 NRA 및 11 개의 기하학적 벤치마크를 해결했습니다.
• 특히 NQSynth 는 실현 불가능하거나 (또는 가장 약한 전제조건을 계산하기 어려운) 많은 명세에 대해 성공적으로 프로그램을 합성했으며, 이는 SyGuS 도구가 완전히 실패하는 시나리오였습니다.
• 실험은 NQSynth 의 주요 병목 현상이 합성 로직 자체가 아니라, 특히 더 큰 입력의 경우 양화 소거 단계 (QEPCAD) 에 있음을 강조했습니다.

의의 및 주장
본 논문은 NRA 명세로부터의 프로그램 합성 도구 세트에 새로운 기법을 추가했다고 주장합니다. 그 주요 의의는 다음과 같습니다:

1. 실현 불가능성 처리: 현재 최첨단 SyGuS 도구들이 결여된 기능인, 해가 존재하지 않는 입력에 대해 우아하게 대처하는 프로그램을 합성하는 실용적인 방법을 제공합니다.
2. 유리수 정밀도: 부동 소수점 산술과 관련된 반올림 오차를 피하기 위해 유리수 입력과 출력을 대상으로 함으로써, 고정밀도가 필요한 응용 프로그램에 대한 수학적 정확성을 보장합니다.
3. SyGuS 를 넘어선 접근: 문법적 검색이나 표준 양화 소거에만 의존하는 대신 수론적 속성 (RRT 및 RRI) 을 활용함으로써, 실현 가능한 명세조차 기존 SyGuS 도구의 범위를 벗어난 문제들을 해결합니다.

저자들은 $HTP_{\mathbb{Q}}$의 난이도로 인해 일반적인 완전한 해가 이론적으로 불가능할 것으로 결론지으면서도, 그들의 건전하고 불완전한 절차가 다양한 벤치마크에서 기존 방법들을 크게 능가하는 견고한 실용적 해법을 제공한다고 주장합니다. 향후 연구로는 루프 없는 프로그램이 충분한 조건을 조사하고 무거운 양화 소거 엔진에 대한 의존도를 줄이는 것이 제안됩니다.