FormalJudge：面向智能体监督的神经符号范式
FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight
AI 导读
研究者提出 FormalJudge，一种用形式化验证监督 LLM 智能体行为的神经符号框架，以数学保证替代 LLM-as-a-Judge 的概率评分。该框架采用双向 Formal-of-Thought 架构，LLM 先自顶向下把人类高层意图分解为原子化可验证约束，再自底向上用 Dafny 规约和 Z3 SMT 求解证明合规。在覆盖行为安全、多领域约束遵循和智能体向上欺骗检测的三个基准上对 7 个智能体模型的实验显示，FormalJudge 相比 LLM-as-a-Judge 基线平均提升 16.6%；7B 判别模型检测 72B 智能体欺骗的准确率超过 90%，呈现弱到强泛化；迭代精化带来近线性的安全提升。