神经符号合规：集成LLM与SMT求解器实现金融法律自动分析

金融法规日益复杂，阻碍了自动化合规——尤其是在最少人工监督下维持逻辑一致性。我们提出一个神经符号合规框架，将大语言模型（LLM）与可满足性模理论（SMT）求解器集成，以实现形式可验证性和基于优化的合规纠正。LLM解释法规与执法案例以生成SMT约束，而求解器负责强制一致性，并在出现处罚时计算恢复合法所需的最小事实修改。与面向透明度的方法不同，我们的方法强调逻辑驱动的优化，提供可验证、法律上一致的推理，而非事后解释。在台湾金融监督管理委员会（FSC）的87个执法案例上评估，该系统在SMT代码生成上达到86.2%的正确率，推理效率提升超过100倍，并持续纠正违规行为，为基于优化的合规应用奠定了初步基础。