Cognitive Dissonance DSPy provides a framework for multi-agent LLM systems to rigorously resolve belief conflicts. It targets developers and researchers seeking ground truth for disagreements, offering deterministic resolution via machine-checked proofs for formalizable claims, moving beyond heuristic-based arbitration.

How It Works

The system leverages DSPy for agent-based belief extraction and conflict detection. Identified conflicts are translated from natural language into the Coq formal specification language. A Coq prover then attempts to generate a machine-checked proof for the claim. This integrated loop of dissonance detection, NL-to-Coq translation, and online proving offers a novel approach to achieving verifiable consensus among LLM agents.

Quick Start & Requirements

• Requirements: Python 3.10+, Coq theorem prover (coqc command), Ollama or compatible API endpoint.
• Installation: Clone the repository, set up a Python virtual environment, and install dependencies via pip install -r requirements.txt. Coq installation instructions are provided for Ubuntu/Debian and macOS.
• Links: Repository: https://github.com/evalops/cognitive-dissonance-dspy.git. Examples: examples/mathematical_claims.py, examples/advanced_theorems.py, examples/comprehensive_demo.py.

Highlighted Details

• Supports formal verification of arithmetic, algebra, and basic algorithmic properties like sorting correctness.
• Demonstrates proof generation for claims such as "factorial 7 = 5040" in under 502ms.
• Achieves an 80% success rate on a set of 15 claims with an average proof time of 179.7ms.
• Resolves conflicts deterministically, avoiding reliance on voting or arbitration heuristics.

Maintenance & Community

• Primary community interaction point is GitHub Issues. No specific details on maintainers, sponsorships, or dedicated community channels (e.g., Discord/Slack) are provided in the README.

Licensing & Compatibility

• The project is licensed under the MIT license, which is permissive for commercial use and integration with closed-source projects.

Limitations & Caveats

• Initial scope is limited to formalizable claims within arithmetic, algebra, and simple algorithmic properties. Claims that cannot be formalized fall back to heuristic methods. Future work aims to expand coverage and improve error handling for formalization failures.