Frontiers Forum on AI + Formal Methods 2025

October 11-12, 2025, Hong Kong

Since 2022, we have witnessed and are still witnessing rapid and promising development in the AI (esp. generative AI) world, and more recently (e.g. since DeepSeek R1), growing attentions are being drawn to formal methods in the AI community, e.g. as to how formal methods can be used to improve the mathematical/logical reasoning capability of AI models. On the other hand, formal methods are also expected to play a vital role in improving or ensuring the safety and reliability of AI models (and/or agentic AI systems). Last but not least, the formal methods community may also benefit from the rapid development in the AI community, as more powerful AI models will likely make formal verification/reasoning tasks cheaper and more accessible in practical use. This forum endeavours to bring both AI and Formal Methods communities together and to explore how AI and formal methods can be integrated to bring significant mutual benefit to both worlds.

Keynote Speaker

josephsifakis

Joseph Sifakis

Verimag laboratory, Grenoble

Industry Speaker

zhouhong

Hong Zhou

Invited Speaker from Industry

Invited Speakers

randy

Randy Goebel

University of Alberta

sam

Sam Staton

University of Oxford

xiangyu

Xiangyu Zhang

Purdue University

hongxia

Hongxia Yang

Hong Kong Polytechnic University

gagandeepsingh

Gagandeep Singh

University of Illinois Urbana-Champaign

xiaoming

Xiao-Ming Wu

The Hong Kong Polytechnic University

wenda

Wenda Li

University of Edinburgh

junxian

Junxian He

The Hong Kong University of Science and Technology

weiyang

Weiyang Liu

The Chinese University of Hong Kong

zhengying

Zhengying Liu

Moonshot AI

Program

Opening

Shing-Chi Cheung from The Hong Kong University of Science and Technology

Session 1

Chaired by Jun Sun from Singapore Management University

Keynote: Bringing AI to Autonomous Systems

Abstract

Joseph Sifakis from Verimag Laboratory and RITAS/SUSTECH

Industry Invited Talk: Integrating Statistical Intelligence and Logical Intelligence to better meet the future challenges

Abstract

Hong Zhou from Industry

Coffee Break

Talk 1: Why a blend of neurosymbolic methods are necessary for improving the formalization of AI foundation models?

Abstract

Randy Goebel from University of Alberta

Talk 2: AI Auditors for Code and Coding Agent

Abstract

Xiangyu Zhang from Purdue University

Lunch

Session 2

Chaired by Lei Ma from University of Tokyo and University of Alberta

Talk 3: Expressive probabilistic programming, and world models for safe AI

Abstract

Sam Staton from University of Oxford

Talk 4: Formal Methods for the LLM Era

Abstract

Gagandeep Singh from University of Illinois Urbana-Champaign

Coffee Break

Session 3

Chaired by Jialun Cao from The Hong Kong University of Science and Technology

Talk 5: Will mathematical theorem proving be solved by scaling laws?

Abstract

Wenda Li from University of Edinburgh

Talk 6: Kimina-Prover: A Large Formal Reasoning Model Based on Reinforcement Learning

Abstract

Zhengying Liu from Moonshot AI

Panel Discussion

Hosted by Shing-Chi Cheung from The Hong Kong University of Science and Technology

Panel Discussion

Joseph Sifakis from Verimag Laboratory and RITAS/SUSTECH

Hong Zhou from Industry

Randy Goebel from University of Alberta

Sam Staton from University of Oxford

Xiangyu Zhang from Purdue University

Gagandeep Singh from University of Illinois Urbana-Champaign

Session 4

Chaired by Jialun Cao from The Hong Kong University of Science and Technology

Talk 7: Co-GenAI: A Novel Fusion-Driven Platform

Abstract

Hongxia Yang from Hong Kong Polytechnic University

Talk 8: Reading Out Transformer Activations for Precise Localization in Language Model Steering

Abstract

Xiao-Ming Wu from the Hong Kong Polytechnic University

Coffee Break

Talk 9: Learning to Model Code Execution for General Reasoning of Language Models

Abstract

Junxian He from The Hong Kong University of Science and Technology

Talk 10: Towards Formal Reasoning with Large Language Models

Abstract

Weiyang Liu from The Chinese University of Hong Kong

Panel Discussion

Hosted by Lei Ma from University of Tokyo and University of Alberta

Panel Discussion

Hongxia Yang from Hong Kong Polytechnic University

Xiao-Ming Wu from the Hong Kong Polytechnic University

Junxian He from The Hong Kong University of Science and Technology

Weiyang Liu from The Chinese University of Hong Kong

Wenda Li from University of Edinburgh

Zhengying Liu from Moonshot AI

Closing

Venue

10 W, 2f CONFERENCE HALL 4 - 7, Hong Kong Science Park, Hong Kong

The Science Park offers an incredibly varied array of different spaces – from the 10,000-square-foot Grand Hall exhibition space with a mega cargo lift, to over 30 intimate break-out rooms, meeting rooms and outdoor event spaces, all within minutes of international hotels. The park truly has something to offer every MICE event — everything from small group gatherings and personal meetings to large-scale conferences and mega events can be catered to at this incredible venue. Strategically located in the middle of Hong Kong, it benefits from the equidistant transport links from Hong Kong Island and the Mainland China border. It’s the perfect choice for MICE events looking to attract Mainland Chinese vendors and attendees.

Building Floor 1 Floor 2

Registration

Registration Closed.

Join Online via [🔗Bilibili], [🔗Chaspark], or [🔗Zoom]

Organizing Committee

General Chair

Speaker 3

Shing-Chi Cheung

The Hong Kong University of Science and Technology

Co-Chair

Speaker 3

Jun Sun

Singapore Management University

Co-Chair

Speaker 3

Lei Ma

University of Tokyo and University of Alberta

Local Chair

Speaker 3

Jialun Cao

The Hong Kong University of Science and Technology

Conference Agent