AlphaProof Code 対 MathForm-8B：同じLeanパイプラインの2つの段階であり、2つの競合ではない

AlphaProof Codeの論文を注意深く読むと、発表では強調されていないある数字が目に飛び込んでくる。DeepMindの5人の研究者がSignalの検証に費やした4週間のうち、自動化できなかったのは最初の工程だった。人間の専門家が複数のモデルを組み合わせて作業しながらSignalのセキュリティ目標を形式的なLean仕様に翻訳し、証明作業が始まる前に専門家がその一つひとつをレビューした。そこがボトルネックだ。MathForm-8Bは、OpenBMBが2026年8月14日にHugging Faceで公開した80億パラメータの自動形式化モデルであり、まさにその工程を自動化しようとする直接的な試みだ。自然言語の数学的命題を受け取り、他の誰かが証明できる状態のLean 4定理文を出力する。両者を並べて見ても、二つの製品を比較しているのではない。数学とプロトコルセキュリティの違いによって隔てられた、一つのパイプラインの連続する二つの段階を見ているのだ。

パイプライン：作業が進む順に

実在のソフトウェアの形式検証には三つの仕事がある。第一に、何が真でなければならないかを決め、それを形式言語で書き下すこと。第二に、実装がそれを満たすことを証明すること。第三に、証明を機械的に検査すること。なぜなら、誤った証明は証明がないより悪いからだ。

MathForm-8Bは第一の仕事を、狭い入力クラスに対して行う。教科書風の数学的主張だ。「すべての実数 x について、x² は非負である」と与えると、Lean 4 でのインポート、型、定理ヘッダーを返す。返さないのは証明であり、著者らは証明探索は他人の問題だと明言している。報告されている数値はすべてベンダー報告による未再現のもので、6つのベンチマークにわたる構文チェック下での平均 Pass@8 が 88.06%、より厳しい一貫性チェック下では 72.37% である——この2つの数字の差こそが、構文的に妥当な文が求められた内容とは異なる意味を持つ頻度の正直な尺度である。

AlphaProof Codeはジョブ2と3に加えて、MathForm-8Bには手が届かなかった仕様化段階も担う。Signalのセキュリティ目標は、MathFormが訓練された意味での数学的主張ではない。それらはプロトコルに関する表明だ——デバイスが一時的に侵害される前後を通じてメッセージが保護され続けること、イニシエーターとレスポンダーが名乗るとおりの相手であること。それらをLeanに変換するには、どの8B自動形式化器も持たないプロトコル専門知識が必要だった。仕様が存在するようになると、証明作業は完全にエージェントに委ねられ、検査はLeanのカーネルとゲートキーパーエージェントに委ねられた。その際、comparatorをホールドアウト仕様コピーに対して

それぞれを実際に使うのにいくらかかるか

• 重み — MathForm-8B：ダウンロード可能、Apache 2.0、BF16 の safetensors シャード4つ、Qwen3-8B からファインチューニング。AlphaProof Code：なし。今回のリリースは、Lean による開発、AArch64 セマンティクス、および github.com/google-deepmind/code-verification にある libsignal バインディングです。

• 実行する — MathForm-8B：Transformers、vLLM、または SGLang。いずれも OpenAI 互換エンドポイントを公開し、所有するハードウェア上で動作します。AlphaProof Code：エンドポイントなし、API なし、ウェイトリストなし、価格なし。これは DeepMind がスケールする前に「継続的な研究」が必要だと述べている研究フレームワークです。

• 入力 — MathForm-8B: 自然言語で書かれた数学の命題。AlphaProof Code: 形式仕様と、それに対して証明したいバイナリ。

• 出力 — MathForm-8B: 未証明の Lean 4 定理文。AlphaProof Code: 機械検証済みの証明、またはコードが壊れている場合の反証。

• 人間によるレビュー — MathForm-8B: 出力されたステートメントをレビューしますが、一貫性が72.37%であるため、その多くをレビューすることになります。AlphaProof Code: 専門家が証明作業を開始する前にすべての仕様をレビューし、その後エージェントがコードベースの約1%を再確認対象としてフラグを立てます。

• 既知の制限 — MathForm-8B: 数学的記述のみで証明生成はなく、READMEでリンクされているコードリポジトリはリリース時点ではまだプレースホルダーでした。AlphaProof Code: SPQRヒーリングに対する耐量子保証はなく、ペイロードのプライバシーもなく、昇格ごとに1セッションで、MAC偽造バウンドは単一セッション内の25,000メッセージ付近で空虚になります。

MathForm-8Bが埋めなければならないギャップ

自動形式化器がSignalの仕様を書いて、研究者たちが初期に集中して費やす数週間を節約できたと言いたくなるのは自然だ。しかし論文自身の記述はそうではないと述べており、その理由は具体的である。プロトコルの仕様は主張の言い換えではない。敵対者モデルに関する選択なのだ。Signalの研究には、ハンドシェイク後にDiffie–Hellmanを破る量子攻撃者を用いるDolev–Yaoの記号的トラックと、古典的敵対者と具体的なバウンドを用いる計算的トラックがある。これら二つのトラックは同じコードについて異なる定理を述べており、どちらを選ぶかはセキュリティ上の帰結を伴う工学的決定である。「x² ≥ 0 を示せ」をLeanに変換するよう訓練されたモデルが、その判断を下すことはない。

自動形式化器がもっともらしく実行できるのは、その作業の機械的な部分である。散文で書かれたセキュリティ目標と既存のLean定義のライブラリが与えられたとき、プロジェクト固有の表現様式でステートメントの初稿を作成し、専門家が修正できるようにする。それは実際の節約になるが、見出しが示唆するよりもはるかに小さい節約だ。論文は、200を超える計算的項目と約35の記号的項目からなる仕様逸脱カタログを報告している。そのうち15項目はDouble Ratchet分析における欠落またはバグであり、これは人間によるレビュー段階が見つけたものである。ステートメントの草稿を作るモデルは、数学ベンチマークでのPass@8スコアではなく、そのカタログに対して評価される必要があるだろう。

2つの数値がまったく比較できない場合

MathForm-8Bの88.06%とAlphaProof Codeの650万行は異なるものを測っており、同じ列に並べるべきではない。一方は著者らが構築したベンチマークスイートに対するヒット率であり、他方は1つのターゲットに対して生成された証明の量である。ベンダーは、88.06%が構文チェックを用いていることを率直に認めている。これは弱い基準である——文はコンパイルできても誤った主張を形式化してしまう可能性があり、それが整合性の数値が16ポイント低い理由である。

AlphaProof Code の図で同様の趣を持つのは検証作業である：以前に修正済みだった Signal の2つのバグ、すなわち弱状態バグと小部分群バグが、隔離されたコピーに再導入され、どちらの場合も、システムはバグのある版がセキュリティ定理を満たさないことの機械検証済みの証明を生成した。これはネガティブテストであり、自動形式化ベンチマークに完全に欠けているのはまさにネガティブテストだ。MathForm-8B は「意図的に誤った命題を与えると、モデルがそう指摘した」という形式の結果を報告していない。

実際にそれらをどのように組み合わせて使うか

具体的には、そしてこれが比較の中で近い将来に実現可能な唯一の部分だが、自動形式化器に下書きを作らせ、強力な汎用モデルにその下書きを批判させ、証明エージェントに証明を試みさせる。各段階には異なる失敗モードがあり、3つすべてを1つのキー経由でルーティングするのが実用的な利便性だ。OrcaRouterでは、200を超えるモデルが、プロバイダー定価・マークアップ0%で単一のAPIの背後に並んでいる。そのため、同じ文を2つのモデルに送ってLeanの差分を取る仕様下書きループは、3つの契約と3つのSDKではなく、routing-DSLの呼び出しになる。自動フェイルオーバーは、選んだモデルが調子の悪い午後を過ごしている場合をカバーする。

そうしたもののどれも提供しないのは保証だ。MathForm-8Bは命題を与え、モデルたちは批評を与えるが、それを証明しなければならない何かが依然として必要だ。現時点で、実際にデプロイされたコード上でそのループを閉じる唯一の公開システムはAlphaProof Codeであり、それは販売されていない。

勝者を選ぶのではなく、両方の論文を読むべき理由

MathForm-8B は、狭い役割を持ち、実測された精度の上限が現実に存在する、有用な成果物だ。AlphaProof Code はワークフローの実証であり、そこから最も転用可能な知見は証明の量ではなく分業だ。仕様作業には人間と強力な汎用モデルが必要であり、証明作業にはエージェントチームとカーネルが必要で、その間の境界こそが難しさのすべてが宿る場所である。検証パイプラインを構築する者は誰でも、この分業を真剣に受け止め、自動形式化を第一段階のコストを下げる部分として扱うべきだ — それを置き換える部分としてではなく。

今月何をダウンロードすべきかを決めるチームに向けた、正直なまとめ:MathForm-8B は、Lean を扱っていて下書き支援が欲しいなら、Yes です。AlphaProof Code については、アーティファクトリポジトリと仕様逸脱カタログを読んでください。というのも、そのカタログは、本番コードの形式検証がまだ届かない領域について、どんな発表よりも多くを語ってくれるからです。