Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

あなたは、手がかりがどのように見方を変えるかによって意味が変わる言語で書かれた謎を解こうとしている探偵だと想像してください。これは、コンピュータサイエンスの一分野である**充足可能性モジュロ理論（SMT）**の世界です。SMTは、一連の論理的なルールが同時に真となり得るかどうかを判断しようとするソフトウェアのことです。これは、プログラムがクラッシュするかどうか、秘密のコードが解読可能か、あるいはロボットの経路が安全であるかどうかをチェックする、超スマートなパズル解決策だと考えてください。

ほとんどの場合、これらのパズルは単純な直線や単純な加算（$x + y = 5$ のようなもの）しか含まないため、簡単です。コンピュータはこの分野において驚異的な能力を持っています。しかし、非線形算術（$x \times y$ や $x^3$ のように、値が掛け合わされたり累乗されたりするルール）を導入すると、事態は一変します。突然、ルールは曲線を描き、ねじれます。そして、数学は非常に困難になります。実際、整数においては、これらすべてのパズルを解くための完璧で100%完全な手法を作成することは、数学的に不可能です。このため、コンピュータ科学者は、すべての不可能なケースを解決できるという保証はできないものの、迅速に答えを見つけるための巧妙なショートカットを用いる「十分に優れた」探偵を構築しているのです。

これから読む論文は、これまでのものよりも、このトリッキーで曲線的なパズルを解くのが得意な新しい探偵、qfn2lを紹介しています。著者であるチェコ工科大学の研究者たちは、従来のショートカットが特定の難しいパズル、つまり累乗（$x^3$ など）や混合積（$x^2y$ など）を含むパズルに対して苦戦していることに気づきました。彼らは、探偵の道具箱をアップグレードし、以前のモデルから逃げていた誤った推測を捕まえるための、よりタイトな網として機能する新しいルール一式を用意することにしました。

旧来の方法：解釈できない関数による推測

このアップグレードを理解するために、以前の探偵がどのように機能していたかを見てみましょう。例えば、$f(x, y)$ とラベル付けされた謎の箱があるとします。あなたはその中に何が入っているのか分かりませんが、同じ数値を入力すれば、同じ数値が出力されることは分かっています。旧来の方法では、$x \times y$ のようなあらゆる乗算を、この謎の箱として扱っていました。コンピュータは箱の値を推測し、それが理にかなっているかを確認し、もしそうでなければ、その推測を修正するためのルールを追加していました。

これは単純なケースではうまく機能しましたが、スイカの重さを知るために、単に「重い」とだけ知っているようなものでした。それはあまりにも曖昧すぎました。パズルに $x^3$ のような高い累乗が含まれる場合、旧来のルールは緩すぎました。探偵は値を推測し、コンピュータは「いいえ、それは適合しません」と言い、そして修正のために非常に弱いルールを追加しました。探偵は、答えを見つける前に時間が切れてしまうことが多く、何度も推測と失敗を繰り返さなければなりませんでした。

新しいトリック：割線による網の締め付け

この論文の著者たちは、これらの累乗を謎の箱として扱うのをやめ、代わりにそれらを新しい定数、つまり累乗の結果を表す単純な数値として扱うことにしました。しかし、本当の魔法は、これらの数値をチェックするための新しいルールにあります。

彼らは、任意の整数 $v$ に対して、関数 $x^k$（例えば $x^3$）は $v$ と $v+1$ の間で非常に予測可能な挙動を示すことを発見しました。彼らは**割線（セカント）**に基づいた新しいルールを作成しました。グラフ上の曲線を描いてみてください。割線とは、その曲線上の2点を結ぶ直線です。著者たちは、点 $(v, v^k)$ と次の整数点との間に直線を描けば、その直線が曲線の周りに非常にタイトな「フェンス」を作り出すことを発見しました。

ここでの比喩は以下の通りです：

• 旧来の方法： 探偵は、起こりうる答えの周りに、大きく緩い円を描いていました。描くのは簡単ですが、多くの誤った推測を招き入れてしまいました。
• 新しい方法： 探偵は、答えの曲線の周りを密接に包み込む、一連のタイトで直線的なフェンスを描きます。もし推測がこれらのタイトなフェンスの外側に落ちた場合、探偵は即座にそれが間違いであることを理解し、推測を内側へと押し戻すためのルールを追加します。

これらのフェンスは非常にタイトであるため、探偵は推測の回数を減らすことができます。これにより、特に立方や混合積を含むパズルにおいて、正解へと遥かに速く収束します。

「3つの立方体の和」への挑戦

新しい探偵が機能していることを証明するために、著者たちは「3つの立方体の和」と呼ばれる有名なクラスのパズルでテストを行いました。これらは、「3つの整数をそれぞれ3乗して足し合わせると、特定の数になる組み合わせを見つけられるか？」と問う問題です。

例えば、パズルは $x^3 + y^3 + z^3 = 79$ となります。

これは標準的なソルバーにとって悪夢です。数値は巨大になる可能性があり、関係性は複雑です。著者たちは、新しいソルバーである qfn2l を、既存の最高峰のソルバー（Z3、cvc5、MathSATなど）と比較しました。

• 他のソルバーは $x^3 + y^3 + z^3 = 79$ のパズルを解こうとしましたが、3分後に諦めました（タイムアウトしました）。
• 新しいソルバー qfn2l は、わずか 20秒 で答え（$x = -19, y = 35, z = -33$）を見つけ出しました。

結果：競争力のある新たな挑戦者

研究者たちは、標準ライブラリである SMT-LIB から集められた 25,444 個の膨大なパズルのコレクションに対して、彼らのソルバーを実行しました。その結果は以下の通りです。

1. 全体的なパフォーマンス： 新しいソルバーは、既存の最高のツールと同等の性能を持っています。合計で約 14,000 個のパズルを解決しており、これはトップクラスの性能に近いですが、あらゆる種類のパズルにおいて Z3 のような最強のツールをすべて上回ったわけではありません。
2. 得意分野： 新しいソルバーは、累乗と混合積が支配的なパズルにおいて圧倒的な輝きを放ちます。「MathProblems」ファミリー（3つの立方体の和を含む）において、約 53% のインスタンス（1,100件中 585〜587件）を解決しました。他のソルバーは、これらの特定のタイプの問題に対して著しく苦戦しました。
3. トレードオフ： 著者たちは、パズルの異なる部分が整合しているかどうかをより厳密にチェックしようとする（「合同公理」と呼ばれる）バージョンのソルバーをテストしました。その結果、この追加のチェックを行うことは、一般的なパズルにおいてソルバーの速度を低下させ、全体で約 1,600 件少ない解決数になることが分かりました。これは、ほとんどの問題において、タイトなフェンス（割線境界）があれば十分であり、すべての整合性ルールをチェックするという重い作業は必要ないことを示唆しています。

なぜこれが重要なのか

この論文は、解決不可能な問題を解決したと主張しているわけではありません。問題が数学的に決定不能であるため、あらゆるケースを解決できるコンピュータは存在しないことを著者たちも認めています。しかし、彼らは、これらの曲線的で非線形なルールを近似する方法を変えること、具体的には、タイトな割線ベースのフェンスを使用することで、「十分に優れた」探偵をよりスマートにできることを示しました。

彼らは、既存のエンジン（Z3）の上で動作するオープンソースのツールを構築し、よりスマートな戦略が、最も困難な整数のパズルにおいてブルートフォース（総当たり）アプローチに勝てることを証明しました。ソフトウェアがクラッシュしないことを検証したり、暗号プロトコルが安全であることを確認したりしようとしている人々にとって、この新しい手法は、舞台裏の数学をチェックするための、より速く、より信頼できる方法を提供します。

要約すると、著者たちは、乱雑で曲線的な問題を取り上げ、その周りにタイトな線を引くことで、コンピュータが以前よりもずっと速く真実を見つけられるようにしたのです。