Programs involving discontinuities introduced by control flow constructs such
as conditional branches pose challenges to mathematical optimization methods
that assume a degree of smoothness in the objective function's response
surface. Smooth interpretation (SI) is a form of abstract interpretation that
approximates the convolution of a program's output with a Gaussian kernel, thus
smoothing its output in a principled manner. Here, we combine SI with automatic
differentiation (AD) to efficiently compute gradients of smoothed programs. In
contrast to AD across a regular program execution, these gradients also capture
the effects of alternative control flow paths. The combination of SI with AD
enables the direct gradient-based parameter synthesis for branching programs,
allowing for instance the calibration of simulation models or their combination
with neural network models in machine learning pipelines. We detail the effects
of the approximations made for tractability in SI and propose a novel Monte
Carlo estimator that avoids the underlying assumptions by estimating the
smoothed programs' gradients through a combination of AD and sampling. Using
DiscoGrad, our tool for automatically translating simple C++ programs to a
smooth differentiable form, we perform an extensive evaluation. We compare the
combination of SI with AD and our Monte Carlo estimator to existing
gradient-free and stochastic methods on four non-trivial and originally
discontinuous problems ranging from classical simulation-based optimization to
neural network-driven control. While the optimization progress with the
SI-based estimator depends on the complexity of the programs' control flow, our
Monte Carlo estimator is competitive in all problems, exhibiting the fastest
convergence by a substantial margin in our highest-dimensional problem.

控制流结构中引入的不连续性对于假设目标函数响应曲面具有一定平滑性的数学优化方法构成挑战。在此论文中，我们将平滑解释（SI）与自动微分（AD）相结合，以高效计算平滑程序的梯度。SI 与 AD 的结合使得参数综合可以直接基于梯度进行分支程序，例如校准模拟模型或将其与神经网络模型结合在机器学习流程中。我们详细说明了 SI 中为确保可行性所做的近似效果，并提出了一种新的蒙特卡罗估计器，通过 AD 和抽样的组合来估计平滑程序的梯度，从而避免了潜在的假设。通过使用我们的工具 DiscoGrad 将简单的 C++ 程序自动转换为平滑可微形式，我们进行了广泛的评估。我们将 SI 与 AD 的组合以及我们的蒙特卡罗估计器与现有的无梯度和随机方法在四个非平凡的问题上进行比较，这些问题从经典的基于模拟的优化到神经网络驱动的控制。虽然 SI 估计器的优化进展取决于程序控制流的复杂性，但我们的蒙特卡罗估计器在所有问题中都具有竞争力，在最高维问题中具有明显最快的收敛速度。

自动微分跨条件分支的平滑方法

Smoothing Methods for Automatic Differentiation Across Conditional  Branches

We consider the problem of mining signal temporal logical requirements from a
dataset of regular (good) and anomalous (bad) trajectories of a dynamical
system. We assume the training set to be labeled by human experts and that we
have access only to a limited amount of data, typically noisy. We provide a
systematic approach to synthesize both the syntactical structure and the
parameters of the temporal logic formula using a two-steps procedure: first, we
leverage a novel evolutionary algorithm for learning the structure of the
formula; second, we perform the parameter synthesis operating on the
statistical emulation of the average robustness for a candidate formula w.r.t.
its parameters. We compare our results with our previous work [{BufoBSBLB14]
and with a recently proposed decision-tree [bombara_decision_2016] based
method. We present experimental results on two case studies: an anomalous
trajectory detection problem of a naval surveillance system and the
characterization of an Ineffective Respiratory effort, showing the usefulness
of our work.

本文提供了一种系统的方法来合成时序逻辑公式的语法结构和参数，其中利用了一种新颖的进化算法来学习公式的结构，然后对候选公式的平均鲁棒性执行参数综合，以应对动力系统的异常轨迹检测和无效呼吸努力的表征两个案例研究。

一种强健的基因算法用于从数据中学习时序规范

A Robust Genetic Algorithm for Learning Temporal Specifications from  Data

We propose a simple technique for verifying probabilistic models whose
transition probabilities are parametric. The key is to replace parametric
transitions by nondeterministic choices of extremal values. Analysing the
resulting parameter-free model using off-the-shelf means yields (refinable)
lower and upper bounds on probabilities of regions in the parameter space. The
technique outperforms the existing analysis of parametric Markov chains by
several orders of magnitude regarding both run-time and scalability. Its beauty
is its applicability to various probabilistic models. It in particular provides
the first sound and feasible method for performing parameter synthesis of
Markov decision processes.

我们提出了一种简单的技术，用于验证具有参数转换概率的概率模型，通过将参数转换替换为极值的不确定选择，可以分析结果，在此基础上利用现成的方法计算区域在参数空间中的概率的上下界，其优美之处在于其适用于各种概率模型，特别是提供了执行参数综合的马尔可夫决策过程的第一个完整的有效方法。