AIAI Seminar - 1 November 2021 - Talks by Filip Smola, Yifei Xie and Ionela Mocanu Talk by Filip Smola Title: Mechanising Resources and Processes in Isabelle/HOL Abstract: In this talk I will give an overview of my work on mechanising resources and process composition in Isabelle/HOL. I will focus on an example of adding locations to resources and how we can express the related processes. This allows us to formally verify compositions of processes that depend on knowledge of the domain, in this case moving resources based on a graph representation of the locations. I will also give a brief overview of what we have mechanised so far, and conclude with our current work: adding distribution information to non-deterministic resources. Talk by Yifei Xie Title: Mathematical Optimization Model for Multi-committee BFT Consensus Algorithm Abstract: Byzantine fault-tolerance (BFT) algorithms are essential to various distributed systems. However, existing BFT algorithms like Practical BFT (PBFT) suffer from scalability and performance limitations, due to their high message communication complexity. To address these issues, an effective solution is to partition peer set into multiple small committees and run the consensus process in parallel. Although previous works have been successful in enhancing both the scalability and the performance of studied BFT algorithms by this way, their contribution is still not enough for rapidly scaling-up distributed applications. Moreover, partitioning a peer set is challenging due to 1) heterogeneous communications delays between different peers as the latter are generally geographically distributed, and 2) peers may have different crash and/or Byzantine failures, which leads to the failure of the BFT algorithm consensus. Consequently, it is fundamental to make optimal decisions on the number of formed parallel committees and the peers’ allocation as leader or followers. Therefore, my work focuses on applying mathematical optimization model to optimally partition peer set to guarantee high performance and scalability of multi-committee BFT in random delays and failures conditions. We conducted experiments on Microsoft Azure cloud platforms and shows 24% performance improvement compared to not applying optimization model. Such performance improvement is vital for many domain applications including new blockchain applications and traditional replica services Talk by Ionela Mocanu Title: Learning Implicitly with Noisy Data in Linear Arithmetic Abstract: Robust learning in expressive languages with real-world data continues to be a challenging task. Numerous conventional methods appeal to heuristics without any assurances of robustness. While \textit{probably approximately correct} (PAC) Semantics offers strong guarantees, learning explicit representations is not tractable, even in propositional logic. However, recent work on so-called “implicit" learning has shown tremendous promise in terms of obtaining polynomial-time results for fragments of first-order logic. In this work, we extend implicit learning in PAC-Semantics to handle noisy data in the form of intervals and threshold uncertainty in the language of linear arithmetic. We prove that our extended framework keeps the existing polynomial-time complexity guarantees. Furthermore, we provide the first empirical investigation of this hitherto purely theoretical framework. Using benchmark problems, we show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice. Nov 01 2021 14.00 - 15.00 AIAI Seminar - 1 November 2021 - Talks by Filip Smola, Yifei Xie and Ionela Mocanu AIAI Seminar talks hosted by Filip Smola, Yifei Xie and Ionela Mocanu Online
AIAI Seminar - 1 November 2021 - Talks by Filip Smola, Yifei Xie and Ionela Mocanu Talk by Filip Smola Title: Mechanising Resources and Processes in Isabelle/HOL Abstract: In this talk I will give an overview of my work on mechanising resources and process composition in Isabelle/HOL. I will focus on an example of adding locations to resources and how we can express the related processes. This allows us to formally verify compositions of processes that depend on knowledge of the domain, in this case moving resources based on a graph representation of the locations. I will also give a brief overview of what we have mechanised so far, and conclude with our current work: adding distribution information to non-deterministic resources. Talk by Yifei Xie Title: Mathematical Optimization Model for Multi-committee BFT Consensus Algorithm Abstract: Byzantine fault-tolerance (BFT) algorithms are essential to various distributed systems. However, existing BFT algorithms like Practical BFT (PBFT) suffer from scalability and performance limitations, due to their high message communication complexity. To address these issues, an effective solution is to partition peer set into multiple small committees and run the consensus process in parallel. Although previous works have been successful in enhancing both the scalability and the performance of studied BFT algorithms by this way, their contribution is still not enough for rapidly scaling-up distributed applications. Moreover, partitioning a peer set is challenging due to 1) heterogeneous communications delays between different peers as the latter are generally geographically distributed, and 2) peers may have different crash and/or Byzantine failures, which leads to the failure of the BFT algorithm consensus. Consequently, it is fundamental to make optimal decisions on the number of formed parallel committees and the peers’ allocation as leader or followers. Therefore, my work focuses on applying mathematical optimization model to optimally partition peer set to guarantee high performance and scalability of multi-committee BFT in random delays and failures conditions. We conducted experiments on Microsoft Azure cloud platforms and shows 24% performance improvement compared to not applying optimization model. Such performance improvement is vital for many domain applications including new blockchain applications and traditional replica services Talk by Ionela Mocanu Title: Learning Implicitly with Noisy Data in Linear Arithmetic Abstract: Robust learning in expressive languages with real-world data continues to be a challenging task. Numerous conventional methods appeal to heuristics without any assurances of robustness. While \textit{probably approximately correct} (PAC) Semantics offers strong guarantees, learning explicit representations is not tractable, even in propositional logic. However, recent work on so-called “implicit" learning has shown tremendous promise in terms of obtaining polynomial-time results for fragments of first-order logic. In this work, we extend implicit learning in PAC-Semantics to handle noisy data in the form of intervals and threshold uncertainty in the language of linear arithmetic. We prove that our extended framework keeps the existing polynomial-time complexity guarantees. Furthermore, we provide the first empirical investigation of this hitherto purely theoretical framework. Using benchmark problems, we show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice. Nov 01 2021 14.00 - 15.00 AIAI Seminar - 1 November 2021 - Talks by Filip Smola, Yifei Xie and Ionela Mocanu AIAI Seminar talks hosted by Filip Smola, Yifei Xie and Ionela Mocanu Online
Nov 01 2021 14.00 - 15.00 AIAI Seminar - 1 November 2021 - Talks by Filip Smola, Yifei Xie and Ionela Mocanu AIAI Seminar talks hosted by Filip Smola, Yifei Xie and Ionela Mocanu
