research
∙
06/03/2023
Message-passing selection: Towards interpretable GNNs for graph classification
In this paper, we strive to develop an interpretable GNNs' inference par...
share
research
∙
06/02/2023
Evaluating Language Models for Mathematics through Interactions
The standard methodology of evaluating large language models (LLMs) base...
research
∙
05/25/2023
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
Large language models (LLMs) present an intriguing avenue of exploration...
research
∙
03/15/2023
A large-scale multimodal dataset of human speech recognition
Nowadays, non-privacy small-scale motion detection has attracted an incr...
research
∙
10/21/2022
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
The formalization of existing mathematical proofs is a notoriously diffi...
research
∙
05/25/2022
Autoformalization with Large Language Models
Autoformalization is the process of automatically translating from natur...
research
∙
05/22/2022
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
In theorem proving, the task of selecting useful premises from a large l...
research
∙
01/11/2022
MDPose: Human Skeletal Motion Reconstruction Using WiFi Micro-Doppler Signatures
Motion tracking systems based on optical sensors typically often suffer ...
research
∙
04/19/2021
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
We report on a formalization of schemes in the proof assistant Isabelle/...
research
∙
03/18/2021
Unsupervised Doppler Radar-Based Activity Recognition for e-healthcare
Passive radio frequency (RF) sensing and monitoring of human daily activ...
research
∙
01/15/2021
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
While designing inductive bias in neural architectures has been widely s...
research
∙
01/08/2021
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabell...
research
∙
06/13/2020
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs
Mathematical proofs can be mechanised using proof assistants to eliminat...
research
∙
11/27/2018
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Many problems in computer algebra and numerical analysis can be reduced ...
research
∙
04/11/2018
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
In complex analysis, the winding number measures the number of times a p...
research
∙
04/11/2018