💻 computer science

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

本文针对现有合成工具在处理不可实现的非线性实算术规范时的局限性，提出了一种框架，该框架能够合成有理数输入/输出程序以要么满足规范要么正确报告不存在性，其中包含针对单输出情形的完备算法以及针对一般规范并在 NQSynth 工具中实现的保真但不完备的方法。

原作者： S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi

发布于 2026-05-26

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一位主厨（计算机），正试图遵循一份极其严格的食谱（规范）来制作一道菜肴（程序输出）。

问题：“不可能”的食谱

在计算机科学领域，有一种流行的方法称为SyGuS（语法引导合成）。它就像一个机器人厨师，试图找到一份食谱，使其适用于你抛给它的每一种可能的食材组合。

然而，有时你给机器人的食谱是有缺陷的。例如，想象一份食谱说：“做一个宽度正好为 1 米的蛋糕，但你只有一个宽度为 10 厘米的烤盘。”

如果你给机器人一个小烤盘，它可以做一个小蛋糕。
如果你给它一个大烤盘，在里面做一个 1 米宽的蛋糕在物理上是不可能的。

老式工具（如 SyGuS）看到这种情况会说："我放弃了！这份食谱对于每一种情况都是无法遵循的，所以我根本不会编写任何代码。"即使对于那些可能的情况（比如当你有一个小烤盘时），它们也拒绝提供帮助。

新方法：“聪明”的厨师

这篇论文的作者 Akshay、Chakraborty、Govind 和 Joshi 表示："这还不够好。我们需要一位厨师，在可能时烹饪，在不可能时礼貌地说‘我做不到’。"

他们创建了一种构建程序的新方法，能够处理非线性实数算术（涉及曲线、平方和复杂关系的数学，而不仅仅是简单的加法）。他们的目标是合成一个程序，该程序：

成功： 如果输入允许得出正确答案，则完美地计算出它。
承认失败： 如果输入使得答案不可能，它不会崩溃或猜测；而是明确地说：“此处无解。”

“有理”规则：无舍入误差

他们工作的关键部分在于如何处理数字。计算机通常使用“浮点数”（如 3.14159...），这类似于近似值。如果你用近似值做数学运算，就会产生微小的误差（舍入误差），这些误差累积起来可能导致大错误。

作者决定使用有理数（分数，如 22/7 或 3/4）。

类比： 想象建造一座房子。浮点数学就像使用一把略微弯曲的尺子；你的墙壁可能会倾斜。有理数学就像使用激光精确的蓝图，其中每个测量值都是精确的。
权衡： 精确数学的计算速度较慢，但它保证了零误差。作者想要的程序在数学上是完美的，而不仅仅是“差不多”。

三大发现

1. “无解”之谜（理论极限）
作者证明，为每一个可能的数学问题创建一个完美程序，其难度等同于解决数学中一个著名的未解之谜，即希尔伯特第十问题（该问题询问我们是否总能判断特定类型的方程是否有解）。

隐喻： 他们表明，要求计算机解决每一个可能版本的这个问题，就像要求它解开一个连最伟大的数学家都尚未破解的谜题。
结果： 因此，他们证明了编写一个“无循环”程序（简单的直线型食谱）来解决所有情况是不可能的。你需要循环（重复步骤）来处理复杂性。

2. “单输出”奇迹
虽然一般问题很难，但他们找到了一个“甜蜜点”。如果程序只需要产生一个单一数字作为输出（例如，仅找出三角形的高度），他们就创建了一个完美且完整的算法。

工作原理： 他们使用了两个经典的数学技巧：
- 实根隔离： 找出数轴上解必须存在的精确“区间”。
- 有理根定理： 一条将答案搜索范围限制在少量有限可能性列表中的规则。
结果： 对于单输出问题，他们的工具（称为NQSynth）保证如果答案存在则能找到它，或者正确地说它不存在。

3. “足够好”的通用解决方案
对于具有多个输出的问题（例如，同时找出高度和宽度），完美的解决方案太难保证。因此，他们构建了一个“可靠但不完整”的算法。

隐喻： 把这想象成一名侦探，他无法解决城市里的每一起犯罪，但非常擅长解决他遇到的那些案件。如果他们找到了一个解决方案，他们知道它是 100% 正确的。如果他们找不到，那可能只是时间不够，而不是因为不存在解决方案。
结果： 他们的工具NQSynth成功解决了许多其他最先进工具（如 CVC5）未能触及的困难数学问题，即使那些其他工具被给予了问题的“更简单”版本。

工具：NQSynth

团队构建了一个名为NQSynth的原型工具。

功能： 它接收一个复杂的数学规则，并编写一个 Python 程序，使用分数完美地遵循该规则。
性能： 在他们的测试中，NQSynth 解决了83 个困难基准中的 59 个，而次优工具仅解决了 26 个。它特别擅长处理“不可实现”的规范（即“不可能”的食谱），通过正确识别何时存在解决方案以及何时不存在。

总结

这篇论文是关于教导计算机成为诚实且精确的数学家。新方法教导计算机，当问题看起来不可能时不要放弃，而是：

使用精确分数以避免错误。
如果可能，解决问题。
如果不可能，自信地说“我做不到”。

他们证明，虽然为每一个场景提供“完美”的解决方案在数学上是不可能的，但他们可以构建一个工具，该工具对单变量问题完美工作，并对复杂的多变量问题表现卓越，击败了该领域当前的最佳工具。

技术摘要：非线性实算术的程序合成：超越可实现性

问题定义
本文致力于解决从非线性实算术（NRA）的无量化子理论规范中合成程序的问题。与传统的语法引导合成（SyGuS）不同，后者在规范“不可实现”（即存在某些输入值，使得没有任何输出能满足规范）时会失效，本文提出了一种新颖的合成目标。其目标是合成一个程序，对于任何有理数输入，要么产生一个满足规范的有理数输出，要么明确报告不存在此类输出（记为 $\bot$ ）。

为了避免固定精度浮点运算中固有的舍入误差（这种误差可能导致在近似评估时，原本有效的实数解失效），作者将域限制为有理数输入和输出。这定义了RPSQ（带理数输入和输出的实程序合成）问题类。合成后的程序允许包含循环、条件语句和赋值操作，并在有理数上运行。

理论难度与局限性
作者为该问题确立了重要的理论边界：

与希尔伯特第十问题的相互归约性：他们证明了 RPSQ 与有理数域上的希尔伯特第十问题（ $HTP_{\mathbb{Q}}$ ）是相互归约的。由于 $HTP_{\mathbb{Q}}$ 是数论中长期悬而未决的问题，这意味着针对 RPSQ 的通用且完备的合成算法很可能不存在。
无循环合成的不可能性：论文证明，RPSQ 无法仅使用无循环程序来解决。如果存在无循环解，则意味着有理算术理论允许量词消去，而这一结果已知是不可判定的（Robinson, 1959）。

方法论与算法
鉴于通用的不可判定性，作者提出了一种分层方法：

实数上的可实现性与有理数上的可实现性：他们表明，如果一个规范在实数上是可实现的，那么任何由现有 SyGuS 工具（在实数上运行）合成的程序，只要输入和输出是有理数，也作为有理数情况下的有效解。然而，反之则不成立；有理数的解并不一定意味着实数的解。
单输出（ $|Y|=1$ ）的完备且可靠算法：对于具有单个输出变量的规范，作者提出了一种可靠且完备的算法（算法 1）。该方法将问题分为两种情况：
- 严格不等式：利用**实根隔离（RRI）**寻找多项式符号保持不变的区间。通过在这些区间内采样有理点（利用有理数在实数中的稠密性），该方法找到了严格约束的解。
- 非严格不等式：对于位于边界上的解（非严格不等式变为等式的情况），算法采用有理根定理（RRT）。这使得能够枚举由边界条件导出的多项式方程的有限候选有理根集合。
  该算法将这些方法与量词消去（使用 QEPCAD）相结合，以确定解存在的弱前置条件。
通用情况（ $|Y|>1$ ）的可靠但不完备算法：对于多个输出变量，作者提出了算法 2（实现在工具NQSynth中）。这是一个可靠但不完备的过程，它迭代地将多输出问题分解为单输出子问题：
- 它查询 NRA 预言机（Z3）以找到一个满足的有理赋值（模型）。
- 它基于该模型固定除一个输出变量之外的所有变量，将问题简化为可由上述完备算法解决的单输出合成实例。
- 它构建一个决策列表（一系列 if-then-else 分支），其中每个分支对应于通过量词消去导出的特定前置条件。
- 该过程重复进行，通过否定已找到的解的前置条件来细化规范，直到规范变得不可满足或发生超时。

实现与实验结果
作者在名为NQSynth的原型工具中实现了他们的方法。他们将其与两种竞争方法进行了评估：

QEPCAD+CVC5：一种修改后的 SyGuS 流水线，首先计算实数上的弱前置条件，然后合成程序。
ModEnum：一种受 Monniaux 在线性算术方面工作启发的基于模型枚举的方法。

评估使用了两个基准集：

NRA 基准：来自 SMT-LIB 2024 存储库的 83 个改编基准（meti-tarski/Arthan, asin, zankl 系列）。
几何基准：51 个建模 2D 和 3D 几何关系（圆、环形区域、双曲线）的规范。

关键结果：

NQSynth 在 120 秒超时内解决了 83 个 NRA 基准中的 59 个和 51 个几何基准中的 33 个。
相比之下，QEPCAD+CVC5 解决了 26 个 NRA 基准和 16 个几何基准，而ModEnum 解决了 23 个 NRA 基准和 11 个几何基准。
值得注意的是，NQSynth 成功地为许多不可实现（或弱前置条件难以计算）的规范合成了程序，而 SyGuS 工具在这种情况下会完全失效。
实验强调，NQSynth 的主要瓶颈是量词消去步骤（QEPCAD），特别是对于较大的输入，而不是合成逻辑本身。

意义与主张
本文声称向从 NRA 规范进行程序合成的技术库中添加了一种新颖的技术。其主要意义在于：

处理不可实现性：它提供了一种实用的方法来合成能够优雅处理无解输入的程序，这是当前最先进的 SyGuS 工具所缺乏的能力。
有理数精度：通过针对有理数输入和输出，它避免了与浮点算术相关的舍入误差，确保了需要高精度的应用在数学上的正确性。
超越 SyGuS：该方法通过利用数论性质（RRT 和 RRI）而非仅仅依赖语法搜索或标准量词消去，解决了现有 SyGuS 工具无法触及的问题，即使对于可实现规范也是如此。

作者得出结论，虽然由于 $HTP_{\mathbb{Q}}$ 的难度，通用的完备解在理论上不太可能存在，但他们提出的可靠且不完备的过程提供了一种稳健的实用解决方案，在广泛的基准测试中显著优于现有方法。未来的工作建议研究无循环程序足以满足条件的情况，并减少对重型量词消去引擎的依赖。