Learning, Approximating and Minimising Streaming Automata for Large-scale Optimisation

用于大规模优化的学习、逼近和最小化流自动机

• 批准号: EP/T018313/2
• 负责人: Laure Daviaud
• 金额: $ 4.06万
• 依托单位: University of East Anglia
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT018313%2F2
• 关键词: Learning; Approximating; Minimising; Streaming; Automata

The proposed research lies at the interface of the areas of verification and machine learning, interactions of which are attracting a lot of attention currently and of potential huge benefits for both sides.Verification is this domain of computer science aiming at checking and certifying computer systems. Computer systems are increasingly used at all levels of society and peoples' lives and it is paramount to verify that they behave the way they are designed to and that we expect (examples of crucial importance, among many others, are embedded software for planes auto-pilot or self-driving cars). Unfortunately, the verification of complex systems encounters limits: there is no universal fully automated way to verify every system and one needs to find a good trade-off between the constraints of time, memory space and accuracy, which are often difficult to overcome.Machine learning has been studied since the 50's and regained much attention recently with breakthroughs in speech recognition, image processing or game playing. The development of neural networks (studied since the 60's) awarded Hinton, LeCun, and Bengio the Turing award 2019 and using deep learning, the British firm DeepMind developed its successful AlphaGo and AlphaGo Zero which were impressive steps forward and reaffirmed the amazing potential of machine learning. This project proposes to apply learning techniques in verification to improve the efficiency of some algorithms which certify computer systems and to compute fast accurate models for real-life systems.Automata are one of the mathematical tools used in verification to model computer or real-life systems. Giving certifications on these systems often boils down to running some algorithms on the corresponding automata. The efficiency of such algorithms usually depends on the size of the considered automaton. Minimising automata is thus a paramount problem in verification, as a way to verify large computer or real-life systems faster.This proposal aims at studying the minimisation of some streaming models of quantitative automata using machine learning techniques. The kind of automata we are going to focus on, are streaming models, in the sense that the input is not stored but received as a stream of data and dealt with on the fly, thus being particularly suitable for the treatment of big data. They are also suited to deal with optimisation problems such as minimising the resource consumption of a system or computing the worst-case running time of a program, for example.Minimising these kind of automata is highly challenging and linked with the long-standing open problem of the determinisation of max-plus automata. This proposal gives several directions of research, such as using learning methods to tackle it.

所提出的研究位于验证和机器学习领域的接口，它们的相互作用目前吸引了很多关注，并且对双方都有潜在的巨大利益。验证是计算机科学的一个领域，旨在检查和认证计算机系统。计算机系统越来越多地应用于社会和人们生活的各个层面，验证它们的行为是否符合设计和我们的期望是至关重要的（在许多其他例子中，至关重要的例子是飞机自动驾驶或自动驾驶汽车的嵌入式软件）。不幸的是，复杂系统的验证遇到了限制：没有通用的全自动方法来验证每个系统，并且需要在时间，内存空间和准确性之间找到一个很好的权衡，这通常是难以克服的。机器学习从上世纪50年代就开始被研究，最近随着语音识别、图像处理或游戏方面的突破，机器学习重新受到人们的关注。神经网络的发展（从60年代开始研究）使Hinton， LeCun和Bengio获得了2019年的图灵奖，并且使用深度学习，英国公司DeepMind成功开发了AlphaGo和AlphaGo Zero，这是令人印象深刻的进步，重申了机器学习的惊人潜力。本计划提出将学习技术应用于验证，以提高某些验证计算机系统的算法的效率，并为实际系统计算快速准确的模型。自动机是用于验证计算机或现实系统模型的数学工具之一。对这些系统进行认证通常归结为在相应的自动机上运行一些算法。这种算法的效率通常取决于所考虑的自动机的大小。因此，最小化自动机在验证中是一个最重要的问题，作为一种更快地验证大型计算机或现实系统的方法。本提案旨在使用机器学习技术研究定量自动机的一些流模型的最小化。我们要关注的自动机类型是流模型，从某种意义上说，输入不是存储，而是作为数据流接收并动态处理，因此特别适合处理大数据。它们也适用于处理优化问题，例如最小化系统的资源消耗或计算程序的最坏情况运行时间。最小化这类自动机是极具挑战性的，并且与长期存在的确定最大+自动机的开放性问题有关。提出了几个研究方向，如利用学习方法来解决问题。