About Mahdi Bu Ali Mahdi Bu Ali M.S. (former), Computer Science Neuro-Symbolic AI Applied Ontology Ontology engineering Mahdi Bu Ali completed his MSc in Computer Science at KAUST in 2025 under the supervision of Robert Hoehndorf. His research lay at the intersection of formal mathematics, automated theorem proving, and large language models. His thesis, Automated Theorem Proving with Large Language Models in Lean: An Exploration of Specialized In-Context Learning and General-Purpose Hierarchical Architectures, addresses the long-standing goal of automating mathematical reasoning in interactive theorem provers such as Lean. Automated theorem proving is constrained both by the cost of exploring vast proof search Projects Related Projects 2024 KAUST Center of Excellence for Generative AI (Health and Wellness, BCB theme) Mon, Jan 1 2024 Research Drug mechanisms Neuro-Symbolic AI Rare disease The KAUST Center of Excellence for Generative AI has a Health and Wellness theme, and within that theme the Bioinformatics and Computational Biology (BCB) workstream is responsible for the bio-side problems that generic generative models cannot solve on their own: protein and antibody design, population-specific drug development, and clinical foundation models that can actually reason with structured biomedical knowledge. The BORG group leads the neuro-symbolic and ontology-based components of this work (Sub-WBS FCC/1/5940-07-02), in partnership with Xin Gao's group on AI/drug design and the 2023 Towards sound, complete, and explainable machine learning with biomedical ontologies (CRG11) Sun, Jan 1 2023 - Thu, Dec 31 2026 Applied Ontology Neuro-Symbolic AI Ontology engineering Semantic similarity Deep learning has driven much of the recent progress in bioinformatics, but the resulting models are essentially black boxes: it is hard or impossible to ask why a prediction was made, to verify it against existing knowledge, or to detect biases that emerge from the interaction of dataset, architecture, and training objective. In clinical and biomedical settings these limitations matter, both because clinicians need to trust the systems they use and because formal guarantees of soundness and fairness can only be obtained when the inferential machinery can be inspected. The grand challenge
KAUST Center of Excellence for Generative AI (Health and Wellness, BCB theme) Mon, Jan 1 2024 Research Drug mechanisms Neuro-Symbolic AI Rare disease The KAUST Center of Excellence for Generative AI has a Health and Wellness theme, and within that theme the Bioinformatics and Computational Biology (BCB) workstream is responsible for the bio-side problems that generic generative models cannot solve on their own: protein and antibody design, population-specific drug development, and clinical foundation models that can actually reason with structured biomedical knowledge. The BORG group leads the neuro-symbolic and ontology-based components of this work (Sub-WBS FCC/1/5940-07-02), in partnership with Xin Gao's group on AI/drug design and the
Towards sound, complete, and explainable machine learning with biomedical ontologies (CRG11) Sun, Jan 1 2023 - Thu, Dec 31 2026 Applied Ontology Neuro-Symbolic AI Ontology engineering Semantic similarity Deep learning has driven much of the recent progress in bioinformatics, but the resulting models are essentially black boxes: it is hard or impossible to ask why a prediction was made, to verify it against existing knowledge, or to detect biases that emerge from the interaction of dataset, architecture, and training objective. In clinical and biomedical settings these limitations matter, both because clinicians need to trust the systems they use and because formal guarantees of soundness and fairness can only be obtained when the inferential machinery can be inspected. The grand challenge
