비선형 실수 산술 (Non-Linear Real Arithmetic)을 위한 프로그램 합성: 실현 가능성 (Realizability)을 넘어

우리는 비선형 실수 산술 (Non-Linear Real Arithmetic, NRA) 명세로부터 프로그램을 합성하는 문제를 연구합니다. 구문 유도 합성 (Syntax-Guided Synthesis, SyGuS)과 같은 기존 기술들은 명세가 실현 불가능 (Unrealizable)할 경우 프로그램을 합성하는 데 실패합니다. 우리는 이것이 많은 상황에서 만족스럽지 않다고 주장하며, 임의의 NRA 명세로부터 프로그램을 합성하는 것을 목표로 합니다. 즉, 어떤 입력에 대해서도 합성된 프로그램이 명세를 만족하는 출력을 생성하거나, 그러한 출력이 존재하지 않음을 보고하도록 합니다. 부동 소수점 산술 (Floating-point arithmetic)에 내재된 반올림 오차를 피하기 위해, 우리는 프로그램이 유리수 (Rational) 입력 및 출력에서 작동하도록 제한합니다. 첫째, 우리는 우리가 변형한 합성 문제가 정수론 (Number theory)의 오래된 미해결 문제만큼 어렵다는 것과, 유리수 입력 및 출력을 가진 임의의 NRA 명세로부터 루프가 없는 (Loop-free) 프로그램을 합성하는 것은 일반적으로 불가능하다는 것을 보여줍니다. 둘째, 명세가 단일 출력 변수를 포함하는 경우에 대해 건전하고 완전한 (Sound and complete) 합성 알고리즘을 제시합니다. 또한 실현 가능한 (Realizable) 명세의 경우, NRA (실수 입력 및 출력)를 위해 SyGuS가 생성한 프로그램이 입력과 출력이 유리수인 우리의 문제에 대한 솔루션 역할을 한다는 것을 보여줍니다. 셋째, 명세의 일반적인 사례에 대해 건전하지만 (필연적으로 불완전한) 합성 알고리즘을 제공합니다. 우리는 우리의 접근 방식을 NQSynth라는 프로토타입 도구로 구현하였으며, 이 도구는 명세를 실현 가능하게 변환하더라도 최신 SyGuS 도구들이 도달할 수 없는 많은 벤치마크를 해결합니다.