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

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

Problem Definition
This paper addresses the problem of synthesizing programs from specifications in the quantifier-free theory of Non-Linear Real Arithmetic (NRA). Unlike traditional Syntax-Guided Synthesis (SyGuS), which fails when a specification is "unrealizable" (i.e., there exist input values for which no output satisfies the specification), this work proposes a novel synthesis objective. The goal is to synthesize a program that, for any rational input, either produces a rational output satisfying the specification or explicitly reports the non-existence of such an output (denoted by $\bot$).

To avoid rounding errors inherent in fixed-precision floating-point arithmetic, which can cause valid real solutions to fail when evaluated with approximations, the authors restrict the domain to rational inputs and outputs. This defines the problem class RPSQ (Real Program Synthesis with Rational inputs and outputs). The synthesized programs are allowed to contain loops, conditionals, and assignments, operating on rational numbers.

Theoretical Hardness and Limitations
The authors establish significant theoretical boundaries for this problem:

1. Inter-reducibility with Hilbert's Tenth Problem: They prove that RPSQ is inter-reducible with Hilbert's Tenth Problem over the rationals ($HTP_{\mathbb{Q}}$). Since $HTP_{\mathbb{Q}}$ is a long-standing open problem in number theory, this implies that a general sound and complete synthesis algorithm for RPSQ is unlikely to exist.
2. Impossibility of Loop-Free Synthesis: The paper demonstrates that RPSQ cannot be solved using only loop-free programs. If a loop-free solution existed, it would imply that the theory of rational arithmetic admits quantifier elimination, a result known to be undecidable (Robinson, 1959).

Methodology and Algorithms
Given the general undecidability, the authors propose a tiered approach:

1. Realizability over Reals vs. Rationals: They show that if a specification is realizable over the reals, any program synthesized by existing SyGuS tools (which operate over reals) also serves as a valid solution for the rational case, provided the inputs and outputs are rational. However, this does not hold in reverse; a solution for rationals does not necessarily imply a solution for reals.

2. Sound and Complete Algorithm for Single-Output ($|Y|=1$): For specifications with a single output variable, the authors present a sound and complete algorithm (Algorithm 1). This approach separates the problem into two cases:

   • Strict Inequalities: It utilizes Real Root Isolation (RRI) to find intervals where the sign of polynomials is invariant. By sampling rational points within these intervals (exploiting the density of rationals in reals), it finds solutions for strict constraints.
   • Non-Strict Inequalities: For solutions lying on the boundary (where non-strict inequalities become equalities), the algorithm employs the Rational Root Theorem (RRT). This allows for the enumeration of a finite set of candidate rational roots for the polynomial equations derived from the boundary conditions.
     The algorithm combines these with Quantifier Elimination (using QEPCAD) to determine the weakest preconditions for the existence of solutions.

3. Sound but Incomplete Algorithm for General Case ($|Y|>1$): For multiple output variables, the authors propose Algorithm 2 (implemented in the tool NQSynth). This is a sound but incomplete procedure that iteratively decomposes the multi-output problem into single-output sub-problems:

   • It queries an NRA oracle (Z3) to find a rational satisfying assignment (model).
   • It fixes all but one output variable based on this model, reducing the problem to a single-output synthesis instance solvable by the complete algorithm described above.
   • It constructs a decision list (a series of if-then-else branches) where each branch corresponds to a specific pre-condition derived via quantifier elimination.
   • The process repeats, refining the specification by negating the preconditions of found solutions, until the specification becomes unsatisfiable or a timeout occurs.

Implementation and Experimental Results
The authors implemented their approach in a prototype tool named NQSynth. They evaluated it against two competing approaches:

• QEPCAD+CVC5: A modified SyGuS pipeline that first computes the weakest precondition over reals and then synthesizes a program.
• ModEnum: A model-enumeration based approach inspired by Monniaux's work on linear arithmetic.

The evaluation used two benchmark sets:

1. NRA Benchmarks: 83 adapted benchmarks from the SMT-LIB 2024 repository (meti-tarski/Arthan, asin, zankl families).
2. Geometric Benchmarks: 51 specifications modeling 2D and 3D geometric relationships (circles, annular regions, hyperbolas).

Key Results:

• NQSynth solved 59 out of 83 NRA benchmarks and 33 out of 51 Geometric benchmarks within a 120-second timeout.
• In contrast, QEPCAD+CVC5 solved 26 NRA and 16 Geometric benchmarks, while ModEnum solved 23 NRA and 11 Geometric benchmarks.
• Notably, NQSynth successfully synthesized programs for many specifications that were unrealizable (or where the weakest precondition was difficult to compute), a scenario where SyGuS tools fail entirely.
• The experiments highlighted that the primary bottleneck for NQSynth was the quantifier elimination step (QEPCAD), particularly for larger inputs, rather than the synthesis logic itself.

Significance and Claims
The paper claims to add a novel technique to the repertoire of program synthesis from NRA specifications. Its primary significance lies in:

1. Handling Unrealizability: It provides a practical method to synthesize programs that gracefully handle inputs for which no solution exists, a capability lacking in current state-of-the-art SyGuS tools.
2. Rational Precision: By targeting rational inputs and outputs, it avoids the rounding errors associated with floating-point arithmetic, ensuring mathematical correctness for applications requiring high precision.
3. Beyond SyGuS: The approach solves problems that are beyond the reach of existing SyGuS tools, even for realizable specifications, by leveraging number-theoretic properties (RRT and RRI) rather than relying solely on syntactic search or standard quantifier elimination.

The authors conclude that while a general complete solution is theoretically unlikely due to the hardness of $HTP_{\mathbb{Q}}$, their sound and incomplete procedure offers a robust practical solution that significantly outperforms existing methods on a wide range of benchmarks. Future work is suggested to investigate conditions under which loop-free programs are sufficient and to reduce dependence on heavy quantifier elimination engines.