认知失调 DSPy：首个结合多智能体认知冲突检测、自然语言到 Coq 的形式化翻译及在线定理证明的系统，推动多智能体间矛盾解决从“争辩”到“证明”。

• 通过 DSPy 框架管理多智能体，自动抽取信念、归一化声明，精准识别认知失调。
• 将可形式化的声明转译为 Coq 定理，利用 coqc 编译及 coqchk 独立校验，实现机器验证。
• 解决方案不限于辩论或置信度投票，真正基于数学证明，结果具备可证伪性与严谨性。
• 当前支持算术、基础代数、简单算法性质（如排列与排序正确性）、一阶逻辑片段等。
• 性能表现优异：15 条声明约 80% 成功率，平均证明时间约 180ms，冲突解决无投票，保证确定性。
• 结构清晰：代理信念抽取→声明归一化→NL→Coq 翻译→Coq 证明→结果反馈闭环。
• 开源且易用，依赖 Python 3.10+、Coq 定理证明器及 Ollama API，支持快速上手与扩展。
• 未来规划涵盖更复杂的归纳、递归结构支持，增强错误提示，集成跨证明器验证，提升理论数据集基准表现。

打破多智能体系统仅靠辩论的局限，让机器证明成为信念冲突的最终裁决者，推动认知一致性达到新高度。

🔗github.com/evalops/cognitive-dissonance-dspy
#人工智能# #多智能体系统# #形式化验证# #定理证明# #认知失调#