ハクソク

世界を動かす技術を、日本語で。

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

233日前原文(github.com)

概要

ProofOfThought は、 Z3定理証明 と LLM を組み合わせた推論フレームワーク。 OpenAI API を利用し、自然言語クエリに論理的な答えを返す仕組み。 バッチ評価 や 簡単なインストール方法 を提供。 高レベルAPIと低レベルDSLの 2層アーキテクチャ を採用。 詳細やサンプルは examples/ ディレクトリや arXiv論文 で確認可能。

ProofOfThought：LLMとZ3による推論フレームワーク概要

  • ProofOfThought ：大規模言語モデル（LLM）と Z3定理証明器 を連携した推論システム
  • 自然言語クエリ を入力し、論理的根拠に基づく回答を生成
  • OpenAI API を利用したLLMクライアントの設定
  • z3dsl.reasoning モジュールによる高水準な推論API提供
  • バッチ評価 機能で複数クエリの一括検証が可能

クイックスタート手順

  • OpenAIクライアント の初期化
    • from openai import OpenAI
    • client = OpenAI(api_key="...")
  • ProofOfThoughtインスタンス の作成
    • from z3dsl.reasoning import ProofOfThought
    • pot = ProofOfThought(llm_client=client)
  • クエリ実行と回答取得
    • result = pot.query("Would Nancy Pelosi publicly denounce abortion?")
    • print(result.answer) # 出力例: False

バッチ評価手順

  • バッチ評価パイプライン の利用
    • from z3dsl.reasoning import EvaluationPipeline
    • evaluator = EvaluationPipeline(pot, output_dir="results/")
  • データセット指定による評価実行
    • result = evaluator.evaluate(dataset="strategyqa_train.json", max_samples=10)
    • print(f"Accuracy: {result.metrics.accuracy:.2%}") # 精度表示

インストール方法

  • 必要パッケージのインストール
    • pip install z3-solver openai scikit-learn numpy

アーキテクチャ

  • 2層構造アーキテクチャ
    • 上位層：z3dsl.reasoning（高レベルAPI、Pythonインターフェース）
    • 下位層：z3dsl（JSONベースのZ3定理証明器インターフェース）
  • 一般ユーザー は高レベルAPI利用を推奨

追加情報・サンプル

  • examples/ ディレクトリでAzure OpenAI対応例も含むサンプルを提供
  • 詳細情報・論文 ：
    • arXiv論文：https://arxiv.org/abs/2409.17270

参考リンク

  • arXiv:2409.17270 （ProofOfThoughtの詳細な技術解説）

Hackerたちの意見

面白いアプローチだね。うちのチームも、ビジネスオペレーションのポリシーをLEANでエンコードする似たようなプロトタイプを作ってるよ。まずは内部のナレッジベース（GoogleドキュメントやWikiページ）をLLMを使ってLEANに変換するんだ。それからソルバーを使って一貫性を確認する。Wikiページが変更されたら、またそのプロセスを実行して、基本的にはプロセスのリンターみたいな感じ。プロトタイプの段階を超えたとは言えないけど、LEANへの変換にはエンジニアが目を通す必要があるからね。でも、特に法律や財務のコンプライアンスが厳しい分野では、確かに期待できるアプローチだよ。

└

自動形式化のギャップは確かに埋めるのが難しいね。私たちは、NeurIPS 2025の論文で、明確に定義された文法における自動形式化の不確実性定量化を探求したよ: https://arxiv.org/abs/2505.20047 。もしもっと詳しく話したいことがあれば、気軽にチャットしよう！

└

そのポリシーの例を教えてもらえる？ Leanに適用できるような、現実世界で十分に定義されたものを思いつくのが難しいんだ。

└

それはすごくクールだね。矛盾する指針を体系的に特定するのに超役立ちそう。

リポジトリの詳細はあまりないね、掘り下げないといけない。これは、言及された論文のためのアーティファクトとしての意味合いがあるのかも。間違ってなければ、これは主にLLMに実際のクエリを「論理的に」表現するZ3プログラムを生成させるためのAPIだね。これによって生じる「監視」は、評価される論理的な命題を文字通り読む能力と、ソルバーを実行してそれが成り立つかどうかを確認することだよ。自然に疑問が浮かぶのは、誰が一連のSMTルールを手動で読んで、実際の理解と照らし合わせて正確にダブルチェックできるのかってこと。定数をダブルチェックするのは誰？ LLMが誤って（あるいは意図的に、目標を達成するために）論理的にも現実的にも不健全な事実やルールを追加するのをどう防ぐの？ 論文では論理ベンチマークで*51%*の誤検出率が報告されてる！ これは驚くほど高い数字で、LLMが論理モデルに弱いか、常に不健全なものを生み出していることを示唆してる。残念ながら、これがどのように評価されているのか、そして何が不足しているのかについては情報が少ないね。

└

そうだね。論文は昨年、GPT-4oで書かれたものだよ。それ以来、新しいモデルでずいぶん良くなった。例えば、https://arxiv.org/pdf/2505.20047 のタブ1では、テキストのみとSMTのみのパフォーマンスを比較してる。o3-miniは、テキストの推論をSMTでうまく反映してるし、Gemini Flash 2.0とも比較できる。このことは、ページ29の図14、15で見ることができるよ。AWSの自動推論チェックのような商業用製品では、ドメインからモデルを構築して（例えばPDFポリシー文書から）、正確性をクロスチェックして、回答生成の際には、LLMからのQ/Aペアがポリシーに従っているかをソルバーを使って確認するだけなんだ。これにより、99%を超える健全性保証を提供できる。つまり、サービスがQ/Aペアがポリシーに対して有効または保証されていると言った場合、99%以上の確率で正しいってことだよ。 https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-...

これは非常に興味深い研究分野だね。数年前に、論理と確率的論理推論エンジンを使って、結論が前提から導かれることを確認するようなことをしたよ。エージェントを使って、ドメイン知識を合成、形式化、批判することもやった。もちろん、これは万能ではないけど、ある程度の正確性は確保できると思う。シンボリズムやエージェントを「判定者」として導入するのは、今後の有望な方法だと思うよ。例えば、これを見てみて: https://arxiv.org/abs/2410.10934

└

うん！君の研究を読んだよ！すごく面白いね！この夏、AWS ARChecksで自動形式化のための似たような深い研究エージェントに取り組んでたんだ。似たようなパターンを使ってね。残念ながら、その研究は公開されてないけど、一般に利用可能な製品で遊んでみて！ [1] https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-...

└

エージェント/LLMを判定者として使うのはバイアスがかかっていて、ブートストラップにはいいけど、性能を人工的に制限しちゃう。能力が向上するにつれて、LLMを判定者として使うのは限界があるから、専門の人間の判定者か、決定論的オラクルに移行する必要があるよ。

面白い研究だね！DSLがどんな感じかリポジトリ見に行ったけど、わかりやすい例が見つけにくかったよ。READMEにサンプルを追加してくれたら嬉しいな。

└

こんにちは！興味を持ってくれてありがとう！それやってみるね。とりあえず、11ページ以降を見てみて。いろんな状況について説明してるよ！

LLMは結局、統計的な言語モデル（当たり前だけど）で、推論するものじゃないんだよね。論理プログラム、特にPrologのソースを生成するのが異常にうまくいくことに気づいたけど、[1]、多分Prologが記号的な自然言語処理のために導入されたから、トレーニングセットに翻訳の例が豊富にあるからかも。Z3の代替Datalog構文[2]をチェックする価値があるかもね、LispっぽいSMTLib構文の代わりに。

└

そうそう！Z3のDatalog構文はすごくいいよね！私たちは文法の論文でSMT[1]を使ったけど、これはソルバーとの相互運用性が一番高かったからなんだ。でも、私たちの技術はPROLOGでも動くよ；NeurIPSのレビューアーの要望でテストしたから。これもdatalog[2]で動くはずだと思うよ。

このプロジェクトを思い出させる驚きの体験がGemini 2.5 Proであったんだ。オンラインCASシステムを使って方程式のシステムを解く手助けをLLMに頼んでたんだけど、CASシステムが思ったように動かなくて。GeminiとCASシステムについて何度かやり取りした後、Geminiがそのまま解を教えてくれたんだ。LLMがこういうことが得意だとは思ってなかったから、驚いたよ。解にたどり着くためにPythonのsympyを使ったって言ってた。だから、曖昧なLLMともっと厳密なツールの組み合わせは強力な効果を持つんだね。

└

人間と同じように…難しい数値計算は得意じゃないけど、それを得意なコンピュータを発明できるんだよね。頑張れば、たくさんの数値計算を使ってテキストを予測するプログラムを作れるけど、難しい数値を処理するのはあんまり得意じゃない。で、そのプログラムが数値計算が得意なプログラムを作ったり使ったりする方法を予測できるんだ。

└

数学にはLLM+sympyがすごく好きなんだ。LLMにsympyのプログラムを書かせることで、記号操作が正しく行われてるって信頼できるんだよね。コードも人間とLLMの両方で繰り返し編集・改善できる便利なアーティファクトで、gitの履歴もあるし。テストやアサーションを実行して通過させることで、数学が正しいままである自信を築いて維持できる。sympyのコードからlatexに簡単にレンダリングするためのヘルパー関数も使ってる。量子消しゴム実験の背後にある数学の多くはこんな感じでやったよ。

└

ツールを使って問題を解決する手助けをしてくれるのは分かるよ。それはいいアイデアだし、期待以上にうまくいったみたいだね。でも、手元にあるからってCASの代わりにLLMを使って数学を正しくやらせようとするのは、バスのパスを持ってるからってバスでトラックレンタルの場所に行く代わりに、何十回もバスで引っ越しするようなもんだと思う。

これ合ってる？統計的なLLMの出力を形式論理モデルに通すってこと？それって「クズを入れたらクズが出る」ってことにならない？

└

それは主観的だね。過去数千年で発明されたものは全部クソだったって主張することもできるし、洞窟での生活の方がずっと楽だったかもしれないけど、短命だっただろうね。

└

形式論理は役に立つフィルターとして機能するよね。つまり、「クソが入れば、フィルターでクソが出る」ってこと。進化は完全にランダムな「クソ」な突然変異で動いていて、それが環境によって「フィルター」されるってことを忘れないで。

それこそ、次のAI冬が来る前にLLMが私たちに達成させてくれることを期待していることなんだよね。

つまり、核心的なアイデアはLLMを使って推論を構造化されたJSONのドメイン特化言語（DSL）でドラフトし、それを第一階の論理に決定論的に翻訳して、定理証明器（Z3）で検証することなんだ。最終的な答えが証明可能に含意される（さもなければ反例が出る）ってのが面白いよね。ただの説得力のある思考の連鎖じゃないんだ。

これ、めっちゃ面白い！ただ考えを声に出すだけじゃなくて、検証可能な日記を持ってるAIなんだね。まるで脳の中に暗号化された公証人がいる哲学者みたい。素晴らしい仕事だね！