Due to COVID-19 outbreak across the world, we need to move our theory seminars online to ZOOM. We are staying on track with the schedule and Yoriyuki Yamagata will give his talk tomorrow at 2pm.
Topic: Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning.
Abstract: “Falsification” is a method to find a system input or parameter (counter-example) which causes a behavior violating a given specification (usually given by metric or signal temporal logic). Because the correctness of a complex CPS is difficult to be proven, falsification is more practical approach than full verification. A counter-example found by falsification can be used for debugging and testing. Failure of falsification does not generally mean the correctness of the system, but suggests it in some degree. “Robustness guided falsification” is an approach of falsification. “Robustness” is a numerical measure of how robustly a formula holds. If robustness becomes negative, the formula is false. Therefore, minimizing robustness can lead falsification of a formula.
In this talk, we introduce a method to recast robustness guided falsification to a “reinforcement learning problem”. Reinforcement learning is a machine learning technique in which an agent finds a law of an interacting environment and maximizes a reward. We implement our method using “deep reinforcement leaning”, in which deep neural networks are used, and present a case study to explore its effectiveness. (This work is a collaboration with Shuang Liu, Takumi Akazaki, Yihai Duan, Jianye Hao)
Senior Researcher, Software Analytics Research Group, Information Technology Reseaerch Institute, AIST
We are glad to announce that Professor Jan A Bergstra, formerly Director of Informatics, University of Amsterdam, and chair of Informatics Section of Academia Europaea will be visiting Swansea University next week.
Johannes Aldert "Jan" Bergstra (born 1951) is a Dutch computer scientist. His work has focussed on logic and the theoretical foundations of software engineering, especially on formal methods for system design.
We are looking forward to welcome Paul Schafer, who will be visiting Swansea University on 18 to 23 January.
When people who are logicians ask me about what I do, I tell them that I study computability theory.
We are glad to welcome Hideki Tsuiki in Swansea again. This Thursday we really enjoyed his talk on “Imaginary Cubes — Mathematics, Puzzle, Art and Education”.
Abstract: Imaginary cubes are three-dimensional objects with square projections in three orthogonal ways just as a cube has. How many different kinds of imaginary cubes can you imagine? In this talk we show that there are 16 kinds of minimal convex imaginary cubes which includes regular tetrahedron, cuboctahedron, and two objects that we call H and T. As we will explain, H and T have a lot of beautiful mathematical properties related to tiling, fractal, and higher-dimensional geometry, and based on these properties, the speaker has designed a puzzle, constructed three-dimensional math-art objects, and used them for educations at various levels from elemental school to graduate schools. In this talk, I will explain mathematics of imaginary cubes and show the activities I have been engaged in. I will carry a couple of copies of the puzzle and some of the math-art objects so that the audience can enjoy them while I am staying in Swansea.
Following the Summer School, we are really proud to host the 2nd Proof Society Workshop. The workshop was an opportunity to listen to a lot of interesting invited and contributed talks on proof theory and various areas of its application:
Adam Wyner: Computational Law – The Case of Autonomous Vehicles
Yong Cheng: Exploring the incompleteness phenomenon
Matthias Baaz: Towards a Proof Theory for Henkin Quantifiers
Sonia Marin: On cut-elimination for non-wellfounded proofs: the case of PDL
Gilles Dowek: Logical frameworks, reverse mathematics, and formal proofs translation
Benjamin Ralph: What is a combinatorial proof system?
William Stirton: Ordinal assignments correlated with notions of reduction
Oliver Kullmann: Practical proof theory: practical versions of Extended Resolution
Anton Setzer and Ulrich Berger on behalf of Ralph Matthes: Martin Hofmann’s case for non-strictly positive data types – reloaded
Laura Crosilla: Philosophy of mathematics and proof theory
Takako Nemoto: Recursion Theory in Constructive Mathematics
Arno Pauly: Combinatorial principles equivalent to weak induction
Antonina Kolokolova: The proof complexity of reasoning over richer domains
Joost Joosten: The reduction property revisited
Helmut Schwichtenberg: Computational content of proofs
Thanks to all the speaker and participants and we hope to see you all again soon.
This week we are glad to welcome two visitors here at Swansea, namely Hideki Tsuiki from Kyoto University and Kristijonas Čyra from the Imperial College of London.
Hideki will give a talk on “Infinite Adequacy Theorem through Coinductive Definitions” today at 14:00 as a part of our Theory seminar series and Kristijonas will speak on “Argumentation-enabled Explainable AI Applications” this Thursday at 15:00 at the CoFo.
Professor (Course of Mathematical Science, Graduate School of Human and Environmental Studies, Kyoto University). Ressearch Interests: Computation over Real numbers and Topological spaces, Domains and their topologies, Fractals and their models, Semantics of Programming Languages, Object Oriented Programming, Mathematical Logic, Lambda Calculus.
Postdoctoral Researcher in AI at the Department of Computing, Imperial College London. I manage researchers, enthusiastically supervise and teach students, present my work at top tier international conferences, review and assess the works of others and give highest quality feedback, organise research events, represent and speak on behalf of my colleagues and fellow AI researchers during institutional and public engagement opportunities.
Wordpress is loading infos from loria
Please wait for API server guteurls.de
to collect data from
Ulrich Berger is currently attending the 3rd Workshop on Mathematical Logic and its Applications, Nancy, France, where he will present a talk on Extracting the Fan Functional.
Dongseong Seon (선동성) from KAIST, Korea is visiting Swansea. This Thursday he will give a talk on computing Haar averages as a part of our Theory seminar series. For more infromation on this topic, please click here.
As a part of our Theory Seminars, today we welcomed Ryota Akiyoshi from Waseda University, who gave a talk on Takeuti’s finitism.
Abstract: In this talk, we address several mathematical and philosophical issues of Gaisi Takeuti’s proof theory, who is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He furthered the realization of Hilbert’s program by formulating Gentzen’s sequent calculus for higher-oder logics, conjecturing that the cut-elimination holds for it (Takeuti’s conjecture), and obtaining several stunning results in the 1950-60’s towards the solution of his conjecture.
This talk consists of two parts. (1) To summarize Takeuti’s background and the argument of the well-ordering proof of ordinals up to ε0 , (2) To evaluate it on philosophical grounds. Also, we will explain several mathematical and philosophical issues to be solved. This is joint work with Andrew Arana.
My research fields are philosophy of mathematics and logic, mathematical logic (proof theory), and theoretical computer science (type theory). The main philosophical question in my research is "what is a proof ?".
Ulrich, Monika and Olga attended Hausdorff Trimester Program Types, Sets and Constructions in Bonn, Germany. During this research trip they have participated in the Constructive Mathematics workshop and had a chance to collaborate with partners from the past and existing projects, including COMPUTAL, CONRCON and CID.