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) を返し、思考の停止ポイントを明示します。