ICMS 2020

Session J: Artificial Intelligence and Mathematical Software

Organisers

Dr Matthew England (Coventry University, UK) and Dr Changbo Chen (Chinese Academy of Sciences, China).

Aim and Scope

The session will cover the intersection between Mathematical Software for exact or error-controllable computation, and Artificial Intelligence (AI). All talks in the session must be on the intersection, but they may focus on either direction: i.e. either (1) using Mathematical Software to improve Artificial Intelligence; or (2) using Artificial Intelligence to improve Mathematical Software.

Topic (1) has been discussed in the literature for a long time but there is now a renewed focus as part of the drive for "explained AI". Meanwhile, topic (2) follows recent parallel develops in the different ICMS communities: computer algebra systems, theorem provers, and SAT/SMT solvers for example have all been recently shown to give an improved performance when heuristic decisions are taken by ML rather than the user/developer. This sessions aims to bring together developers of different mathematical software with a common interest on the intersection with artificial intelligence.

Accepted Talks

  • Chris Brown (US Naval Academy)
    Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving
    Click for Abstract.
  • Changbo Chen, Zhangpeng Zhu and Haoyu Chi (Chinese Academy of Sciences, Chongqing)
    Variable Ordering Selection for Cylindrical Algebraic Decomposition with Artificial Neural Networks
    Click for Abstract.
  • Michael R. Douglas (Stony Brook University)
    Formal Methods and Scientific Computation
    Click for Abstract.
  • Dorian Florescu and Matthew England (Coventry University)
    A machine learning based software pipeline to pick the variable ordering for algorithms with polynomial inputs
    Click for Abstract.
  • Stephen Forrest (Maplesoft)
    Deep Learning in Maple
    Click for Abstract.
  • Yaoshun Fu and Wensheng Yu (Beijing University of Post and Telecommunications)
    A formal Proof in Coq of the Fundamental Theorems of Continuous Functions on Closed Intervals
    Click for Abstract.
  • Na Lei (Dalian University of Technology)
    AE-OT: A New Generative Model based on Extended Semi-discrete Optimal Transport
    Click for Abstract.
  • Miroslav Olsak (University of Innsbruck)
    GeoLogic: Graphical Interactive Theorem Prover for Euclidean Geometry
    Click for Abstract.
  • Vijay Ganesh (University of Waterloo)
    SAT Solvers and Machine Learning: The Next Frontier
    Click for Abstract.
  • Tianyu Sun and Wensheng Yu (Beijing University of Post and Telecommunications)
    Formalization of the Axiom of Choice and its Equivalent Theorems in Coq
    Click for Abstract.
  • Naijun Zhan (Chinese Academy of Sciences, Beijing)
    Practical Verification of Intelligent Cyber-Physical Systems
    Click for Abstract.