🤖 machine learning

FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks

本論文は、数学的推論ベンチマークにおける意味不変性の欠陥がモデルのランキングを歪め、集計精度と意味的一貫性の間に重大な乖離を露呈させることを明らかにする測定プロトコル「FormInv」を導入し、ベンチマーク設計の選択が暗黙のうちにどのモデルが優れていると見なされるかを決定することを示す。

原著者： Nishal Thomas, Noel Thomas

公開日 2026-05-29

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Nishal Thomas, Noel Thomas

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

以下は、論文「FormInv」を平易な言葉と日常的な比喩を用いて説明したものです。

大きなアイデア：「変形」テスト

数学の試験を受ける学生を想像してください。「4 の平方根は 0 以上ですか？」と質問すると、彼らは「はい」と答えます。次に、全く同じ質問を少し言い換えて、「0 は 4 の平方根以下ですか？」と尋ねます。

もしその学生が本当に賢ければ、両方とも「はい」と答えるはずです。しかし、最初の質問には正解し、2 番目の質問には間違えてしまったらどうでしょうか。

これがまさに、この論文が GPT-4o、Claude、DeepSeek といった最先端の AI モデルについて発見したことです。彼らは数学において驚くほど優れているにもかかわらず、驚くほど脆いのです。質問の「意味」を変えずに「形」だけを変えると、AI はしばしば混乱し、異なる答えを出してしまいます。

著者たちは、この不安定性を「意味的不変性のギャップ（Semantic Invariance Gap）」と呼んでいます。平易な英語で言えば、「AI は数学を理解しているのではなく、単に文のパターンを認識しているだけだ」ということです。

問題：「ひっかけ問題」の罠

この論文は、現在のベンチマーク（AI の標準的なテスト）は欠陥があると主張しています。なぜなら、それらは特定の 1 つのやり方だけで質問しているからです。まるで、ドライバーを直線の高速道路だけでテストしているようなものです。そこでは完璧に運転できても、同じルートでも車線が入れ替わった状態で運転を求められれば、衝突してしまうかもしれません。

研究者たちは以下のことを発見しました。

高いスコアは誤解を招く： AI は標準的なテストで 96% の正解率を得るかもしれません。しかし、同じ質問を異なる方法で尋ねると、AI が質問が同じものであることに気づかないため、その「96%」は大幅に低下します。
「順位逆転」： これが最も衝撃的な部分です。質問の「仕方」によって、勝者が変わってしまいます。
- 「順序 A」で質問すると、モデル X が勝ちます。
- 同じ質問を「順序 B」で尋ねると、モデル Y が勝ちます。
- これは、選手は同じなのにゲームのルールを切り替えるたびに優勝チームが変わってしまうスポーツリーグのようなものです。

解決策：「全会一致監査」

これらの欠陥のある質問をどうやって見つけるのでしょうか。著者たちは「FormInv」というプロトコルを作成しました。

これは、タレントショーの審査員団のようなものです。9 人の異なる審査員（AI モデル）が、特定の質問が混乱を招くか、あるいは欠陥があることに全員が同意すれば、それは審査員ではなく質問自体に問題がある可能性が高いのです。

プロトコル： 彼らはある質問を取り上げ、9 種類の異なる AI モデルに答えさせます。
発見： 9 人中 6 人が「言い換え（再構成）」された質問を間違え、一方で全員が元の質問に正解した場合、そのシステムは言い換えられた質問を「欠陥あり」としてマークします。
結果： 彼らは、既存のテストに含まれる「言い換えられた」質問の約 3% から 47% が、実際には数学的に誤っていたり、混乱を招いたりしていることを発見しました。AI が数学に失敗したのではなく、テストが AI に失敗したのです。

「フリーベンチマークなし」のルール

この論文は、大胆な主張を行っています。「完璧なテストなど存在しない」というのです。

9 種類の異なる車をランク付けしようとしていると想像してください。

速度でテストすれば、車 A が勝ちます。
燃費でテストすれば、車 B が勝ちます。
ハンドリングでテストすれば、車 C が勝ちます。

著者たちは、AI の数学テストでも同じことが起こると言っています。どの AI もあらゆる種類の言い換えに完璧なわけではないため、テストを設計する人がどの「種類」の質問を含めるかを選ぶことができます。質問を選ぶことで、彼らは密かに誰がレースに勝つのかを決めているのです。この論文は、なぜモデルが勝ったのかを理解できるように、この選択を透明化するためのツールを提供しています。

重要な要点

精度だけがすべてではない： モデルが 96% の精度を持っていても、質問を言い換えると半数の失敗に陥る可能性があります。これは、それが数学を真に「理解」しているのではなく、パターンに基づいて推測しているだけであることを意味します。
「不変性のギャップ」： これは、AI の一貫性を測定する新しいスコアです。AI が質問の尋ね方に関わらず、同じ質問に対して同じ答えを出せる場合、高い「不変性」スコアを持ちます。この研究で最良のモデルでも、一貫性は約 82% にとどまっており、5 問に 1 問程度で一貫性を欠いていました。
テストの改善： 著者たちは、複数の AI モデルが混乱するかどうかを確認することで、テスト質問が「欠陥あり」かどうかを自動的にチェックするツール（FormInv）を構築しました。彼らはこれを使って既存のテストを修正し、トップ AI モデルの順位付けを変更しました。

まとめの比喩

翻訳者をテストしていると想像してください。

古い方法： 翻訳者に「The cat is on the mat（猫はマットの上にいる）」をフランス語に翻訳するよう求めます。彼らは完璧にこなします。あなたは彼に A を与えます。
新しい方法（FormInv）： 翻訳者に「The mat has a cat on it（マットには猫がいる）」「Is the cat on the mat?（猫はマットの上にいるか）」「On the mat sits the cat（マットの上に猫が座っている）」を翻訳するよう求めます。
結果： 翻訳者は最初の文は正解しますが、他の文では失敗します。あなたは彼が実際にフランス語を理解しているのではなく、最初の文を暗記しただけだと気づきます。

FormInv は、誰が言語を真に理解し、誰が単にパターンを暗記しているだけなのかを見極めるために、2 番目のセットの質問を私たちに強いるツールです。

技術的概要：FormInv 数理解論ベンチマークにおける意味的不変性の測定プロトコル

1. 問題提起

大規模言語モデル（LLM）の数理解論に関する現在のベンチマークは、標準的な問題定式化に基づいて計算された集計精度指標に大きく依存している。本論文は、モデルの性能が質問の表現方法に依存しないという前提に立っているため、そのような指標は不十分であると主張する。著者らは、重要な「測定ギャップ」を特定している：モデルは標準的なベンチマークで高い精度を示すことが多いが、論理的に同等な言い換えに対して一貫した回答を生成する能力である意味的不変性を維持できていない。

本論文は、標準的なベンチマーク（例：GSM8K、MATH、MathCheck）が、言い換えの意味的同等性の厳密な検証を欠いていることを強調している。その結果、ベンチマークのランキングは、真の推論能力の尺度というよりは、特定の表現方法に起因する人工物である可能性がある。著者らは、この問題を形式化するために、心理測定理論、特に項目機能差（Differential Item Functioning: DIF）と一般化可能性理論を援用している。彼らは、モデルの回答が意味的に同等な言い換えに基づいて変化するならば、それは真の数学的理解の欠如を示し、代わりに表面的なパターン認識に依存していることを意味すると仮定している。

2. 手法

2.1 FormInv プロトコル

著者らは、意味的不変性を監査し定量化するために設計された測定プロトコルFormInvを提案する。このプロトコルは、以下の 3 つの中核的コンポーネントで構成される：

不変性ギャップ（IG）と意味的一貫性率（SCR）：
- IG： 言い換えの等価クラス全体にわたるモデルの二値回答の標準偏差として形式的に定義される。数学的には、 $IG(f, [x]_\sim) = \sqrt{p(1-p)}$ であり、ここで $p$ は等価クラス内での正解の確率である。IG が 0 であることは、完全な不変性を意味する。
- SCR： すべての言い換え形式に対してモデルが正解する定理の割合である。IG が分散を測定するのに対し、SCR は正解性と不変性の交差を測定する。
- コホランの Q 検定： $k > 2$ の言い換えファミリー全体での周辺均質性の統計的検定として使用され、モデルの失敗率がファミリーによって有意に変化するかを判定する。
8 分類の言い換え分類体系：
ベンチマークは、検証の厳密さによって分類される 8 つの異なる変換ファミリーに対してモデルを評価する：
- T1（形式的に証明可能）： ファミリー F4（表記）、F6（順序）、F7（展開）、および F8（同等性）。これらは Lean4/FOL 規則またはコンピュータ代数システム（CAS）による検証（例：SymPy）に依存する。
- T2（条件付き妥当）： ファミリー F1（構文）、F2（量化子）、および F3（受動態）。これらは型文脈に依存し、適用可能な場合はテンプレートまたは CAS によって検証される。
- T3（ヒューリスティック）： ファミリー F5（接続詞のバリエーション）。これらは自然言語のヒューリスティックに依存し、分野の専門家によるレビューを必要とする。
モデル間一致監査：
新たな品質管理メカニズムであり、超半数のモデル（例：9 モデル中 6 以上）が標準バージョンは合格しつつも言い換えバージョンに失敗した場合、その言い換えは意味的に誤っているとフラグが付けられる。これは、モデルの推論ではなく、言い換え自体の体系的な誤りが普遍的な失敗を引き起こすという仮定を利用している。

2.2 ベンチマーク構築

基盤： 評価には、数論、代数学、実解析などの分野にまたがるMathlib4（Lean4 検証済み）から厳選された 103 個の定理が使用される。
データセット： 主要なデータセット（FormInv v1）は、760 個のアイテム（103 個の定理 × 約 7.4 個の言い換え）を含む。拡張された「Track B」評価では、ntp-mathlib から 100 個のより困難な定理を使用し、811 個のアイテムとなる。
検証： 言い換えは GPT-4o によって生成され、多段階プロトコルによって検証される：代数ファミリーには CAS、表面ファミリーにはテンプレート保証、定義ファミリー（F7/F8）には 100% の人間専門家レビューが用いられる。

2.3 実験設定

本研究は、366〜811 個のアイテムに対して9 つの最先端モデル（GPT-4o、Claude Sonnet/Haiku、DeepSeek V3/R1、Gemini 2.5 Flash、Llama 3.3 70B を含む）を評価する。モデルは、厳格な TRUE/FALSE 制約付きのゼロショットモードで評価される。

3. 主要な結果

3.1 不変性ギャップ対精度

最も重要な発見は、集計精度と意味的一貫性の間の乖離である。

Claude Haiku 4.5 は 86% の精度を達成するが、**SCR は 50%**に過ぎず、正解の半分が言い換え間で不整合であることを意味する。
DeepSeek V3 は 96.4% の精度と82% の SCRを達成する。
10 ポイントの精度の差は、32 ポイントの SCR の差を隠している。論文は、精度のみが「構造的な失敗に対して憲法的に盲目」であると指摘している。
精度と平均 IG 間には強い負の相関（ $r = -0.415$ ）があるが、これは IG の定義によって代数的に駆動されており、特定ファミリーに対する不変性を保証するものではない（原文の相関値は -0.965 だが、Track B の記述と整合させるため文脈を確認。原文の 3.1 節では r = -0.965 と明記されているため、これを維持する）。→ 修正：原文の 3.1 節では $r = -0.965$ と明記されているため、これを維持する。精度と平均 IG 間には強い負の相関（ $r = -0.965$ ）があり、より精度の高いモデルは一般的に不変性が高いことを示唆しているが、この相関は IG の定義によって代数的に駆動されており、特定ファミリーに対する不変性を保証するものではない。

3.2 ランキングの逆転と相補性

モデルのランキングは安定しておらず、言い換えファミリーによって逆転する：

F6（比較順序）： GPT-4o はアイテムの 0.0% を失敗するのに対し、Claude Sonnet は 16.7% を失敗する。
F7（定義的展開）： Claude Sonnet は約 6% を失敗するのに対し、GPT-4o は 10.0% を失敗する。
この相補的な失敗パターンは、単一のモデルがすべてのファミリーをパレート支配していないことを意味する。したがって、ベンチマーク設計者は、勝者を決定するファミリーの重み付けを暗黙的に選択している。論文はこれを**「フリー・ベンチマークなし」の帰結**として形式化している：任意の目標ランキングに対して、それを実現する言い換えファミリー上の重み付け $\lambda$ が存在する。

3.3 品質監査の結果

モデル間一致プロトコルは、既存のベンチマークにおいて意味的に誤った言い換えを正常に特定した：

MathCheck 監査： MathCheck の 129 グループに適用したところ、4 つの意味的に誤った言い換え（3.1%）がフラグ付けされた。これらの誤りを除去すると、GPT-4o はランク 2 からランク 4 に転落し、Claude Haiku と DeepSeek V3 が浮上した。
FormInv v1 監査： プロトコルは、GPT-4o によって生成されたアイテム内で 11 個の誤りを特定した。これには、双条件の過剰適用、受動態の逆転、型文脈の剥奪が含まれる。これらの誤りは単一モデル評価では見えないが、一致性によって暴露された。

3.4 難易度レジーム依存性

より困難な定理を使用した「Track B」評価において：

精度と不変性の間の相関は弱まった（ $r = -0.415$ 、有意ではない）。
F5（接続詞のバリエーション）の特定の難易度は解消され、すべてのファミリーは類似した失敗率（28〜35%）でクラスター化した。
推論モデル（DeepSeek R1、o4-mini）は、困難な定理において最低の IG を示し、Chain-of-Thought による熟考が、定理が高度な推論を要求する場合にのみ表面への感受性を低下させることを示唆している。

4. 貢献

不変性フレームワーク： Doob の条件付き期待値定理と DIF 理論に基づき、SCRとIGを意味的不変性の主要指標として形式化する。検証の厳密さに基づき、言い換えファミリーを T1、T2、T3 の階層に分類する。
FormInv ベンチマーク： Lean4 検証済み定理から派生した 760 個以上のアイテムのデータセットであり、厳密なモデル間一致監査を用いて 9 つのモデルで評価される。
FormInvSelector： ファミリーごとの SCR プロファイルを使用して、特定のタスクレジーム（例：定義的推論対比較タスク）に対して期待失敗率が最低のモデルを推奨するアルゴリズム。
言い換え品質監査： モデル間一致（9 モデル中 6 以上が言い換えに失敗）が、意味的に誤ったベンチマークアイテムを検出する自動化された低コストな方法であることを実証し、ベンチマークの誤りとモデルの誤りを効果的に分離する。

5. 意義と主張

本論文は、FormInvが、測定不変性理論と DIF に基づく指標を形式的数理解論に適用した最初のプロトコルであると主張している。その意義は以下の 3 点にある：

隠れた欠陥の露呈： 標準的な精度指標は誤解を招く可能性があり、表面的な性能と真の意味的理解の間に「32 ポイントのギャップ」を隠していることを暴露する。
ベンチマークの完全性： ベンチマーク構築者が公開前に自らのデータセットを監査するためのツールを提供し、ランキングが欠陥のある言い換えの人工物となることを防ぐ。著者らは、「プログラム的に言い換えを生成する場合、どれだけのものが誤っているか分からない」と断言している。
レジームを考慮した評価： 単一の「最良」モデルという概念に挑戦し、ランキングがレジーム依存（言い換えファミリーと難易度によって変動）であることを実証する。論文は、ベンチマーク設計者が含めるファミリーを選択することで暗黙的に勝者を選定しており、FormInv がこの選択を明示的かつ監査可能にするものだと結論づけている。

著者らは限界について謙虚であり、すべての言い換えを Lean4 で完全認証することは今後の課題であり、現在の研究は 103 個の厳選された定理（Track B では 100 個のより困難な定理に拡張）に依存していると指摘している。彼らは、FormInv が既存の精度ベースの評価を置き換えるものではなく、補完する指標であることを強調している。