数学AIを、ひとつの脳から、
協調する系へ。

01 / ORIGIN

研究の出発点は、数学を文章生成だけで扱うことへの違和感でした。

数学の問題を解くとき、人は一つの表現に留まりません。図を見て関係を予想し、座標へ移し、 式を変形し、補題を立て、もう一度図へ戻ります。重要なのは文章の長さではなく、同じ数学的対象を 別の表現から見直せることです。

MORTRAは、問題文を「点・線・数・集合などの対象」「対象の間の関係」「証明したい結論」に分け、 それらを動かせる形で保持します。解答は文章を一度に生成するのではなく、小さな変換と証明を積み重ねて作ります。

一つの万能な解法を作るのではなく、異なる数学の見方が協力できる共通基盤を作る。

02 / SELF-ORGANIZATION

手掛かりは、多細胞生物の自己組織化です。

多細胞生物では、一個の細胞が身体全体を直接制御しているわけではありません。各細胞は局所的な情報を受け取り、 周囲と信号を交換しながら、組織として一貫した働きを作ります。MORTRAでは、この考え方を複数の記号推論器へ移します。

Sheaf-ADMMは、どの推論器に計算時間を配るか、どの途中結果を優先するかの調整に使います。 連続値の合意や多数決が数学的な真偽を決めることはありません。探索の調整と証明の検証を分けることが、この設計の要点です。

03 / COOPERATIVE PROVING

証明器は、競争するのではなく、途中の仕事を引き継ぎます。

幾何の演繹は図形の関係を素早く広げられます。座標法は関係を方程式へ変えられます。 Wu法とGroebner消去は、多項式として結論を確かめられます。どれか一つへ統一すると、他の方法の強みを失います。

MORTRAは、途中の命題を型付きの共通形式へ変換します。これにより、ある証明器が止まった場所から、 別の証明器が仕事を続けられます。最後に証明書を最初から再実行し、同じ結論へ到達したものだけを正答にします。

04 / FPGA

FPGA化の目的は、より深く探索するための時間を作ることです。

難しい問題では、補助点や補助線の候補が急速に増えます。測定すると、CPU時間の多くは最終的な証明ではなく、 「二点は同じではないか」「三点は一直線上にないか」といった単純な候補検査に使われていました。

MORTRAでは、候補の列挙と明らかに使えない候補の除外だけをFPGA向け回路へ移します。 動的な代数処理と最終的な証明はCPU側に残します。つまり、FPGAは答えを決める装置ではなく、 証明器が調べるべき候補を高速に送り出す装置です。

現在はRTLシミュレーションと論理合成まで完了しています。FPGA実機上の速度ではなく、回路として実装できることを確認した段階です。

05 / RESULT

IMO幾何は17題から25題へ。AlphaGeometryと同数です。

IMO-AG-30は、2000年から2022年までの国際数学オリンピック幾何30題を形式化した評価です。 基準となる記号推論器は17/30でした。MORTRAは複数の証明法と構成探索を統合し、25/30まで伸ばしました。

DeepMindのAlphaGeometryも同じ評価で25/30を報告しています。AlphaGeometryはニューラル言語モデルと記号推論の組み合わせ、 MORTRAは外部LLMを使わない記号推論器の協調という違いがあります。

06 / NEXT

証明から、作問、動的な作図、ロボットによる構成へ。

証明の過程を点、線、円、変換の履歴として保存できれば、そのまま図を動かし、立体を切断し、 ロボットアームへ作図命令を送れます。同じ仕組みを逆向きに使えば、条件を満たす新しい問題の探索にもつながります。

MORTRAが目指しているのは、答えを文章で返すだけの数学AIではありません。 数学的な対象を理解し、動かし、検証し、現実の作図までつなげられる計算基盤です。