我们针对不均衡分布学习问题，构建了一种双效证明系统的交互式协议，该协议能够学习给定函数的最大傅立叶特征，学习类 AC^0 [2] 和 k-juntas。此外，我们还提供了一个用于布尔函数学习的新模型，样本复杂度与 n 无关。

Apr, 2024

该论文介绍了一种新的命题证明追踪格式，可以消除复杂的处理，从而实现有效（正式）证明检查。通过使用 C 实现证明检查器来证明该格式的好处。然后在 Coq 中形式化命题证明检查的理论，并从形式化中提取出该格式的一个正确性自证明的证明检查器。使用 280 个不可满足的实例对其性能进行了评估，并使用该格式正式验证了布尔勾股三元组猜想的最近 200 TB 的证明。

Oct, 2016

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

我们使用交互式定理证明器 Isabelle/HOL 对一种近似策略迭代算法在因子化马尔可夫决策过程上进行了形式验证。接着，我们展示了如何将形式化的算法细化为可执行的验证实现。所开发的实现方案经过了基准问题的评估，表明其实用性。作为细化的一部分，我们开发了经过验证的软件以认证线性规划解法。该算法基于丰富的形式化数学库，并推动了交互式定理证明器的现有方法的极限。我们讨论了验证项目的过程以及为形式验证所需的算法修改。

Jun, 2024

本文详细阐述了如何使用具备局部条件的概率 Hoare 逻辑对安全性进行推理，以 Vernam、El-Gamal 加密系统以及儿童游戏为例，证明了它们满足的安全属性并否定了不满足的属性。

Aug, 2021

该文主要研究 IQP 电路的量子计算和经典模拟问题，探究在有误差和噪声存在时的处理方法和纠错技术。

Oct, 2016

提出了一种交互协议，使客户端的输入、输出和计算完全保密，并且不需要任何量子计算能力或记忆，可用于经典或量子输入 / 输出；引入身份验证协议，使其可以检测到干扰服务器。此外，作者进一步将其推广到全经典客户端，以在不泄露私密信息的情况下完成盲量子计算。

Jul, 2008

该论文探讨了在模 $2^l$ 的整数环上进行安全计算的问题，提出了具有半诚实和恶意安全性的三方安全计算协议，并将其应用于安全服务器辅助的机器学习推理中，性能表现较好。

Dec, 2019

本文介绍了两种使用 SMT 解决带有线性有理成本函数最小化的一般性过程，并将其与标准最小化技术相结合。我们已将程序封装在 MathSAT SMT 求解器内，并成功与其他最先进的工具在 Linear Generalized Disjunctive Programming 领域中进行了实验。结果表明，我们的工具在这些问题上是非常有竞争力的，并且在许多情况下表现更好，展示了该方法的潜力。

Oct, 2014

本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。

Jul, 2022