💻 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 のような分数）を使用することにしました。

比喩：家を建てることを想像してください。浮動小数点数の数学は、わずかに曲がった定規を使うようなもので、壁が傾く可能性があります。有理数の数学は、すべての測定が正確なレーザー精度の設計図を使うようなものです。
トレードオフ：正確な数学は計算が遅いですが、ゼロの誤差を保証します。著者らは、「だいたい合っていればよい」のではなく、数学的に完璧なプログラムを望みました。

3 つの大きな発見

1. 「解けない」謎（理論的限界）
著者らは、あらゆる可能な数学的問題に対する完璧なプログラムを作成することは、数学の有名な未解決の謎であるヒルベルトの第10問題（特定の種類の方程式に解が存在するかどうかを常に判断できるかどうかを問うもの）を解くことと同じくらい難しいことを証明しました。

比喩：彼らは、コンピュータにこの問題のあらゆるバージョンを解くよう求めることは、最も偉大な数学者たちさえも解明できていないなぞなぞを解くよう求めるようなものだと示しました。
結果：このため、すべてのケースを解決する「ループなし」のプログラム（単純な直線的なレシピ）を書くことは不可能であることを証明しました。複雑さを処理するにはループ（反復ステップ）が必要です。

2. 「単一出力」の奇跡
一般的な問題は難しいですが、彼らは「絶妙なポイント」を見つけました。プログラムが出力として単一の数値のみを生成する必要がある場合（三角形の高さだけを求めるなど）、彼らは完璧で完全なアルゴリズムを作成しました。

仕組み：彼らは2つの古典的な数学のトリックを使用します。
- 実数根の分離：解が存在しなければならない数直線上の正確な「隙間」を見つけること。
- 有理根定理：解の探索を少数の有限な可能性のリストに制限する規則。
結果：単一出力の問題については、彼らのツール（NQSynth）は、解が存在すればそれを見つけ、存在しなければ正しくそれを言うことが保証されています。

3. 「十分良い」一般的な解決策
複数の出力（高さだけでなく幅も求めるなど）を伴う問題については、完璧な解決策を保証することは難しすぎます。そこで、彼らは「健全だが不完全な」アルゴリズムを構築しました。

比喩：これは、街のすべての犯罪を解決できないが、遭遇する犯罪を非常に上手に解決できる探偵のようなものです。もし解を見つけたなら、それが100% 正しいことを知っています。もし解を見つけられなければ、それは解が存在しないからではなく、単に時間がなかったからかもしれません。
結果：彼らのツールNQSynthは、他の最先端のツール（CVC5 など）が手をつけられなかった多くの難しい数学的問題を成功裡に解決しました。それらの他のツールが「より簡単な」バージョンの問題を与えられた場合でもです。

ツール：NQSynth

チームはNQSynthと呼ばれるプロトタイプツールを構築しました。

機能：複雑な数学の規則を受け取り、分数を使用してその規則を完璧に追従する Python プログラムを作成します。
パフォーマンス：テストにおいて、NQSynth は83の難しいベンチマークのうち59を解決し、次に良いツールは26しか解決できませんでした。特に、解が可能かどうかを正しく識別することで、「実現不可能な」仕様（「不可能な」レシピ）を処理する点で優れていました。

まとめ

この論文は、コンピュータに誠実かつ精密な数学者になることを教えるものです。問題が不可能に見えるときにあきらめるのではなく、新しい方法はコンピュータに以下を教えます：

誤差を避けるために正確な分数を使用する。
可能であれば問題を解決する。
不可能であれば自信を持って「これはできません」と言う。

彼らは、あらゆるシナリオに対する「完璧な」解決策は数学的に不可能であることを証明しましたが、単一変数の問題については完璧に機能し、複雑な多変数の問題については驚くほどよく機能し、分野内の現在の最高水準のツールを凌駕するツールを構築できることを示しました。

技術的概要：非線形実数算術におけるプログラム合成：実現可能性の限界を超えて

問題定義
本論文は、量化子なし非線形実数算術（NRA）の理論における仕様からプログラムを合成する問題に取り組みます。従来の構文誘導型合成（SyGuS）は、仕様が「実現不可能」（すなわち、仕様を満たす出力が存在しない入力値が存在する）である場合に失敗しますが、本研究は新しい合成目的を提案します。その目標は、任意の有理数入力に対して、仕様を満たす有理数出力を生成するか、あるいはそのような出力の存在を明示的に報告する（ $\bot$ で表記）プログラムを合成することです。

固定精度の浮動小数点演算に固有の丸め誤差（近似値で評価された際に有効な実数解が失敗する原因となる）を回避するため、著者は定義域を有理数入力および出力に制限します。これにより、有理数入力・出力を伴う実数プログラム合成（RPSQ）という問題クラスが定義されます。合成されたプログラムは、有理数に対して動作するループ、条件分岐、代入を含むことを許容します。

理論的難易度と限界
著者は、この問題に対する重要な理論的境界を確立しました：

ヒルベルトの第 10 問題との相互還元可能性：彼らは、RPSQ が有理数上のヒルベルトの第 10 問題（ $HTP_{\mathbb{Q}}$ ）と相互還元可能であることを証明しました。 $HTP_{\mathbb{Q}}$ は数論における長年の未解決問題であるため、RPSQ に対する一般的な健全かつ完全な合成アルゴリズムが存在する可能性は低いことを意味します。
ループなし合成の不可能性：本論文は、RPSQ がループなしプログラムのみでは解決できないことを示しています。ループなしの解が存在すれば、有理数算術の理論が量化子除去を許容することを意味することになり、これは既知の決定不能な結果（Robinson, 1959）に反します。

手法とアルゴリズム
一般的な決定不能性を踏まえ、著者は階層的なアプローチを提案します：

実数上の実現可能性と有理数上の実現可能性：彼らは、仕様が実数上で実現可能であれば、既存の SyGuS ツール（実数上で動作する）によって合成された任意のプログラムも、入力と出力が有理数である限り、有理数の場合の有効な解としても機能することを示しました。ただし、これは逆には成り立ちません。有理数に対する解は、必ずしも実数に対する解を意味するわけではありません。
単一出力（ $|Y|=1$ ）に対する健全かつ完全なアルゴリズム：単一の出力変数を伴う仕様に対して、著者は健全かつ完全なアルゴリズム（アルゴリズム 1）を提示します。このアプローチは問題を 2 つのケースに分割します：
- 厳密不等式：多項式の符号が不変である区間を見つけるために**実数根の分離（RRI）**を利用します。これらの区間内で有理数点をサンプリングすることにより（実数における有理数の稠密性を活用）、厳密な制約に対する解を見つけます。
- 非厳密不等式：境界上に存在する解（非厳密不等式が等式となる場合）に対して、アルゴリズムは**有理数根の定理（RRT）**を採用します。これにより、境界条件から導出された多項式方程式の候補となる有理数根の有限集合を列挙することが可能になります。
  このアルゴリズムは、これらを量化子除去（QEPCAD を使用）と組み合わせ、解の存在に対する最弱事前条件を決定します。
一般ケース（ $|Y|>1$ ）に対する健全だが不完全なアルゴリズム：複数の出力変数に対して、著者はアルゴリズム 2（ツールNQSynthに実装）を提案します。これは健全だが不完全な手続きであり、多出力問題を単一出力のサブ問題に反復的に分解します：
- NRA オラクル（Z3）にクエリを送り、有理数の充足割り当て（モデル）を見つけます。
- このモデルに基づいて 1 つの出力変数を除くすべての出力変数を固定し、上記の完全なアルゴリズムで解決可能な単一出力合成インスタンスに問題を縮小します。
- 各ブランチが量化子除去を通じて導出された特定の事前条件に対応する決定リスト（一連の if-then-else ブランチ）を構築します。
- 見つかった解の事前条件を否定して仕様を精緻化し、仕様が充足不可能になるか、タイムアウトが発生するまでこのプロセスを繰り返します。

実装と実験結果
著者は、NQSynthというプロトタイプツールにアプローチを実装しました。彼らはこれを 2 つの競合アプローチと比較評価しました：

QEPCAD+CVC5：実数上で最弱事前条件を計算し、その後プログラムを合成する、修正された SyGuS パイプライン。
ModEnum：線形算術に関する Monniaux の研究に触発された、モデル列挙に基づくアプローチ。

評価には 2 つのベンチマークセットが使用されました：

NRA ベンチマーク：SMT-LIB 2024 リポジトリから適応された 83 のベンチマーク（meti-tarski/Arthan, asin, zankl ファミリー）。
幾何学ベンチマーク：2 次元および 3 次元の幾何学的関係（円、環状領域、双曲線）をモデル化した 51 の仕様。

主要な結果：

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}}$ の難しさにより一般的な完全な解が理論的にはあり得ないものの、彼らの健全かつ不完全な手続きは、広範なベンチマークにおいて既存の手法を大幅に上回る堅牢な実用的な解を提供すると結論付けています。今後の研究として、ループなしプログラムで十分である条件の調査と、重厚な量化子除去エンジンへの依存度の低減が提案されています。