Feb, 2024

SMLP: 符号机器学习求解器

HTML
PDF
TL;DR基于符号机器学习证明器 (SMLP) 的数据样本系统探索工具和库通过模拟或执行系统的一系列输入向量获得，SMLP旨在通过灰盒方法基于此数据对系统进行探索：SMLP将数据探索的统计方法与构建和探索机器学习模型相结合，通过与系统响应进行紧密交互的反馈循环，进而探索这些模型，从而结合概率和形式方法。SMLP已应用于Intel的工业环境中，用于分析和优化模拟电路的硬件设计。SMLP是一个通用工具，可应用于可由机器学习模型对系统进行采样和建模的系统。
发现论文，激发创造
  • HolStep：高阶逻辑定理证明的机器学习数据集

    本文介绍了一种基于 Higher-Order Logic 证明的新数据集，旨在开发基于机器学习的定理证明策略并提出基于该数据集的各种机器学习任务，通过一些基于逻辑回归、卷积神经网络和循环神经网络的基准模型显示出将机器学习应用于 HOL 定理证明的前景。

    Mar, 2017

  • 使用形式化数学开发无缺陷的机器学习系统

    通过可交互的证明助手，开发者能够证明机器学习系统的正确性，这种方法暴露了所有的实现错误，并通过 Certigrad 实现了优化的随机计算图，并生成了一个机器可验证的证明，证明了系统采样的梯度是数学梯度的无偏估计方法。

    Jun, 2017

  • MLSys: 机器学习系统的新前沿

    介绍ML系统在实际部署中的难点，并提出在传统系统和ML领域交叉的新兴研究方向：ML系统的硬件和软件实现以及针对预测精度之外的指标进行的ML优化，同时介绍了一个新的会议MLSys。

    Mar, 2019

  • SAMP：自适应混合精度模型推理工具包

    本文提出了一种自适应混合精度(SAMP)工具包来控制量化率，以平衡效率和性能，可以轻松量化模型进行推理。实验结果表明，SAMP工具包的加速比优于PyTorch和FasterTransformer，同时保证所需性能。此外，SAMP基于模块化设计，可无缝集成到PyTorch中处理各种下游任务。

    Sep, 2022

  • 使用PySR和SymbolicRegression.jl进行可解释的机器学习科学

    PySR是一种旨在发现可解释的符号模型的实用符号回归的开源库，其后端基于Julia库SymbolicRegression.jl，具有多种功能，包括自动微分和将表达式分发到整个集群中的数千个内核，同时我们引入了“EmpiricalBench”这种新的基准来衡量其在科学领域中的适用性。

    May, 2023

  • 利用FPGA进行符号回归用于快速机器学习推理

    本篇论文提出一种利用符号回归技术和FPGA实现的机器学习模型优化算法，成功地将一个由3层神经元组成的模型大幅优化，准确率超过90%，执行时间缩短了13倍。

    May, 2023

  • 零知识证明与机器学习相遇：一个调研

    人工智能技术进展迅速，机器学习模型的使用逐渐成为我们日常生活的一部分。这篇论文提供了一份对基于零知识证明的可验证机器学习（ZKP-VML）技术的综合调查报告，分析了不同机器学习场景中可能存在的可验证性问题，并通过详细分析和分类现有工作的技术方法，讨论了ZKP-VML领域面临的关键挑战和未来方向。

    Oct, 2023

  • SMLP：符号机器学习证明器（用户手册）

    SMLP是一个开源工具，用于探索和优化由机器学习模型表示的系统。SMLP使用符号推理进行模型的探索和优化，遵循验证和稳定性约束，并基于SMT、约束和神经网络求解器。

    May, 2024

  • miniCodeProps：证明代码属性的最小基准

    利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。

    Jun, 2024

  • 安全机器学习通过嵌入过度近似

    本研究解决了在受监管或安全关键场景中，机器学习模型行为的形式化保证问题。提出了一种创新的方法，结合了一种简单的架构、基于投影梯度法的严格训练算法，以及寻找强反例的问题表述，从而有效满足设计者选择的特性。研究结果显示，该框架能够在实际应用中良好扩展，并提供全特性满足的保证，推动了相关研究方向的发展。

    Sep, 2024