作者提出了一种推理系统的设计方案，该系统通过将两个命题分解为更小的组件并搜索逻辑冲突来检测它们之间的矛盾，而不是依赖 LLM 的直接判断。

  • 该系统将概率探索与形式化验证分离开来，以提高在有限生成预算下的效率。
  • 命题识别利用蕴含关系在不同逻辑结构之间映射对应内容。
  • 一种寻求冲突的搜索策略旨在比无向搜索更高效地找到同一主体的正形和负形。
  • 初始实现针对命题逻辑，输出 CONTRADICTION、CONSISTENT 或 UNKNOWN。

作者正在寻求讨论、批评、替代方案以及帮助实施或测试此假设的合作者。