United States

The formal verification of algorithms in the realm of Markov Decision Processes poses unique challenges, as they build on diverse mathematical concepts.
We present a methodology based on interactive theorem proving that facilitates the development of verified implementations of algorithms for solving factored Markov Decision Processes.
As a case study, we formally verify an algorithm for approximate policy iteration in the theorem prover Isabelle/HOL. 
We show how the verified algorithm can be refined to an executable, verified implementation.
Our evaluation on benchmark problems shows that it is practical.
As part of the development, we build verified software to certify linear programming solutions.
We discuss the verification process and our modifications to the algorithm during formalisation.

AAAI 2025

Formally Verified Approximate Policy Iteration

mdps

pomdps

planning with markov models

technical paper

We are pleased to announce the Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI-25), which will be held in Philadelphia, Pennsylvania at the Pennsylvania Convention Center from February 25 to March 4, 2025.

The purpose of the AAAI conference series is to promote research in Artificial Intelligence (AI) and foster scientific exchange between researchers, practitioners, scientists, students, and engineers across the entirety of AI and its affiliated disciplines. AAAI-25 will feature technical paper presentations, special tracks, invited speakers, workshops, tutorials, poster sessions, senior member presentations, competitions, and exhibit programs, and a range of other activities to be announced.

### [Invited Speakers](https://aaai.org/conference/aaai/aaai-25/aaai-25-invited-speakers/)

Register [here](https://aaai.org/conference/aaai/aaai-25/registration/)

The purpose of the AAAI conference series is to promote research in Artificial Intelligence (AI) and foster scientific exchange between researchers, practitioners, scientists, students, and engineers across the entirety of AI and its affiliated disciplines. AAAI-25 will feature technical paper presentations, special tracks, invited speakers, workshops, tutorials, poster sessions, senior member presentations, competitions, and exhibit programs, and a range of other activities to be announced.



We provide improved upper and lower bounds for the Min-Sum-Radii (MSR) and Min-Sum-Diameters (MSD) clustering problems with a bounded number of clusters $k$. In particular, we propose an exact MSD algorithm with a running-time of $n^{O(k)}$. We also provide $(1+\epsilon)$ approximation algorithms for MSR with a running-time of $O(kn) +(1/\epsilon)^{O(dk)}$ in metrics spaces of doubling dimension $d$. For MSD we get a similar approximation bound (with an extra $2^{O(k/\epsilon)}$ factor in the second term).

Our algorithms extend to $\alpha$-MSR, where radii are raised to an $\alpha$ power, for $\alpha>1$, whereas for $\alpha$-MSD we prove an exponential time ETH-based lower bound for $\alpha>\log 3$. All algorithms can also be modified to handle outliers. 

Moreover, we can extend the results to variants  that observe \emph{fairness} constraints, as well as to the general framework of \emph{mergeable} clustering, which includes many other popular clustering variants. We complement these upper bounds with ETH-based lower bounds for these problems, in particular proving that $n^{O(k)}$ time is tight for MSR and $\alpha$-MSR even in doubling spaces, and that $2^{o(k)}$ bounds are impossible for MSD.

Improved Fixed-Parameter Bounds for Min-Sum-Radii and Diameters k-Clustering and Their Fair Variants

Large Language Models (LLMs) have demonstrated remarkable proficiency in generating code. However, the misuse of LLM-generated (synthetic) code has raised concerns in both educational and industrial contexts, underscoring the urgent need for synthetic code detectors. Existing methods for detecting synthetic content are primarily designed for general text and struggle with code due to the unique grammatical structure of programming languages and the presence of numerous ``low-entropy'' tokens. Building on this, our work proposes a novel zero-shot synthetic code detector based on the similarity between the original code and its LLM-rewritten variants. Our method is based on the observation that differences between LLM-rewritten and original code tend to be smaller when the original code is synthetic. We utilize self-supervised contrastive learning to train a code similarity model and evaluate our approach on two synthetic code detection benchmarks. Our results demonstrate a significant improvement over existing SOTA synthetic content detectors, with AUROC scores increasing by 20.5\% on the APPS benchmark and 29.1\% on the MBPP benchmark.

Uncovering LLM-Generated Code: A Zero-Shot Synthetic Code Detector via Code Rewriting

Deep learning models have demonstrated exceptional performance in a variety of real-world applications. These successes are often attributed to strong base models that can generalize to novel tasks with limited supporting data while keeping prior knowledge intact. However, these impressive results are based on the availability of a large amount of high-quality data, which is often lacking in specialized biomedical applications. In such fields, models are often developed with limited data that arrive incrementally with novel categories. This requires the model to adapt to new information while preserving existing knowledge. Few-Shot Class-Incremental Learning (FSCIL) methods offer a promising approach to addressing these challenges, but they also depend on strong base models that face the same aforementioned limitations. To overcome these constraints, we propose AnchorInv following the straightforward and efficient buffer-replay strategy. Instead of selecting and storing raw data, AnchorInv generates synthetic samples guided by anchor points in the feature space. This approach protects privacy and regularizes the model for adaptation. When evaluated on three public physiological time series datasets, AnchorInv exhibits efficient knowledge forgetting prevention and improved adaptation to novel classes, surpassing state-of-the-art baselines.

AnchorInv: Few-Shot Class-Incremental Learning of Physiological Signals via Feature Space-Guided Inversion

Assignment problems are a classic combinatorial optimization problem in which a group of agents must be assigned to a group of tasks such that maximum utility is achieved while satisfying assignment constraints. Given the utility of each agent completing each task, polynomial-time algorithms exist to solve a single assignment problem in its simplest form. However, in many modern-day applications such as satellite constellations, power grids, and mobile robot scheduling, assignment problems unfold over time, with the utility for a given assignment depending heavily on the state of the system. We apply multi-agent reinforcement learning to this problem, learning the value of assignments by bootstrapping from the known polynomial-time greedy solver and then learning from further experience. We then choose assignments using a distributed optimal assignment mechanism rather than by selecting them directly. We demonstrate that this algorithm is theoretically justified and avoids pitfalls experienced by other RL algorithms in this setting. Finally, we show that our algorithm significantly outperforms other methods in the literature, even while scaling to realistic scenarios with hundreds of agents and tasks.

Multi Agent Reinforcement Learning for Sequential Satellite Assignment Problems

Multi-modality pre-training paradigm that aligns protein sequences and biological descriptions has learned general protein representations and achieved promising performance in various downstream applications. However, these works were still unable to replicate the extraordinary success of language-supervised visual foundation models due to the ineffective usage of aligned protein-text paired data and the lack of an effective function-informed pre-training paradigm. To address these issues, this paper curates a large-scale protein-text paired dataset called ProtAnno with a property-driven sampling strategy, and introduces a novel function-informed protein pre-training paradigm. Specifically, the sampling strategy determines sampling probability based on the confidence and coverage of property annotations, balancing the data quality and data quantity in face of large-scale noisy data. Furthermore, motivated by significance of the protein specific functional mechanism, the proposed paradigm explicitly model protein static and dynamic functional segments by two segment-wise pre-training objectives, injecting fine-grained information in a function-informed manner. Leveraging all these innovations, we develop ProtCLIP, a multi-modality foundational model that comprehensively represents function-aware protein embeddings. On 22 different protein benchmarks within 5 types, including protein functionality classification, mutation effect prediction, cross-modality transformation, and protein-protein interaction prediction, our ProtCLIP consistently achieves the state-of-the-art performance, with remarkable improvements of 75% on average in five cross-modality transformation tasks, 59.9% in GO-CC and 39.7% in GO-BP protein function prediction. The experimental results demonstrate the extraordinary potential of ProtCLIP serving as the protein multi-modality foundation model.

ProtCLIP: Function-Informed Protein Multi-Modal Learning

Neural video compression has recently demonstrated significant potential to compete with conventional video codecs in terms of rate-quality performance. These learned video codecs are however associated with various issues related to decoding complexity (for autoencoder-based methods) and/or system delays (for implicit neural representation (INR) based models), which currently prevent them from being deployed in practical applications. In this paper, targeting a practical neural video codec, we propose a novel INR-based coding framework, PNVC, which innovatively combines autoencoder-based and overfitted solutions. Our approach benefits from several design innovations, including a new structural reparameterization-based architecture, hierarchical quality control, modulation-based entropy modeling, and scale-aware positional embedding. Supporting both low delay (LD) and random access (RA) configurations, PNVC outperforms existing INR-based codecs, achieving nearly 35\%+ BD-rate savings against HEVC HM 18.0 (LD) - almost 10\% more compared to one of the state-of-the-art INR-based codecs, HiNeRV and 5\% more over VTM 20.0 (LD), while maintaining 20+ FPS decoding speeds for 1080p content. This represents an important step forward for INR-based video coding, moving it towards practical deployment. The source code will be available for public evaluation.

PNVC: Towards Practical INR-based Video Compression

Autonomous robots are becoming more versatile and widespread in our daily lives. From autonomous vehicles to companion robots for senior care, these human-centric systems must demonstrate a high degree of reliability in order to build trust and, ultimately, deliver social value. How safe is safe enough for robots to be wholeheartedly trusted by society? Is it sufficient if an autonomous vehicle can avoid hitting a fallen cyclist 99.9% of the time? What if this rate can only be achieved by the vehicle always stopping and waiting for the human to move out of the way? I argue that, for trustworthy deployment of robots in human-populated space, we need to complement standard statistical methods with clear-cut robust safety assurances under a vetted set of operation conditions. We need runtime learning to minimize the robot’s performance loss during safety-enforcing maneuvers by reducing its inherent uncertainty induced by its human peers, for example, their intent (does a human driver want to merge, cut behind, or stay in the lane?) or response (if the robot comes closer, how will the human react?). We need to close the loop between the robot’s learning and decision-making so that it can optimize efficiency by anticipating how its ongoing interaction with the human may affect the evolving uncertainty, and ultimately, its long-term performance.

From Gambits to Assurances: Game-Theoretic Integration of Safety and Learning for Interactive Robotics

My thesis primarily focuses on hyper-spectral image generation from frequency spectrums for downstream computer vision tasks. Hyper-spectral images are images with more than three channels commonly created by special hyper-spectral cameras or from frequency spectrums of various sensing applications such as radargrams or distributed acoustic sensing (DAS) systems. The range of frequencies considered in a frequency spectrum is typically too large to map one frequency to one image channel, i.e. we generally consider a frequency spectrum of 2500 Hz. Frequencies need to be binned together in frequency bands where each band forms one image channel. Usually, frequency bands are created either by expert knowledge or trial-and-error.
I research how filters can be trained to automatically select frequencies and bin them into frequency bands. My aim is to represent a variety of signal information and decrease noise. Signal representation is optimised for object detection on time-sequenced images with a set number of image channels. The object detection task consists of localising and classifying events in the generated hyper-spectral images. Events are typically types of intrusions, structural changes, or defined actions and structures, e.g. someone climbing a fence. Events and noise often share at least some frequencies and vary between application types.

Hyper-Spectral Image Generation from Frequency Spectrums

Mechanistic interpretability is one of the most exciting and important research programs in current AI. My aim is to build some philosophical foundations for the program, along with setting out some concrete challenges and assessing progress to date. I will argue for the importance of propositional interpretability, which involves interpreting a system’s mechanisms and behavior in terms of propositional attitudes: attitudes (such as belief, desire, or subjective probability) to propositions (e.g. the proposition that it is hot outside). Propositional attitudes are the central way that we interpret and explain human beings and they are likely to be central in AI too. A central challenge is what I call thought logging: creating systems log all of the relevant propositional attitudes in an AI system over time. I will examine currently popular methods of interpretability (such as probing, sparse auto-encoders, and chain of thought methods) as well as philosophical methods of interpretation (including psychosemantics and representation theorems) to assess their strengths and weaknesses as methods of propositional interpretability.

Premium content

Downloads

Next from AAAI 2025

Improved Fixed-Parameter Bounds for Min-Sum-Radii and Diameters k-Clustering and Their Fair Variants

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES