docs/benchmarks.md

# AXIS Benchmark Set (Signature Questions)

このドキュメントは、AXIS の推論能力を評価するための「看板問題」を定義します。これらの問題は LLM 単体では間違えやすく、AXIS の構造推論（Lattice Cross / Rule-based Simulation）が必須となるものです。

---

## 1. 様相論理：S5フレームの推論 (Modal Logic S5)
**【設問】** フレーム R が反射的 (reflexive)、推移的 (transitive)、かつユークリッド的 (euclidean) である場合、常に成り立つ式はどれか。
A. □A -> □□A
B. ◊A -> □◊A
C. □A -> A
D. 上記すべて (S5公理系)

**期待される AXIS の挙動:**
- `frame:reflexive`, `frame:transitive`, `frame:euclidean` を全て抽出。
- `modal_reflexive_axiomT`, `modal_transitive_axiom4`, `modal_euclidean_axiom5` が全てヒット。
- **結論:** Choice D

---

## 2. トポロジー：高次元球面の反証 (Topology Refutation)
**【設問】** 次の主張のうち、論理的に棄却（反証）できるものはどれか。
A. n > k のとき、π_n(S^k) は常に有限群である。
B. n < k のとき、π_n(S^k) は常に 0 である。
C. すべての n に対して、π_n(S^1) は常に Z と同型である。

**期待される AXIS の挙動:**
- `refute_mode: ON` を検知。
- A に対して `topo_refute_n_gt_k_always_finite` ルールが反証（Refutation）を生成。
- C に対して `topo_refute_s1_all_Z` ルールが反証を生成。
- **結論:** Choice A & C

---

## 3. ハイブリッド論理：複雑なフレームの特性 (Hybrid Logic H1)
**【設問】** Serial かつ Transitive だが、Reflexive でも Euclidean でもないフレームにおいて、Hybrid Logic の式として妥当なものはどれか。
A. @i □ p -> @i p
B. @i ◊ p -> @i □ ◊ p
C. @i ◊ T ∧ (@i □ p -> @i □ □ p) ∧ @i ¬@i □ i
D. @i ◊ j ∧ @j ◊ k ∧ @i ¬ ◊ k

**期待される AXIS の挙動:**
- `logic:hybrid`, `frame:serial`, `frame:transitive`, `frame:not_reflexive`, `frame:not_euclidean` を抽出。
- `hybrid_characterize_serial_trans_notrefl_noteucl` ルールが発火。
- **結論:** Choice C

---

## 4. なぜ LLM ではなく AXIS なのか（LLM の失敗例）
- **幻覚 (Hallucination):** LLM は π_3(S^2) を 0 だと答えたり、有限群だと思い込む傾向がありますが、AXIS は DB の証拠に基づき「ℤ（無限群）である」という反例を保持します。
- **混合 (Mixing):** LLM は推移性とユークリッド性を混同しやすいですが、AXIS は `requires` 条件により、プロパティが揃わない限りルールを適用しません。
- **説明への逃げ:** 証拠がない場合に LLM は「文脈によります」と濁しますが、AXIS は `WAIT (insufficient_evidence)` を返し、思考の停止ポイントを明示します。