ProofOfThought: Z3定理証明を用いたLLMベース推論

 (github.com/DebarghaG)
3 ポイント 投稿者 GN⁺ 2025-10-05 | 1件のコメント | WhatsAppで共有
  • ProofOfThought は 大規模言語モデル(LLM) と Z3定理証明器 を組み合わせ、強力でありながら 解釈可能な推論 を支援する
  • このプロジェクトは 自然言語クエリ に対して 正確で信頼性の高い推論結果 を提供する
  • 高水準のPython APIを通じて、開発者は 複雑な推論タスク を簡単に実装・実験できる
  • Z3DSL によりJSONベースの低水準DSLへのアクセスも提供され、柔軟なカスタマイズが可能
  • Sys2Reasoning Workshop NeurIPS 2024 掲載を通じて、最新研究成果の実用化の利点を示している

ProofOfThought オープンソースプロジェクト紹介

ProofOfThoughtは、大規模言語モデル(LLM)とZ3定理証明器を組み合わせた ニューロシンボリック(神経記号)プログラム合成方式 を採用するオープンソース推論ライブラリである。実世界の複雑な問題に対して 堅牢で解釈可能な推論結果 を提供する点が、実運用と研究の両面で重要な意義を持つ。

オープンソースの性質上、誰でも研究、サービス、開発などに自由に活用でき、既存の単純なLLMベース推論システムより 推論過程の検証とエラー解釈が容易 であるという利点がある。他の推論システムと比べて、自然言語入力 → 論理プログラムへの自動変換 → Z3ベース推論という構造的透明性が大きな特徴である。

システムアーキテクチャと主要構成

  • 高水準API(z3dsl.reasoning) :

    • 自然言語ベースの推論クエリを実行
    • 初心者でも簡単に適用できるPythonインターフェースを提供

  • 低水準DSL(z3dsl) :

    • JSONベースでZ3定理証明器にアクセス可能
    • 複雑なカスタマイズや自動化パイプライン構築に有利

主な機能例

  • LLMが入力されたクエリを論理式(シンボリックプログラム)に変換

  • Z3証明器を通じて真・偽(yes/no)または条件ベースの解釈結果を生成

  • 例:

    • クエリ: "Nancy Pelosiは中絶を公に非難するか?"
    • 結果: False(いいえ)

  • 評価パイプライン(EvaluationPipeline)を提供:

    • 大規模データセットに対するバッチ評価が可能
    • 精度などの自動レポート出力

適用・活用事例

  • 研究目的の 推論ベンチマーク自動化
  • LLMベースの知識グラフや高階論理問題の自動証明サービス
  • 複雑な政策クエリ、自然言語討論の自動判定など、多様なAIサービスへの適用可能性を持つ

研究上の意義と特徴

  • NeurIPS 2024のSys2Reasoningワークショップで発表
  • 既存LLMの限界(推論の不確実性)を補完する シンボリック解釈ベースの信頼性
  • 推論結果と根拠の透明性および解釈可能性は、実サービス開発において大きな強み

結論

ProofOfThoughtはLLMとZ3定理証明器の長所を組み合わせ、堅牢で解釈可能なAI推論インフラ を構築したい開発者や研究者に実質的な価値を提供する。プロジェクトのライセンスと構造はオープンソース生態系に適するよう設計されており、学術研究と産業活用の両面で魅力的である。

関連記事

1件のコメント

 
GN⁺ 2025-10-05
Hacker Newsの意見
  • Gemini 2.5 Proでの興味深い体験が語られている。オンラインCASシステムで連立方程式を解こうとしていたが、CASが期待どおりに動かなかったためGeminiに助けを求めたところ、Geminiが直接解答を提示した。Pythonのsympyパッケージを使ったと説明している。曖昧なLLMと厳密なツールの組み合わせが強力な効果を生む可能性があるという印象を共有している
    • 人間にかなり似ている感じがする。私たちは複雑な計算は苦手だが、非常に優れたコンピュータを作ってそれをうまくこなしている。そして莫大な努力の末に、数値計算を基盤としてそこそこテキスト予測はできるが難しい計算は不得手なプログラムも作った。結局、そのプログラムが数値計算に強いプログラムを作って使う方法を予測できるようになった
    • 数学ではLLMとsympyの組み合わせが本当に気に入っている。LLMにsympyコードを書かせれば、記号演算が正しく行われたことを信頼できる。コード自体が成果物として残るため、人間でもLLMでも段階的に修正・改善でき、git履歴などで管理も可能だ。テストや検証を通すことで数学的正確性への信頼も維持できる。sympyコードから簡単にlatexへ変換するヘルパー関数も使っている。最近のquantum eraser実験に関する数学作業もこの方法で進めている。githubリンク
    • ツールを使って問題解決の過程をLLMと一緒にたどるのは、妥当な方法だということは理解できる。実際、期待以上によく機能した。しかし、数学をLLMに処理させる方向へ誘導するためにCASを使わないのは、アパートの引っ越しを貨物トラックではなくバスで何度も往復して行うようなものだ、という比喩を挙げている。すでにバスパスを持っているからそうしているだけ、という見方だ
  • LLMは結局のところ統計的言語モデルであることが強調されている。論理プログラム、特にPrologのソースコードを生成するのは、期待以上にうまくいくという経験が述べられている。おそらくPrologが記号的自然言語処理に導入されてきたこと、そしてトレーニングデータセットにも翻訳サンプルが豊富にあるためだろう。Z3のDatalog構文をSMTLib構文の代わりに使ってみるのも検討に値する。関連デモ および Z3 Datalog構文 の参照が勧められている
    • Z3でのDatalog構文はかなり優れている。私たちはgrammars論文でSMTを使ったが、その理由は複数ソルバーとの互換性が最も高かったからだ。ただし、その方式がPROLOGでもうまく動くことはNeurIPSの査読過程でテストした。Datalogでも動作するはずだと考えている。論文リンク、datalogの例
  • 興味深いアプローチだと思う。私たちのチームも似たように、LEANでビジネス運用ポリシーをエンコードするプロトタイプを作った。内部WikiやGoogle Docsの知識ベースを、まずLLMがLEANコードに変換する。そして一貫性検証のためにソルバーを実行する。Wikiが更新されるとプロセス全体が再実行され、一種のプロセスLinterとして機能する。ただし、LEANへの変換自体にエンジニアのレビューが必要だったため、プロトタイプ段階にとどまった。それでも、法務・財務コンプライアンスが求められる分野では有望な方法だ
    • 自動形式化の壁が本当に高いことに言及している。私たちのNeurIPS 2025論文では、よく定義された文法を対象に自動形式化の不確実性を定量化して分析した経験を共有している。論文リンク 詳しい議論を望むならいつでも連絡してほしい
    • LEANとは何か気になる人向けに紹介している。Microsoftが作ったLean Theorem Proverである。プロジェクトリンク
    • 実際の例が気になる。現実の世界で、LEANで定義できるほど正確に記述されたポリシーとはどのようなものか、例を聞いてみたい
    • この方法は、矛盾したガイドラインを体系的に特定できる点が非常に有用そうだ
  • 非常に興味深い研究分野だ。数年前、論理および確率ベースの推論エンジンを使って、前提が結論へ適切につながっているかを検証したことがある。また、agentを使ってドメイン知識を合成・形式化・批判させたこともある。銀の弾丸ではないが、ある程度の正確性は担保できた。ある程度の記号性とagent-as-a-judgeの概念が将来有望だと思う。参考論文
    • その研究は読んだ。かなり素晴らしい。私も最近、AWS ARChecksでautoformalizationエージェントを作った経験がある。まだ非公開だが、一般に利用可能な製品もあるので参考になるはずだ AWSブログ
    • Agent/LLMを判定者として使うのはバイアスがあり、ブートストラップ用途にしか適さないと考えている。性能が十分に高まるとLLM判定者が人工的な限界になってしまうため、結局は人間の専門家判定者か決定論的オラクルへ移行すべきだという立場だ
  • RHELのknife-edge rolling kernelがproof of conceptに使われていることに言及している
  • リポジトリには詳しい説明が不足していると感じた。論文の補助成果物という位置づけなので、それもあり得る。本質的には、LLMにZ3プログラムを生成させようとするAPIのように見える。現実世界のクエリを論理的に表現するよう誘導し、事実、推論規則、目標をすべて含める。監督機能は、論理記述文を直接読み、ソルバーを実行して真偽を確認できるようにする点にある。疑問に思うのは、SMT規則を誰が逐一読んで実際の観点と照合できるのか、定数値は誰が検証するのか、そしてLLMが誤って、あるいは目標達成のために、論理的または現実的にずれた規則を追加しないのか、ということだ。論文では論理ベンチマークに対して 51% のfalse positiveを記録しており、これは驚くほど高い数値で、LLMが論理モデリングに弱いか不完全な規則を生成している兆候だと解釈している。評価が乏しく、なぜそうなるのか明確に説明できていない
    • この論文は昨年GPT-4oで書かれたもので、最新モデルでは状況が大きく改善していると主張している。たとえば最近の論文 のTable 1では、テキストベースとSMTベースの性能を比較している。o3-miniはtext reasoningとSMT上の結果をうまく一致させている。商用製品であるAWS Automated Reasoning Checksでは、ドメインモデルを作成して検証し、回答生成段階ではLLMのQ/Aペアがポリシーに準拠しているかを厳格なソルバー検証にかける。これにより、Q/Aペアのポリシー関連妥当性を99%以上保証できることが強調されている AWSブログ
  • 自分の解釈が正しいかを問う質問だ。LLMが出す確率的な出力が論理モデルへ渡される構造なら、「ゴミを入れればゴミしか出てこない」のではないか、という疑念を示している
    • 形式論理がフィルターの役割を果たす。つまり「ゴミを入れれば、フィルタリングされたゴミが出てくる」ということだ。進化もまた、無作為な「ゴミ」突然変異が自然環境でふるいにかけられるのと同じだ、という比喩を挙げている
    • 常に「ゴミ」が出てくるわけではない、という主張だ。かなりの頻度で有用な出力を生むからこそ意味がある
    • 主観的な評価の問題だ。過去数千年に人類が作ってきたものも、すべてゴミだと言えてしまうかもしれない。突き詰めれば、洞窟で暮らしていた生活のほうが単純だったかもしれない
  • AIが考えるだけでなく、検証可能な日誌を残すという点がとても興味深い。まるで暗号学的な公証人を伴って哲学者が生きているようだ。本当に驚くべき仕事だ
  • 中核となるアイデアは、LLMが推論過程を構造化されたJSON DSLとして下書きし、それを決定論的に一階述語論理へ変換してZ3で定理証明を試みるという点にある。したがって最終出力は、証明可能な結論、または反例になり、説得力だけのあるテキストチェーンとは異なることが強調されている
  • 興味深い研究だ。DSLの例が気になってリポジトリを確認したが、明確な例を見つけるのが難しかった。READMEにサンプルコードスニペットがあるとよいと思う
    • 関心に感謝する。まもなく追加する予定だ。それまでは論文の11ページ以降にさまざまな状況の説明がある 論文PDF