用定理证明增强 LLM：ProofOfThought 框架

基于 LLM 的推理系统，使用 Z3 定理证明，并支持多种后端（SMT2 和 JSON）。

• 双后端支持：可在 SMT2（默认）或 JSON 执行后端之间选择
• Azure OpenAI 集成：原生支持 Azure GPT-4o 和 GPT-5 模型
• 全面的基准测试：已在 5 个推理数据集（ProntoQA、FOLIO、ProofWriter、ConditionalQA、StrategyQA）上进行评估
• 高层 API：为推理任务提供简单易用的 Python 接口
• 批量评估流水线：内置数据集评估与指标计算工具
• 后处理技术：通过 Self-Refine、Self-Consistency、Decomposed Prompting 和 Least-to-Most Prompting 提升推理质量

从 PyPI 安装（推荐）

安装最新稳定版本：

pip install proofofthought

注意：包名为 proofofthought，但导入时使用 z3adapter：

from z3adapter.reasoning import ProofOfThought

从源码安装（开发）

如果要参与贡献或使用最新的开发版本：

git clone https://github.com/debarghaG/proofofthought.git
cd proofofthought
pip install -r requirements.txt

环境要求

• Python 3.12 或更高版本
• OpenAI API key 或 Azure OpenAI endpoint
• Z3 solver（通过 z3-solver 包自动安装）

环境变量

在项目目录中创建 .env 文件：

OPENAI_API_KEY=your-api-key-here

AZURE_OPENAI_ENDPOINT=https://your-endpoint.openai.azure.com/
AZURE_OPENAI_KEY=your-azure-key-here
AZURE_DEPLOYMENT_NAME=gpt-5  # or gpt-4o
AZURE_API_VERSION=2024-02-15-preview

你也可以不使用 .env 文件，直接将这些值设置为系统环境变量。

使用 OpenAI 快速开始

import os
from dotenv import load_dotenv
from openai import OpenAI
from z3adapter.reasoning import ProofOfThought

# Load environment variables
load_dotenv()

# Create OpenAI client
client = OpenAI(api_key=os.getenv("OPENAI_API_KEY"))

# Initialize ProofOfThought
pot = ProofOfThought(llm_client=client, model="gpt-4o")

# Ask a question
result = pot.query("Would Nancy Pelosi publicly denounce abortion?")
print(result.answer)  # False

使用 Azure OpenAI

import os
from dotenv import load_dotenv
from openai import AzureOpenAI
from z3adapter.reasoning import ProofOfThought

# Load environment variables
load_dotenv()

# Create Azure OpenAI client
client = AzureOpenAI(
    azure_endpoint=os.getenv("AZURE_OPENAI_ENDPOINT"),
    api_key=os.getenv("AZURE_OPENAI_KEY"),
    api_version=os.getenv("AZURE_API_VERSION")
)

# Initialize ProofOfThought with your deployment name
pot = ProofOfThought(
    llm_client=client,
    model=os.getenv("AZURE_DEPLOYMENT_NAME")  # e.g., "gpt-4o" or "gpt-5"
)

# Ask a question
result = pot.query("Would Nancy Pelosi publicly denounce abortion?")
print(result.answer)  # False

批量评估

from z3adapter.reasoning import EvaluationPipeline, ProofOfThought

evaluator = EvaluationPipeline(proof_of_thought=pot, output_dir="results/")
result = evaluator.evaluate(
    dataset="data/strategyQA_train.json",
    question_field="question",
    answer_field="answer",
    max_samples=10
)
print(f"Accuracy: {result.metrics.accuracy:.2%}")

执行后端

ProofOfThought 支持两种执行后端：

# SMT2 backend (default) - Standard SMT-LIB 2.0 via Z3 CLI
pot = ProofOfThought(llm_client=client, backend="smt2")

# JSON backend - Custom DSL via Python Z3 API
pot = ProofOfThought(llm_client=client, backend="json")

有关如何选择后端的详细信息，请参阅 BACKENDS.md。

后处理技术

使用高级后处理技术提升推理质量：

# Enable Self-Refine for iterative refinement
pot = ProofOfThought(
    llm_client=client,
    postprocessors=["self_refine"],
    postprocessor_configs={"self_refine": {"num_iterations": 2}}
)

# Use Self-Consistency for improved reliability via majority voting
pot = ProofOfThought(
    llm_client=client,
    postprocessors=["self_consistency"],
    postprocessor_configs={"self_consistency": {"num_samples": 5}}
)

# Chain multiple postprocessors
pot = ProofOfThought(
    llm_client=client,
    postprocessors=["self_refine", "self_consistency"]
)

可用技术：

• Self-Refine：通过自我批判进行迭代优化
• Self-Consistency：对多条推理路径进行多数投票
• Decomposed Prompting：将复杂问题拆分为多个子问题
• Least-to-Most Prompting：从简单到复杂，逐步解决问题

完整文档和使用示例请参阅 POSTPROCESSORS.md。

系统架构

该系统分为两层：

• 高层 API（z3adapter.reasoning）：为推理任务提供简单易用的 Python 接口
• 底层执行（z3adapter.backends）：面向 Z3 的 JSON DSL 或 SMT2 后端

大多数用户应使用高层 API。

示例

examples/ 目录包含针对不同使用场景的完整可运行示例：

• simple_usage.py：OpenAI 基础用法
• azure_simple_example.py：简单的 Azure OpenAI 集成
• backend_comparison.py：比较 SMT2 与 JSON 后端
• batch_evaluation.py：在数据集上进行评估
• postprocessor_example.py：使用后处理技术

通过 pip 安装后运行示例

如果你通过 pip install proofofthought 完成安装，可以在任何位置参考上面的快速开始示例创建自己的脚本。examples 目录主要用于开发和测试。

在开发模式下运行示例

如果你克隆了代码仓库：

cd /path/to/proofofthought
python examples/simple_usage.py

注意：部分示例使用了 utils/azure_config.py 等辅助模块，这些模块只有从代码仓库根目录运行时才可用。

基准测试

你可以将这个代码仓库作为 LLM+Solver 方法的可靠基线。为了判断开发过程中是否破坏了现有功能，这套代码通常会使用 GPT-5，在 5 个数据集各自的前 100 个样本上进行基准测试。这些结果并非最佳成绩；使用相同工具并改进 prompt engineering，完全可以取得更好的结果。如果你通过修改 prompt 得到了更好的成绩，欢迎提交 PR。

要使用两种后端运行全部基准测试并生成结果，请执行：

python experiments_pipeline.py

该命令将：

• 运行全部 5 项基准测试（ProntoQA、FOLIO、ProofWriter、ConditionalQA、StrategyQA）
• 测试 SMT2 和 JSON 两种后端
• 在 results/ 中生成结果表
• 自动更新下方的基准测试结果部分

最后更新时间：2025-10-16 18:14:07

引用

如果这项工作对你有帮助，请考虑引用我们的论文。

@inproceedings{
ganguly2024proof,
title={{PROOF} {OF} {THOUGHT} : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning},
author={Debargha Ganguly and Srinivasan Iyengar and Vipin Chaudhary and Shivkumar Kalyanaraman},
booktitle={The First Workshop on System-2 Reasoning at Scale, NeurIPS'24},
year={2024},
url={https://openreview.net/forum?id=Pxx3r14j3U}
}

@inproceedings{
ganguly2025grammars,
title={Grammars of Formal Uncertainty: When to Trust {LLM}s in Automated Reasoning Tasks},
author={Debargha Ganguly and Vikash Singh and Sreehari Sankar and Biyao Zhang and Xuecen Zhang and Srinivasan Iyengar and Xiaotian Han and Amit Sharma and Shivkumar Kalyanaraman and Vipin Chaudhary},
booktitle={The Thirty-ninth Annual Conference on Neural Information Processing Systems},
year={2025},
url={https://openreview.net/forum?id=QfKpJ00t2L}
}