The NLP-group of the Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam is looking for an Assistant Professor to work on large reasoning models, AI alignment and AI for science and research.

The TCS-group of the Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam is looking for an Assistant Professor to work on machine learning for formal reasoning and verification.

The AI Grand Est ENACT cluster, led by the University of Lorraine and the University of Strasbourg together with CNRS, Inria, Inserm, awards half- and fully-funded PhD contracts in AI-related topics, open to all disciplinary fields including the humanities and social sciences. A full fellowship covers three years of PhD salary plus €10,000 in research expenses; a half-fellowship, which should be combined with another funding source, covers half the salary plus €5,000.

The Archives Henri Poincaré is a joint research unit between the CNRS, the Université de Lorraine, and the Université de Strasbourg, with sites in Nancy and Strasbourg, working on the history and philosophy of science in a broad sense. It is one of the ENACT cluster's priority research units, and the programme can accordingly fund PhD projects in logic and philosophy that engage with AI, whether in their topic or in their methodology. We are particularly interested in projects on AI and mathematics approached from the standpoint of logic and the philosophy of mathematics, though proposals connecting AI to other areas of logic and philosophy are equally welcome. Prospective PhD students interested in developing a project along these lines should get in touch with Yacin Hamami, sufficiently early to leave time to develop a suitable research project before the topic-submission deadline.

The Department of Computer Science at TU Braunschweig is establishing a research group on Formal Methods for Trustworthy Systems and AI, offering several PhD positions. Topics of interest include formal verification, symbolic methods, and automated reasoning, with applications in AI and explainability.

Interested candidates are requested to send their application directly to Clemens Dubslaff, head of the group.

The objective of the thesis will be to investigate verification and synthesis methods for dynamic Multi-Agent Systems, based on formalisms such as the Alternating-time Temporal Logic. Directions explored will include designing efficient model-checking algorithms, determining their complexity bounds, and developing synthesis methods for computing repairs.

The student will conduct their thesis at the Paris North Computer Science Laboratory (LIPN). The expected starting date is March 2026 (negotiable). Applications should be sent directly to Munyque Mittelmann. Please don't hesitate to contact us for more information.

The goal of this project is to use formal methods to develop a systematic way to describe concurrent cryptographic protocols and to reason about their security. 

You will carry out research towards developing formal reasoning principles for concurrent cryptographic protocols and participate in the dissemination of results (conferences, research visits, etc.). In addition, you will perform light supervision duties for bachelor and/or master students and support our courses as teaching assistants (maximum two periods a year).

The thesis work will be conducted within theoretical philosophy. Theoretical philosophy includes epistemology, metaphysics, philosophy of mind, logic, philosophy of language, philosophy of science, as well as the history of philosophy.

It is likely that Valentin Goranko will be the supervisor or co-supervisor if a student with a logic project gets the position. Students can get in touch with him directly if they are interested.

The Centre for Logic, Epistemology and the History of Science (CLE) at UNICAMP invites applications for a postdoctoral position supervised by Prof. Walter Carnielli. The position is linked to the FAPESP Thematic Project "Rationality, Logic and Probability – RatioLog". This project develops a unified framework combining logic, probability, and causal inference to support robust models of rational reasoning. It aims to integrate paraconsistent and paracomplete logics with Bayesian inference and Pearl's causal models, addressing reasoning under contradiction, uncertainty, and intervention. To apply, please send an email to prof. Walter Carnielli (open this call for further instructions).

CLE-UNICAMP is one of the first and highest-ranked academic institutions in Latin America fully dedicated to the areas of Logic, Epistemology, Philosophy, and the History of Science, promoting interdisciplinary research through seminars and scientific meetings, publications, and academic exchange with research groups and institutions in Brazil and around the world.

There is a vacancy for a PhD position in information science at the Department of Information Science and Media Studies. The position is for a fixed-term period of 4 years, of which 25% will be dedicated to teaching, supervision and administrative tasks at the Department.

The PhD project is situated within the research area of logics for multi-agent systems, and their applications to formal verification, synthesis, normative reasoning, mechanism design, analysis of social phenomena, and so on. The logics in question include, but are not limited to, logics for reasoning about agents' strategies, actions, knowledge, beliefs, abilities, etc. The project will be conducted within the Logic and Artificial Intelligence (LAI) research group. The exact scope and focus of the project can be adapted to the candidate's interests.

A research group at the Toulouse University is searching for a candidate motivated to work on the combination of Non-Classical Logical Reasoning and Large Language Models. The PhD thesis will be carried out as part of the project entitled "Designing Artificial Reasoners for Communication" (DesiRes), which started in January 2026 and will end in December 2029. The PhD is expected to start no later than December 2026, preferably in November 2026, and will be funded by a three-year contract.

Assistant Professor Machine Learning for Formal Reasoning and Verification University of Amsterdam (The Netherlands)

Deadline: 7 October 2026

The TCS-group of the Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam is looking for an Assistant Professor to work on machine learning for formal reasoning and verification.

The position of Assistant Professor (Universitair Docent, UD) will be embedded within the Institute for Logic, Language and Computation (ILLC). The ILLC promotes curiosity-driven research and serves as a meeting point for computer scientists from traditional research fields ranging from AI, computer science, and mathematics to linguistics, cognitive science, and philosophy.

We are seeking candidates working at the intersection of artificial intelligence, machine learning, and formal reasoning. Relevant areas include, but are not limited to, automated reasoning, interactive theorem proving systems, formal verification, formalized mathematics, neuro-symbolic methods, and AI-assisted mathematical or logical reasoning.

We particularly welcome candidates whose work connects modern AI and machine learning with formal proof systems, interactive theorem provers, or proof assistants such as Lean, Rocq, or Isabelle. At the same time, we also encourage applications from researchers whose work engages more broadly with logic, reasoning, and theoretical computer science.

More information: https://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/16310/Assistant-Professor-Machine-Learning-for-Formal-Reasoning-and-Verification

Written on my phone, apologies for typos.

Applications must be received before 7 October, 2026

KU Leuven’s Declarative Languages and Artificial Intelligence (DTAI) section is seeking outstanding researchers to advance the field of combinatorial optimization within Bart Bogaerts’ research group. Two fully-funded positions are available: a PhD role focused on developing human-understandable explanations for optimization decisions, and a postdoc role aimed at ensuring end-to-end correctness guarantees for combinatorial solvers. Both projects leverage breakthroughs like proof logging and machine-verifiable certificates to enhance reliability, auditability, and trust in AI-driven decisions—critical for high-stakes applications and compliance with regulations like GDPR. Candidates will contribute to innovative research, such as debugging via proofs, rigorous algorithm evaluation, and domain-specific explanation methods.

Applications for the PhD role close September 30, 2026, and for the postdoc role, October 30, 2026.