Automatic generation of POMDP models
Hanna Kurniawati
1 Dec 2025
This project will investigate automatic model generation of one of the most general frameworks for sequential decision-making under uncertainty, namely the Partially Observable Markov Decision Processes (POMDPs). Specifically, we will investigate how...
Robot navigation through crowds
Hanna Kurniawati
1 Dec 2025
Interested in having an autonomous robot helper in conferences/events, such as Open Day, Christmas Party, etc.? This might be the project for you!
Exploring dependent types for matrix representations
Liam O'Connor, Peter Hoefner
11 Dec 2025
Background: Dexter Kozen’s famous completeness theorem for Kleene algebras relies on a fairly intricate proof that n*n matrices over a Kleene algebra are themselves a Kleene algebra. The proof relies on an...
Understanding the Limits of LLMs on Graph Problems
Ahad N. Zehmakan, Jing Jiang
11 Dec 2025
Background
Efficient validation and presentation of policies for MDPs
Patrik Haslum
1 Jan 2026
The Markov Decision Process (MDP) is the canonical model of a sequential decision-making problem under uncertainty, and is solved by probabilistic AI planning methods. The solution to an MDP is a policy:...
Optimal troubleshooting (and other tractable POMDPs)
Patrik Haslum
1 Jan 2026
“Troubleshooting” is the problem of integrated active diagnosis and repair, in which the repairer must repeatedly select between (imperfect) diagnostic tests and repairs to perform to restore functionality of a faulty system,...
Story planning: unlimiting creativity
Patrik Haslum, Hanna Suominen
1 Jan 2026
The plot (or narrative) of a story has some similarity with a plan, as it is usually defined in classical AI planning. This has led researchers to investigate planning-based approaches to automatic...
Auto-verification of an embedded system application
Yan Liu, Peter Hoefner
16 Jan 2026
Keywords: model checking, timed automata, process algebra, computation tree logic, compilation
Axiomatic Geometry in Isabelle/HOL
Peter Hoefner
22 Jan 2026
This project aims to mechanise axiomatic geometry in Isabelle/HOL, providing a machine-checked formalisation of elementary Euclidean geometry based on Tarski-style axioms. The goal is to obtain a trustworthy, reusable foundation for geometric...
Accelerated Satisfaction
Charles Gretton
11 Feb 2026
SAT and #SAT solving in modern heterogeneous HPC environments, making use of GPUs and other accelerators to improve overall scalability and performance. Co-supervised with Dr Cody Christopher.
Discovering Subproblems in SAT and #SAT using HPC
Charles Gretton
11 Feb 2026
Boolean SAT(isfiability) and the related “counting” #SAT problem can be slow to solve on a serial computer. Use distributed HPC to cut formulae up into smaller pieces, so that search can then...
Satisfaction can be Relaxing
Charles Gretton
11 Feb 2026
Revisit, review, and evaluate semi-definite programming (SDP) relaxations of the Boolean SAT problem. Co-supervised with Dr Cody Christopher.
Transformers for Ramsey Colorings
Charles Gretton
11 Feb 2026
“go big or go home”. This project will be co-supervised with Dr Cody Christopher.
PDE Discovery of Force Balance in Toroidal Magnetic Confinement
Matthew Hole
13 Feb 2026
Deep learning of mathematics in fusion energy science
Cognitive fatigue and reduced attention in a medium-fidelity driving simulator
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein, Ms Amany Al Luhaybi and Dr Yonghui Liu.
LLM-driven persuasion on climate claims with biosignals
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein and Dr Yonghui Liu.
Personality preditions from text, wearables and video
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein and Dr Yonghui Liu
Planning Meets LLMs
Sylvie Thiébaux
19 Feb 2026
Background
Breaking Cryptography
Thomas Haines
20 Feb 2026
Cryptography is widely used in many protocols but rarely implemented by someone with a clear idea of what they were doing.
Privacy First Data Science and AI
Graham Williams
20 Feb 2026
Graham Williams
Proving Cryptography
Thomas Haines
20 Feb 2026
Cryptography is widely used in many protocols but rarely implemented by someone with a clear idea of what they were doing.
Creating a spatial intelligent musical instrument in augmented reality
Charles Martin
20 Feb 2026
The idea of this project is to develop new kinds of musical instruments for augmented reality headsets.
Intelligent musical instrument projects with IMPSy
Charles Martin
20 Feb 2026
The idea of this project is to develop new kinds of intelligent musical instruments and platforms for designing them.
Projects in Automated Planning
Pascal Bercher
21 Feb 2026
This is basically a “dummy project announcement” to help you find projects!
Verifying Quantum Error Correction with Topological Connectivity Reasoning
Alex Potanin
15 Apr 2026
Prerequisites: Strong programming skills; ideally familiarity with quantum computing fundamentals; interest in programming languages and/or formal verification. Experience with proof assistants (ideally Rocq) is a plus, but not required.
Computing internship - abilityNEWS Website
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Agentaus Productivity Intern
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing Internship - Comparative Neural Architecture Research: Supervised Fine-Tuning (SFT) vs. Continued Pre-training on V...
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Dynamic Display of Measurements on a Map
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Eccoi SAICOP Sovereign AI Community of Practice
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Humanoid robots in realistic environments (5 projects)
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing Internship - License Provenance and Consent for AI Training Datasets. A Croissant 1.1 Reference Implementation
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Mapbox Tile Engine
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Precipitation Nowcasting for Australia through AI Data Assimilation
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Reviving Endangered Language via ML
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Scalable Zonal Statistics for Continental-Scale Geospatial Analytics
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - Interactive Spatial Technologies for Industrial Augmented Reality
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - abilityNEWS Newsletter
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing Internship - Multimodal Annotation Quality Toolkit - Tracking and Schema Validation for AI Training Video
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing Internship - Neuromorphic Sensors and Reinforcement Learning Datasets - Capability Research Brief
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Computing internship - XtreamINSIGHT: Developing a real-time intelligent agent to analyse streaming data
24 Apr 2026
This position is offered through the ANU Computing Internship courses (COMP4820 / COMP8830).
Research Projects on Efficient High-dimensional Vector Search
Mengxuan Zhang
17 May 2026
How do AI agents remember, retrieve, and reason over massive knowledge bases? The answer lies in vector databases, and this project puts you at the center of building them.
PhD Position in Sustainable AI: Memory and Retrieval Infrastructure for AI Agents
Mengxuan Zhang
18 May 2026
Joint PhD — ANU School of Computing & A*STAR Singapore
PhD Position in Vector Databas: Next-Generation AI Infrastructure
18 May 2026
ANU-based PhD — School of Computing
Formalising and Analysing the Cooperative Board Game “Bomb Busters” in Epistemic Logic
Peter Hoefner, Liam O'Connor
20 May 2026
This project proposes to model the cooperative board game Bomb Busters using epistemic logic to capture how players reason about hidden information and coordinate under communication constraints. The aim is to develop...
Mechanised Mathematics
Michael Norrish
20 May 2026
Mechanising mathematics is the task of turning (relatively) well-understood mathematics into verified proofs with an interactive theorem-proving system. Such verified material can then lie behind high-assurance software.
🚀 Fully Funded PhD Positions in Software Engineering (ANU × SMU Singapore)
Xiaoyu Sun
20 May 2026
We are seeking highly motivated PhD students for fully funded positions in software engineering under a joint PhD program between the ANU and SMU (Singapore). Students enrolled in this program will have...
Responsible AI Research Projects @ANU-Xiaoyu Sun
Xiaoyu Sun
20 May 2026
We are seeking highly motivated Honours/Master students to work on the following research projects to progress responsible AI research. Opportunity for a further PhD study is possible depending on student’s performance in...
Separate Compilation for a Verified Compiler
Michael Norrish
20 May 2026
The verified CakeML compiler compiles a functional language very similar to SML into machine code, and does so in a way guaranteed to be correct by formal proof. However, the compiler must...
Verifying Indentation Sensitive Parsing
Michael Norrish
20 May 2026
Programming languages such as Haskell and Python (and the YAML notation) depend on whitespace as part of indentation to determine their syntax. The specification of this syntax is quite ugly, and very...
Gradual Typing - Language Design and Implementation
Fabian Muehlboeck
26 May 2026
Gradual Typing is the idea of using both static and dynamic typing in the same program. Most notably, TypeScript is a gradually-typed version of JavaScript, allowing users to add statically-checked type annotations...