让大模型调用专业求解器，解决逻辑推理难题。
MCP-Solver: Integrating Language Models with Constraint Programming Systems
- 通过协议让大模型调用约束求解器进行精确推理
- 支持Minizinc、PySAT、Z3等主流求解系统
- 迭代验证确保修改后结果仍符合逻辑规则
MCP-Solver通过模型上下文协议（MCP）将大语言模型（LLMs）与符号求解系统相连接，构建了一个开源的AI系统集成标准。该框架使大模型能够访问形式化求解与推理能力，弥补其在逻辑严谨性方面的不足，同时发挥其语言理解优势。系统实现了对约束编程（Minizinc）、命题可满足性（PySAT）及饱和理论上的可满足性（Python Z3）的支持。采用迭代验证的编辑方法，确保在模型修改过程中保持一致性，并支持结构化优化与精细化调整。
原文摘要 · Abstract (English)
The MCP Solver bridges Large Language Models (LLMs) with symbolic solvers through the Model Context Protocol (MCP), an open-source standard for AI system integration. Providing LLMs access to formal solving and reasoning capabilities addresses their key deficiency while leveraging their strengths. Our implementation offers interfaces for constraint programming (Minizinc), propositional satisfiability (PySAT), and SAT modulo Theories (Python Z3). The system employs an editing approach with iterated validation to ensure model consistency during modifications and enable structured refinement.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。