ProofOfThought
LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON).
Features
- Dual Backend Support: Choose between SMT2 (default) or JSON execution backends
- Azure OpenAI Integration: Native support for Azure GPT-4o and GPT-5 models
- Comprehensive Benchmarks: Evaluated on 5 reasoning datasets (ProntoQA, FOLIO, ProofWriter, ConditionalQA, StrategyQA)
- High-level API: Simple Python interface for reasoning tasks
- Batch Evaluation Pipeline: Built-in tools for dataset evaluation and metrics
- Postprocessing Techniques: Self-Refine, Self-Consistency, Decomposed Prompting, and Least-to-Most Prompting for enhanced reasoning quality
References
- Z3 Theorem Prover — The underlying SMT solver used by ProofOfThought.
- OpenAI API — LLM provider for reasoning generation.
- Azure OpenAI Service — Azure-hosted LLM endpoint support.
- SMT-LIB Standard — The SMT-LIB 2.0 standard used by the SMT2 backend.
- Diataxis Documentation Framework — Framework guiding the structure of this documentation.
Acknowledgements
This work was supported by:
National Science Foundation (NSF) funded AI institute for Intelligent Cyberinfrastructure with Computational Learning in the Environment (ICICLE) (OAC 2112606)
Issue Reporting
If you encounter any issues, please report them via GitHub Issues. When filing an issue, please include:
- A clear description of the problem
- Steps to reproduce the issue
- Your Python version and OS
- Relevant logs or error messages