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年代以来，学习了学习，最近随着语音识别，图像处理或游戏的突破而重新获得了很多关注。这家英国公司DeepMind授予了Hinton，Lecun和Bengio Turing Award，并使用深度学习授予Hinton，Lecun和Bengio Turing Award的发展（自60年代以来的研究）开发，英国公司DeepMind开发了其成功的Alphago和Alphago Zero，这是令人印象深刻的一步，并重申了机器的惊人潜力学习。该项目建议在验证中应用学习技术，以提高某些算法的效率，这些算法证明了计算机系统并计算现实生活中的快速准确模型。Automata是用于验证用于建模计算机或现实生活系统的数学工具之一。在这些系统上提供认证通常归结为在相应的自动机上运行一些算法。这种算法的效率通常取决于所考虑的自动机的大小。因此，最大程度地减少自动机是验证中的最高问题，是一种更快地验证大型计算机或现实生活系统的方式。该提案旨在使用机器学习技术研究一些定量自动机的流流模型的最小化。我们将要关注的自动机是流媒体模型，从某种意义上说，输入不是存储而是作为数据流而接收到的，并随时处理，因此特别适合对大数据的处理。他们还适合处理优化问题，例如最大程度地减少系统的资源消耗或计算程序中最差的运行时间。量化这类自动机是极具挑战性的，并且与长期存在的开放问题联系在一起最高自动机的确定化。该建议提供了一些研究的指示，例如使用学习方法来解决它。