MoSSAIC: AI Safety After Mechanism

B Research Tools Based on Live Theory

Research Support in the Age of AI

We present some initial design prototypes we are currently building around the live theory framework. In particular, we want to demonstrate the kinds of flexible, contextual understanding and feedback processes that facilitate substrate-flexibility, as described in Section Section 4.

These research tools are based around the following two claims:

• Claim 1: Current trends suggest we are heading towards AI models with lower latencies, lower costs, and greater adaptivity. Hence, we should build research tools to more fully exploit the selective advantages that AI will offer over the next few years.
• Claim 2: There are some things that will still require human input. In the context of AI safety, we posit that humans are much better able to identify and isolate subtle connections between phenomena, even when those phenomena lack a unified or formal description.

Our aim is to use the former to allow us to scale the latter. We are developing tools that offload some of the cognitive work to AI, whilst minimizing disruption to the human processes of insight generation. We are designing sensitive research tools that passively add rigor to human conversations, to exploit the productive tension between informal and formal outputs.

Sensitivity in Research Conversation

To demonstrate how we might carry out research with the help of sensitive AI-powered tools, we are designing the following pipeline:

1. Insight Extraction: As conversations happen, insights can be continually marked and extracted into a directed acyclic graph (DAG) format. This structure can then be explored both in the time and context dimensions. This tool is called Live Conversational Threads (LCT) and it performs this extraction from real time audio.
2. Formalism Generation: In keeping with live theory's orientation towards postformal artefacts, we are working on a tool that integrates with LCT. When prompted with a user's context, it generates formalisms from the gathered insights.
3. Discernment of Outputs: To prevent an influx of mathematically sound yet vacuous formalisms, we are developing an interface that enhances human capacity to discern the relevance of the generated mathematical artefacts.

Part 1: Live Conversational Threads (LCT)

We want to capture insights from researcher interactions, minimizing the disruption involved in noting these down and tracking how the conversation develops. LCT is a tool that allows users to capture potential insights from conversations.

Core Functions

LCT¹ captures “threads” (independent parts of a conversation) and the thematic flow of context between them using a DAG structure. Navigating the nodes of this graph allows you to follow the flow of dialogue more naturally.

Figure fig:lct_dag showcases this tool in action.

As seen below in Figure fig:lct_insights, this tool allows users to mark points in a conversation where they intuitively identify contextual progress or sense a potential insight.

Part 2: Formalism Generation

In addition to marking potential progress in a conversation, we want to be able to render any potential insights into a portable format. We plan to implement a further formalism generation tool that exploits AI capabilities to autoformalize natural language statements into mathematically valid formulas.

The consumers of these conversational insights can provide information about their specific research interests or the local context of the substrate in which they are working (see Figure fig:context_input).

The AI-enabled infrastructure operates seamlessly in the background considering the potential insight and local context to produce personalized substrate-sensitive formalisms (Figure fig:thread_list).

Initial formalisms are modelled using causal loop diagrams (see Figure fig:causal_loop). This structure is simple enough to allow for quick modifications and yet rich enough to capture a lot of the underlying dynamics we care about.

This can further be made rigorous by using the toggle button. We can interoperate this causal loop diagram into a provably valid mathematical formula (as shown in Figure fig:deepseek_proof) that can be represented in languages such as Lean to verify correctness.

Part 3: Live Discernment

This system can generate perfectly valid mathematical constructions. However, it takes skill to interpret such formalisms and ensure their relevance.² To avoid an explosion of trivial AI-generated formalisms, we are designing tools to augment human powers of discerning relevance, as we are convinced that these advanced mathematical AIs can generate correct/valid formalisms.

When Discernment is Relevance-Sensitive

A formalism (model) that is relevant to one “domain” does not mean that the relevance will automatically transfer to another. One has to distill the insight of the formalisms to an invariant that can be ported to another domain, and after porting, the relevance of the insight can be actuated in the language of the target domain. Our interface allows users to engage with formalisms across various domains and at multiple levels of granularity.

For instance, one can adopt many “lenses” with an economic paper. On the “surface level,” one can look through the economic-theory lens, or one can zoom in to look at the statistical methods and conclusions, or even further to explore the mathematical model in more detail. Each lens maintains connections to the queries the user is using to investigate the paper.

We are also developing collaborative aspects of the interface.

There will be as many “applications” of insightful formalisms as there are “unique relevance perspectives”. This happens when we have the tools to “identify” in a sensitive way when a particular insight/composition of insights with a “peer-defined” relevance prompt. Such a tool would take an insight (this could be the insight prompt of a particular formalism of it) and a relevance, and apply discernment (this could be human curated or suggestions from an AI) on how the insight fits the “problem” in a sensitive way. Users can then navigate the discernment space by either zooming in on particular details of the formalisms or the problem at hand and adding queries. They can also zoom out and look at the entire inference pipeline of the particular formalism while viewing connections that are relevant to the problem at hand.

A more advanced version of live-discernment would look something like this: Once a user makes contact with the Live-discernment system, they can add the formalisms of interest (the artifacts they would like to discern) to the system. Further, they can add their expressions of relevance to the said instance of the system and, from here, they can start exploring the formalisms via the expressions they have included. This will open up a “unique inference pipeline” that represents the path(s) of discernment the user took. These paths are linked to the particular formalism, and if any other peer is looking at the formalisms, they have the option to explore other peers' pipelines and incorporate them into their own.

document

Improve Explain