「48年前の数学問題」の正体は、1978年の数学オリンピックの幾何問題だった。121量子ビットの超伝導プロセッサーが初めてたどった、証明の3手

この記事には広告(Amazon アソシエイトのリンク)を含みます。

先に書いておくと、この記事は AI の Claude を使って書いています。今回取り上げるのは中国の大学のチームが量子コンピューターで行った研究ですが、「機械に数学の証明をさせる」という AI の中心的な課題を扱う記事ですので、その点はお含みおきください。

「量子コンピューターが48年前の数学問題を確かめた」。2026年9月17日に ScienceAlert がそう報じた研究は、浙江大学と清華大学のチームが9月13日に arXiv に公開した査読前の論文です。見出しだけ読むと、長いあいだ誰にも解けなかった問題に量子コンピューターが決着をつけたように見えます。中身は少し違います。問題は1978年の国際数学オリンピック(IMO)の第4問で、出題されたその年に高校生たちが解いた問題です。しかも量子コンピューターが担ったのは、証明の3手を選ぶところまででした。それでも論文は、これを「初めて」の実験だと言います。見出しとの落差を埋めながら、何が初めてだったのかを見ていきます。

1978年の第4問と、同じころに生まれた「呉の方法」

第4問はこういう問題です。AB = AC の二等辺三角形 ABC がある。その外接円(3つの頂点を通る円)に内側で接し、辺 AB と辺 AC にもそれぞれ点 F と点 G で接する円を描く。このとき、F と G の中点 H が三角形 ABC の内心(内接円の中心)になることを示せ。図は定規とコンパスで描けるくらい単純で、下の画像のような形になります。ただ、証明には角の関係を何段も正しくつないでいく必要があり、思いつきで片づく問題ではありません。


今回の論文には、もうひとつ同じ時代の名前が出てきます。幾何の定理を機械に証明させる古典的な手法「呉の方法」は、中国の数学者・呉文俊(ご・ぶんしゅん)が1970年代の終わりに発表したものです。図形の条件を座標で多項式に書き直し、変数を順番に消していって結論の式が 0 になるかを調べる、という方法で、人間の直感を使わずに証明が機械的に進みます。論文はこの呉の方法と、角の関係を扱う「全角法」の2つを量子回路に載せました。

正方形の対角線を、多項式の割り算で証明する

実験に使ったのは、121個の超伝導量子ビットを11×11の格子に並べたプロセッサーです。隣どうしは220個の可変結合器でつながれ、1量子ビットゲートの精度は99.9%以上、2量子ビットゲートは99%以上、読み出しは98%以上とあります。証明の回路は、このうち必要な量子ビットをつないで組みます。


呉の方法を試す題材に選ばれたのは、「正方形の対角線は直交する」という定理でした。頂点 A を原点に置き、B を (x1, 0)、C を (x3, x2)、D を (x5, x4) とします。AB ⊥ AD、AB ∥ CD、AD ∥ BC、AB = BC という正方形の条件がそれぞれ多項式になり、結論の AC ⊥ BD も多項式 G になります。あとは G を条件の多項式で順に「擬除算」(割り算の一種で、余りだけを取り出す操作)していき、x5、x4、x3、x2 と変数を1つずつ消していきます。4回目の余りが 0 になれば証明が終わります。

量子回路では、多項式を係数の形ではなく「いくつかの点で評価した値」の形で持ちます。変数の指数、評価する点、そこでの値をそれぞれ別の量子ビットの組に入れ、擬除算に必要な掛け算と引き算を量子ビットの上で行います。第1段階の回路は21量子ビット、77層で、1量子ビットゲート150個と2量子ビットゲート89個から成ります。測定は3,000ショットの実行を3,000回繰り返し、読み出した余りの多項式は理論どおり x2x4 − x1x3 でした。4段階目の余りはすべての係数が 0 になり、対角線が直交することが示されました。

ただし論文の Methods には、点ごとの値は古典計算機で前もって計算して回路に埋め込んであり、量子プロセッサーが実行したのは擬除算の算術の部分だと書いてあります。呉の方法を量子化すると、理論上は必要な問い合わせの回数を平方根の程度まで減らせるのですが、今回の回路の大きさではその利点は示せていない、とも論文自身が断っています。

量子回路が選んだ3手

呉の方法は、どの変数をどの順に消すかが最初から決まっています。IMO の第4問で試したのは、それとは違う「次の一手を探す」タイプの証明です。ここで使うのが全角法で、2本の直線のあいだの向き付きの角を基本の量として扱います。

まず問題を小さくします。H は F と G の中点なので、対称性から頂点 A の角の二等分線の上にあることは最初から分かります。残るのは、H が頂点 B の角の二等分線にも乗っていること。全角法で書けば、直線 HB と BA のあいだの角と、HB と CB のあいだの角を足して 0 になる、という式です。論文はさらに、2つの円が接する点を D として、仮定から導ける角の関係を3本に絞りました。この3本を順に当てはめると、HB と BA の角は HD と FD の角に、それは FD と DB の角に、それはマイナスを付けた HB と CB の角に書き換わり、目標の式にたどり着きます。3手の証明です。

量子回路が担ったのは、この3手で「どの関係式を使うか」を選ぶ部分です。回路は12量子ビットで、2つの量子ビットが行動(3本の関係式のどれを使うか)、5つが今の証明の状態、5つが書き換え後の状態を表します。調整できる「戦略回路」が行動の重ね合わせを作り、固定された「推論回路」がその行動に応じて状態を書き換え、「評価回路」が書き換えの良し悪しを損失として出します。損失が小さくなるように戦略回路のパラメーターを更新し、直近4回の損失のばらつきが0.005を下回ったら学習を止めて測定します。測定は1,000ショットを10回。いちばん多く出た行動と出力の状態が、その回の一手になります。

結果は、1回目に2本目の関係式、2回目に1本目、3回目に3本目が最も高い確率で選ばれ、出力の状態もそれぞれ理論どおりの角になりました。人が決めた順番ではなく、回路の学習で3手がそろったわけです。

ここまで読むと、見出しの印象がだいぶ変わります。候補の関係式は3本しかなく、その3本は古典計算機で仮定から導いたものです。選ぶ回数は3回。そして各回のあいだで証明の状態は測定され、次の回のために作り直されます。重ね合わせのまま3手を通して探索したわけではありません。論文はこれらの制限を「使える装置の資源によるもので、枠組みの構造によるものではない」と書いています。

速くもなく、新しくもない。それでも「初めて」

今回の2つの定理は、古典計算機なら一瞬で証明できます。IMO の幾何問題なら、Google DeepMind の AlphaGeometry のような古典計算機の上で動く仕組みが、もっと難しい問題をすでに解いています。速さの利点も、今回は示されていません。新しい定理が見つかったわけでもありません。

それでも論文が「初めて」と言うのは、推論の手順そのものを量子回路として実行した点です。これまでの量子コンピューターの実験は、数値の計算が中心でした。証明の状態や推論の規則を量子ビットに入れ、量子回路の中で書き換え、結果を読み出して証明として組み立てたのは、論文によればこれが最初です。量子自動定理証明の理論的な枠組みは先に提案されていましたが、実機での実証は報告がありませんでした。

この先は、状態を測定せずに次の回へ渡して重ね合わせを保ったまま探索すること、関係式の候補と推論の規則を増やすことが課題だと著者たちは書いています。どちらも、もっと大きく、もっと精度の高い装置が要ります。査読前の論文なので、結果の評価はこれからです。「48年前の問題を確かめた」という見出しは正しいのですが、確かめたのは問題の答えではなく、量子回路に推論をさせられるかどうかのほうでした。

関連する商品

この記事に関連する本や商品は、Amazon で探せます。

上のリンクから購入されると、このブログに紹介料が入ることがあります。

出典

コメント

このブログの人気の投稿

eclipseのコンソール出力の文字化けを直す方法

C++/CLIの型変換

一括画像変換