I work in formal, philosophical, and computational logic, focusing on applications in AI reasoning, interpretability, and formal verification.
I was previously the Stalnaker Postdoctoral Associate at MIT having previously completed my B.Phil and D.Phil in Philosophy at the University of Oxford. In my D.Phil thesis I developed a complete logic for essence and ground which regiment constitutive explanatory readings of ‘necessary for’ and ‘sufficient for’, respectively. My thesis was supervised by Tim Williamson and James Studd and examined by Kit Fine (external) and Ofra Magidor (internal).
My research develops a unified hyperintensional task semantics and axiomatic proof system for the Logos in order to provide scalable oversight for verified AI reasoning. The Logos is an extensible formal language of thought which currently includes tense, modal, counterfactual conditional, constitutive explanatory, relevance, and the standard extensional operators with many more in development. See my research for details.
To train AI systems in verified reasoning that can be interpreted and trusted, I developed the model-checker which leverages the SMT solver Z3 to provide methodology and tooling for rapidly developing modular semantic clauses. I also developed the proof-checker package which implements the proof theory, semantics, and metalogic for the Logos in LEAN. Together, these packages constitute a dual verification architecture for training AI systems in formal reasoning. See software for further details.
Contact: benbrastmckie [at] gmail [dot] com