概念
SMT求解器
自动判定一阶逻辑公式可满足性的工具，常用于验证循环不变量和路径条件，代表工具有Z3、CVC5。
时间轴 (近 90 天)
10月30日
LinguaArray在有限时间内与LLM交互，然后回退到后端求解器，确保LLM的引导是增强而非替代。
待验证50%
10月30日
LLM的输出不被信任为证明，而是作为启发式建议，由求解器进行最终验证，以保持求解器的健全性。
待验证50%
10月7日
SAT/SMT 求解器专门用于判断布尔或算术约束的可满足性，能在搜索空间中高效找到反例或证明无解
待验证50%