別々の方法で考える
図形の演繹、座標計算、Wu法、Groebner消去を、無理に一つの方法へ統一しません。
01 / TRY MORTRA
1問を解く。
2問をつなぐ。
片方だけなら入力した問題を解き、両方なら二つの構造を融合します。問題文、図、模範解答、検証結果までを一つの成果物として返します。
02 / RESULTS
IMO幾何 25 / 30。
IMO-AG-30は、国際数学オリンピックの幾何30題を集めた標準的な評価です。 MORTRAは外部LLMを使わず、複数の記号推論法を組み合わせて25題を証明しました。
IMO-AG-3025 / 30
17題から25題へ / 8題増 / 正答率 +26.7ポイント
探索全体701.4秒254.7秒
63.7%短縮 / 2.75倍高速化
候補の列挙69.83秒7.01秒
90.0%短縮 / 9.96倍高速化
同じIMO-AG-30で比較
MORTRAは初代AlphaGeometryと同じ25/30。AlphaGeometry2とTongGeometryは、この30題では満点です。
AlphaGeometry (2024)
25 / 30
金メダリスト平均
25.9 / 30
MORTRA
25 / 30
TongGeometry
30 / 30
AlphaGeometry2 (2025)
30 / 30
形式化された同じ30題で比較。AlphaGeometry2はこの30題では満点で、さらに広いIMO-AG-50（2000〜2024年の幾何全50題）でも42/50＝84%です。 幾何ではMORTRAは届いていません。ただしAlphaGeometryもTongGeometryも幾何専用で、数列・確率・積分・整数は扱えません。 MORTRAは同じ核で幾何以外も解きます。次の2つがその結果です。
幾何専用ではない
AlphaGeometryもTongGeometryも幾何しか扱えません。MORTRAは同じ核で振り分けます。
オリンピアード幾何（監査済み89題）53 / 89
ロシアARMO 11/12 ・ 中国TST 5/7 ・ IMO Shortlist 5/10 ・ CGMO 5/5
証明ファイルのハッシュが一致したものだけを数えています。
03 / ARCHITECTURE
権限を、面で分ける。
候補を出す面、解く面、順番を決める面、真偽を決める面、速くする面。情報は下へ流れ、権限は上へ戻らない。
途中結果を共有する
一つの方法で証明できた事実を、別の方法でも使える形へ変換して先へ進みます。
正しさは証明で決める
どの経路を調べるかは協調して決めますが、結論の正しさは多数決ではなく証明で確認します。
絞り込みを回路へ
候補検査の専用回路が1サイクル1件で動き、10,000通りでソフト実装と完全一致。論理合成まで通過済みです。数字は実機で測ってから出します。
04 / RESEARCH
LLMは、図で説明できない。
文を書いてから、別に図を描くから。
この研究について詳しくCOORDINATION
異なる証明法をつなぐ
演繹、座標、Wu法、Groebner消去が、それぞれの得意な方法で考え、途中結果を相互に利用します。
SELF-ORGANIZATION
局所の判断から全体解へ
一つの大きなモデルに判断を集中させず、複数の推論器が必要な情報だけを交換して答えへ進む方法を研究しています。
ADAPTIVE SEARCH
必要な経路だけを深く探す
簡単な探索から始め、解けない問題だけ計算を増やします。すべての候補を同じ深さまで調べる無駄を減らします。
HARDWARE
探索の絞り込みを、回路に落とした
候補検査の専用回路を設計し、1サイクル1件で流せる形にしました。10,000通りの入力でソフト実装と完全一致、Xilinx 7-seriesへの論理合成も通過。次は実機に載せて測ります。
数学の標準模型をつくる。
式・図・運動を、一つの構造の別の見え方として持つ。 下の立方体は飾りではありません。断面の多角形を毎フレーム計算しています。
同じ構造を、式でも図でも運動でも指紋を固定した実験規則名つきの導出列