ProofBench — AIハイブリッド・ベンチマーク: 記号計算 + 意味ベースの証明検証システム

 (github.com/Flamehaven)
1 ポイント 投稿者 flamehaven01 2025-10-17 | まだコメントはありません。 | WhatsAppで共有

TL;DR

ProofBenchは、記号数学（SymPy/Pyodide）とAIの意味解析（マルチLLMコンセンサス）を組み合わせた次世代のAIハイブリッド・ベンチマークおよび証明検証システムです。

証明の論理構造と意味的妥当性を同時に評価し、「見た目は正しい」論証を検出して、Logic Integrity Index (LII) で定量化します。

🎯 なぜ作ったのか

従来の証明検証器は

  • 形式論理ベースのため、あまりに厳格で実用的でないか、
  • 文法レベルで止まり、意味的な誤りを捉えられず、
  • 計算コストが高く、リアルタイムなフィードバックが難しいという問題があります。

ProofBenchは、「70% 記号 + 30% 意味」 のハイブリッド・アプローチにより、記号検証の厳密さとAIの柔軟な理解力を組み合わせたAIハイブリッド・ベンチマーク・フレームワークです。

📊 ProofBenchはこのような問いを検証します

  • 「AIは論理的一貫性を理解できるのか？」
  • 「証明構造をグラフベースで可視化すると、誤りのパターンが見えるのか？」
  • 「意味ベースの評価はどの程度信頼できるのか？」
  • 「記号・意味統合型ベンチマークは教育・研究・AI評価に有用か？」

🧩 AIハイブリッド・ベンチマーク指標

  • LII (Logic Integrity Index): 論理的完全性の中核指標
  • Coherence Variance: 複数モデル間の一致度
  • Symbolic Pass Rate: 数学的整合性の比率
  • Semantic Stability: 文脈的一貫性の維持率

これらの数値は、今後AIモデルの「論理力・一貫性・意味解釈力」評価のための共通基準へと発展させることができます。

🔍 アーキテクチャ概要

  • Symbolic Layer — SymPyをPyodideで実行し、ブラウザ内で決定的に検証
  • Semantic Layer — 複数LLMの応答をコンセンサスベースで評価
  • Hybrid Orchestrator — 70/30の基本重み付け（調整可能）、最終スコアを算出
  • LII Engine — 論理完全性指数 + 信頼区間を計算
  • Justification Analyzer — 依存グラフ + サイクル検出
  • Feedback Generator — 自然言語ベースの段階別評価レポートを生成

⚙️ 主な機能 (v3.7.2)

  • ハイブリッド検証エンジン: ブラウザ内PyodideでSymPyを実行 + マルチLLMコンセンサスベースの意味解析
  • LII (Logic Integrity Index): 0–100のスコアと95%信頼区間で論理的一貫性を定量化
  • Justification Graph: 証明間の依存関係を可視化し、循環論法を自動検出
  • Consensus Manager: 複数モデル間の一致度を計算し、コヒーレンスベースの平均スコアを算出
  • Natural Feedback Generator: 各段階の誤り・理由を自然言語でフィードバック
  • UI / Dashboard: 証明ステップごとの結果、グラフビュー、レポート、LIIスコアを可視化
  • Dockerワンクリック実行: docker run 1行ですぐに利用可能
docker run -p 3000:80 ghcr.io/flamehaven/proofbench:latest  
# → http://localhost:3000

🧱 限界

  • 意味レイヤーは複雑な言語的トラップの影響を受ける（記号レイヤーが緩衝）
  • LIIは正式な証明書（cert）ではなく、品質指標
  • 低スペック端末ではPyodideの初期起動コストがある

⚡ フィードバックが欲しい点

  • 70/30の基本重み付けは妥当か？（adaptive weightが必要かどうか）
  • LII + 信頼区間は教育・研究向けベンチマークとして有意義か？
  • 循環論法の検出は、実際の数学・論理課題で有用か？
  • ブラウザ（Pyodide）の性能ボトルネック改善アイデアは？
  • 「見た目は正しいが間違っている」証明サンプルの提供歓迎 🧩

🗺️ ロードマップ

  • セクションごとの可変重み付け（adaptive weighting）
  • 多様な証明フォーマットをサポート（Lean、Coq、Markdown数式など）
  • LII + グラフベースのレポート出力テンプレート強化
  • レッドチーム・ベンチを構築（「もっともらしいが誤っている」証明セットを公開）

🔗 リンク

✍️ 開発コメント

ProofBenchは、AIが「正解」ではなく**「正当性」**を理解できるかを試すためのツールであり、論理構造、意味的一貫性、説明可能性を1つのベンチマークに統合します。

これは単なる検証器ではなく、AIの思考力を測る新しい実験台になるはずです。

関連記事

まだコメントはありません。

まだコメントはありません。