Software

Current methods of AI reasoning employ domain-specific heuristic strategies that remain inconsistent, unverifiable, and opaque. Any morally accountable agent worthy of our trust must be able to premeditate actions, estimate the risk of counterfactual alternatives, rank plans according to preferences and norms, enact chosen plans while monitoring execution, compare intended versus actual outcomes, and update preferences and methods of estimation. In order to conduct transparent planning of this kind, trustworthy AI agents must be able to reason with circumstantial modal, tense, and counterfactual conditional operators, as well as causal, epistemic, and deontic operators for reasoning under uncertainty about imperatives, preferences, and moral responsibility in coordination with human and other AI agents.

In order to equip AI agents with a capacity for self-reflection and high-cognitive reasoning, I developed the model-checker package to implement a programmatic semantics for the Logos, a unified formal language of thought. Building on the current implementation, the next phases of this project are:

  1. Extend the Logos to include causal, epistemic, and deontic operators, implementing semantic theories for each with the model-checker.
  2. Build the proof-checker package in Lean to develop the metalogic and proof theory for the semantic theories implemented in the model-checker.

These projects seek to provide general-purpose tooling and methodology along with detailed documentation to make these resources accessible and to support open-source collaboration. Once these initial phases are well under way, the project will proceed to deploy these resources at scale to build AI agents capable of meta-cognition in addition to deductive, inductive, and abductive reasoning which integrates with existing domain-specific heuristic methods of reasoning determined by the context of application.

Model-Checker

In order to rapidly prototype semantic clauses for the operators included in the Logos and adequately describe their interactions, I used Microsoft's SMT solver Z3 to build the model-checker for developing and implementing semantic theories. The operators currently implemented include:

  • neg — negation
  • wedge — conjunction
  • vee — disjunction
  • rightarrow — the material conditional
  • leftrightarrow — the material biconditional
  • boxright — the must counterfactual conditional
  • diamondright — the might counterfactual conditional
  • Box — necessity
  • Diamond — possibility
  • leq — ground, read “sufficient for”
  • sqsubseteq — essence, read “necessary for”
  • equiv — propositional identity, read “just is for”
  • preceq — relevance

In addition to the operators above, the model-checker provides a TheoryLib consisting of a library of different semantic theories that users can evaluate and modify, as well as contributing their own. You can find more information in the GitHub repository , and installation instructions are provided there. If you have any trouble installing or using the model-checker, or find any surprising or unnatural results, feel free to open an issue .

Programmatic Semantics

Although computational resources are commonplace, the ability to make use of these resources to develop and explore the implications of novel semantic theories remains limited. For instance, Prover9 and Mace are restricted to first-order and equational statements. However, for the purposes of developing new semantic theories and studying their corresponding logics, it is desirable to: (1) introduce a range of primitive operators; (2) specify novel semantic clauses for each operator; (3) define the space of models for the resulting language; (4) set up unit tests for easily evaluating which sentences are a logical consequence of which upon making changes to the semantics; and (5) print readable countermodels if there are any. After developing and testing a semantics for a language, the corresponding model theory and proof theory can be developed with a much better sense of the range of theorems before establishing soundness and attempting to complete the logic.

Whereas the current version of the model-checker provides a programmatic semantics for a range of hyperintensional operators, the next release abstracts on the semantic theory included in the current version so that users may declare primitive operators, providing their semantics. Instead of computing whether a given sentence is a logical consequence of some set of sentences by hand, these resources allow users to search for countermodels or establish logical consequence up to a finite level of complexity specified by the user. If finite countermodels exist, users are able to generate and print those models rather than attempting to do so by hand, which is not only time consuming but prone to error.

Although computational systems cannot search the space of all models (typically a proper class), proving that there are no finite models up to a user-specified level of complexity provides evidence that the logical consequence in question holds in full generality. The broader the range of models considered, the stronger this evidence. Given sufficient evidence, logical consequences can then be established by hand. In the next phase of this project, I intend to incorporate the Lean proof assistant into the methodology in order to streamline the process of axiomatizing novel primitives, providing new tooling for pursuing projects in conceptual engineering.