Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

In A. Martin, K. Hinkelmann, H.-G. Fill, A. Gerber, D. Lenat, R. Stolle, F.
van Harmelen (Eds.), Proceedings of the AAAI 2023 Spring Symposium on
Challenges Requiring the Combination of Machine Learning and Knowledge
Engineering (AAAI-MAKE 2023), Hyatt Regency, San Francisco Airport,
California, USA, March 27-29, 2023.

[orcid=0000-0002-4889-3499, email=, url=, ] [1]

[orcid=0000-0001-8044-1110<EMAIL_ADDRESS>url=https://search.asu.edu/profile/4179815, ] [1] [1]

[orcid=, email=, url=, ]

[orcid=, email=, url=, ]

[orcid=<EMAIL_ADDRESS>url=https://labs.engineering.asu.edu/labv2/, ]
[1]

[1]Corresponding author. [1]These authors contributed equally.

# PyReason: Software for Open World Temporal Logic

Dyuman Aditya  Arizona State University, 699 S Mill Ave, Tempe, AZ, 85281, USA
Kaustuv Mukherji  Srikar Balasubramanian  Abhiraj Chaudhary  Paulo Shakarian

(2023)

###### Abstract

The growing popularity of neuro symbolic reasoning has led to the adoption of
various forms of differentiable (i.e., fuzzy) first order logic. We introduce
PyReason, a software framework based on generalized annotated logic that both
captures the current cohort of differentiable logics and temporal extensions
to support inference over finite periods of time with capabilities for open
world reasoning. Further, PyReason is implemented to directly support
reasoning over graphical structures (e.g., knowledge graphs, social networks,
biological networks, etc.), produces fully explainable traces of inference,
and includes various practical features such as type checking and a memory-
efficient implementation. This paper reviews various extensions of generalized
annotated logic integrated into our implementation, our modern, efficient
Python-based implementation that conducts exact yet scalable deductive
inference, and a suite of experiments. PyReason is available at:
github.com/lab-v2/pyreason.

###### keywords:

Logic programming Neuro Symbolic Reasoning Generalized annotated logic
Temporal logic First order logic Open world reasoning Graphical reasoning AI
Tools

##  1 Introduction

Various neuro symbolic frameworks utilize an underlying logic to support
capabilities such as fuzzy logic [1], parameterization [2], and differentiable
structures [3]. Typically, implementations of such frameworks create custom
software for deduction for the particular logic used, which limits modularity
and extensibility. Further, emerging neuro symbolic use cases including
temporal logic over finite time periods [4] and knowledge graph reasoning [5]
necessitate the need for a logical frmaework that encompasses a broad set of
capabilities. Fortunately, generalized annotated logic [6] with various
extensions [7, 8, 9] capture many of these capabilities. In this paper we
present a new software package called PyReason for performing deduction using
generalized annotated logic that captures many of the desired capabilities
seen in various neuro symbolic frameworks including fuzzy, open world,
temporal, and graph-based reasoning. Specifically, PyReason includes a core
capability to reason about first order (FOL) and propositional logic
statements that can be annotated with either elements of a lattice structure
or functions over that lattice. Further, we have provided for additional
practical syntactic and semantic extensions that allow for reasoning over
knowledge graphs, temporal logic, reasoning about various network diffusion
models, and predicate-constant type checking constraints. This implementation
provides for a fast, memory optimized, implementation of the fixpoint operator
used in the deductive process. By implementing the fixpoint operator directly
(as opposed to a black box heuristic) the software enables full explainability
of the result. As such is the case, this framework captures not only classical
logic, but a wide variety of other logic frameworks including fuzzy logic [10,
11, 12], weighted real valued logic used in logical neural networks [2], van
Emden’s logic [13], Fitting’s bilattice logic [14], various logic frameworks
for reasoning over graphs or social networks [9, 8, 15] (as well as the
various network diffusion models captured by those frameworks), and perhaps
most importantly, logic frameworks where syntactic structure can be learned
using differentiable inductive logic programming [3, 16] as well as other
neuro symbolic frameworks [17, 7]. The key advantages of our approach include
the following:

  1. 1.

Direct support for reasoning over knowledge graphs. Knowledge graph structures
are one of the most commonly-used representations of symbolic data. While
black box frameworks such as [18] also permit for reasoning over graphical
structures, they do not afford the explainability of our approach.

  2. 2.

Support for annotations. Classical logic implementations such as Prolog [19]
and Epilog [20] inherently do not support annotations or annotation functions,
hence lack direct support for capabilities such as fuzzy operators. Further,
our framework goes beyond support for fuzzy operators by enabling arbitrary
functions that can be used over real values or intervals of reals. This is a
key advantage to reasoning about constructs learned with neuro symbolic
approaches such as [2, 3, 16, 17, 7].

  3. 3.

Temporal Extensions. While the framework of [6] was shown to capture various
temporal logics, extensions such as [9] have provided for syntactic and
semantic add-ons that explicitly represent time and allow for temporal
reasoning over finite temporal sequences. Following [9], we use a semantic
structure that represents multiple time points, but we have implemented this
in a compact manner to preserve memory. Our solution allows for fuzzy versions
of rules such as “if $q(A)$ then $r(A)$ in $t$ time steps.” Note that these
capabilities are not present in nearly every current implementation of fuzzy
logic.

  4. 4.

Use of interpretations. We define interpretations as annotated function over
predicates and time together. It allows us to capture facts which are true
before $t=0$. While annotated logic [6] can subsume various temporal logics
without additional constructs, we have enabled temporal reasoning through
incorporating a temporal component in interpretations. By combining annotated
predicates and the time variable, we believe our framework is more flexible
and suitable for emerging neuro symbolic applications involving time - as such
applications will inherently require both time and real-valued annotations.
Additionally, it is to be noted that we do not make a closed world assumption
i.e. anything that is not mentioned in the initial set of interpretations is
$false$. Instead, we consider all other interpretations to be unknown at the
beginning of time.

  5. 5.

Graphical Knowledge Structures. We also implement [8] which provides graphical
syntactic extensions to [6]. This is included in our implementation, notably
adding extended syntactic operators for reasoning in such structures (e.g., an
existential operator requiring the existence of $k$ items). An example of such
a rule would be a fuzzy version of “if $q(A)$ and there exist $k$ number of
$B$’s such that $b(A,B)$ then $r(A)$”.111Note that while this example is
classical, PyReason supports fully annotated logic, allowing for arbitarily
defined fuzzy operators (e.g., t-norms); See section 2 and online supplement
for technical details.

  6. 6.

Reduction to computational complexity due to grounding. Our software leverages
both the inherent sparsity of the graphical structure along with a novel
implementation of predicate-constant type checking constraints that
significantly improves utility in a variety of application domains but also
provide drastic reduction to complexity induced by the grounding problem. We
are not aware of any other framework for first-order logic that provides both
such capabilities.

  7. 7.

Ability to detect and resolve inconsistencies in reasoning. As logical
inferences are deduced through applications of the fixpoint operator over
predefined logical rules, logical inconsistencies can not only be detected but
also located exactly where in the inference process the inconsistency
occurred. We resolve any such inconsistencies by leveraging uncertainty. In
the software implementation, as soon as an inconsistency is detected we relax
and fix the bounds to complete uncertainty. The ability to check and locate
inconsistencies enhance the explainability feature. Neuro symbolic approaches
like [2, 7] may also look to leverage inconsistency as part of loss during the
training phase.

In section 2, we outline the syntax and semantics of [6] as well as our
extensions. Our software implementation is described in section 3 and is
expanded upon in the online only supplement. In section 4, we provide
experimental results of our framework to demonstrate reasoning capabilities in
two different real-world domains. We have conducted experiments on a supply-
chain [21] ($10K$ constants), and a social media [22] ($1.6M$ constants)
dataset. For evaluation, we used various manually-curated logic programs
specifying rules for the temporal evolution of the graph, completion of the
graph, and other such practical use-cases (e.g., identifying potential supply
chain disruptions) and examined how various aspects affect runtime and memory
usage (e.g., number of constants, predicates, timesteps, inference steps,
etc.). The results show that both runtime and memory remain almost constant
over large ranges, and then scale sub-linearly with increase in network size.

#### Online Resources

Open source python library is available at: pypi.org/project/pyreason.
PyReason codebase can be found at: github.com/lab-v2/pyreason.
Online only supplement is available at:
github.com/lab-v2/pyreason/tree/main/lit

##  2 Logical Framework

In this section, we provide an overview of the annotated logic framework with
a high-level description of the logical constructs, knowledge graph structure,
key optimizations, and operation of the fixpoint algorithm.

Figure 1: Example of a knowledge graph

Knowledge graph. We assume the existence of a graphical structure
$G=(\mathcal{C},E)$ where the nodes are also constants (denoted set
$\mathcal{C}$) in a first-order logic framework. The edges, denoted
$E\subseteq\mathcal{C}\times\mathcal{C}$, specify whether any type of
relationship can exist between two constants. Similar to recent frameworks
combining knowledge graphs and logic [3, 18], we shall assume that all
predicates in the language are either unary (which can be thought of as
labeling nodes) or binary (which can be thought of as labeling edges). We note
that we assume the existence of a special binary predicate $\mathit{rel}$,
which we shall treat as a reserved word. For $(a,b)\in E$ we shall treat
$\mathit{rel}(a,b)$ as a tautology and for $(a,b)\notin E$ we shall treat
$\mathit{rel}(a,b)$ as uncertain. Note that we can support no restrictions
among the pairing of constants by creating $G$ as a fully connected graph.
Likewise, we easily support the propositional case by using a graph of a
single node (essentially treating unary predicates as ground atoms). We
provide a running example in this section. In Figure 1, we illustrate how a
knowledge graph is specified in our framework.

######  Example 2.1 (Knowledge Graph)

Consider the following nodes: three students- Phil, John, Mary and two
classes- English and Math. Nodes and edges have unary and binary predicates as
shown in Fig. 1. Hence we get the following non-ground atoms:

student(S), gpa(S), promoted(S)

class(C), difficulty(C)

friend(S,S’)

takes(S,C), grade(S,C), expertise(S,C)

Here, S, S’, and C are variables which when grounded with constants from the
graph, produce ground atoms such as:

student(john), student(phil), student(mary)

class(math), class(english)

takes(john,math), takes(mary, english)

…

In the propositional case, a non-ground atom reduces to a propositional
statement. For e.g. The predicate “takes(john,math)” can be represented as a
propositional statement: “John takes Math class” and can be either True or
False. It is true in this example, as shown in Fig. 1.

Real-valued Interval Annotations. A key advantage of annotated logic [6] is
the ability to annotate the atoms in the framework with elements of a lattice
structure as well as functions over that lattice. In our software, we use a
lower lattice structure consisting of intervals that are a subset of $[0,1]$.
This directly aligns with the truth interval for fuzzy operators [12], as well
as paradigms in neuro symbolic reasoning [2, 7], and social network analysis
[8, 9]. We can fully support scalar-valued annotations by simply limiting
manipulations to the lower bound of the interval and keeping the upper bound
set at $1$. These annotations can support classical logic by limiting
annotations to be $[0,0]$ (false) and $[1,1]$ (true). It can also support tri-
valued logic by permitting $[0,1]$, which represents no knowledge. Of course,
there is no need to conduct restrictions, especially if it is desirable to
support logics that make full use of the interval [2, 8, 9]. Additionally, we
support literals as detailed in [7]. We treat negations the same way as in [1]
\- for an atom annotated with $[\ell,u]$, we annotate its strong
negation($\neg$) with $[1-u,1-\ell]$.

######  Example 2.2 (Real-valued Interval Annotations)

Continuing with the previous example, we can support a variety of annotations
as described above.
Propositional logic:

student(john): [1,1] (example of a True statement)

takes(mary,math): [0,0] (example of a False statement)

Fuzzy logic (using scalar values):

gpa(john): [X,1], X $\in$ [0,1]

Full interval usage:

difficulty(english): [0.3,0.7] (both bounds are used here to capture the
variation among students regarding the perceived difficulty of the subject
“english”).

Modeling uncertainty and/or tri-valued logic:
Let’s assume that we do not have complete knowledge of this network -
specifically, we do not have any information about the friendship between John
and Phil. So, they might be friends (annotated [1,1]) or not friends
(annotated [0,0]). Our framework can model such a case as:

friend(john,phil): [0,1]

Interpretations. Commonly in logic frameworks, an initial set of facts is
used. We use the term “initial interpretations” to capture annotations correct
at the beginning of a program. In the envisioned domains - to include the ones
in which we perform experiments - these initial interpretations shall be
represented as a knowledge graph that not only includes graph $G$ but also
attributes on the nodes and edges (resembling predicates) and real-valued
interval annotations (specifying the initial annotations for each element).
Additionally, following intuitions from various temporal logic frameworks that
incorporate both temporal and other real-valued annotations [9, 8, 23, 24,
25], we extend our syntax to provide for temporal annotations as part of the
interpretations. Following the related work, time is represented as finite
discrete time-points. The initial interpretations comprises what is to be
treated as true before time $0$. Further, with the initial interpretations we
can specify predicates as being either static (in other words, ground atoms
formed with those predicates retain the same annotation across all time
periods) or non-static (which are permitted to change). The ability to add
this restriction has clear benefit in certain domains, and also allows for key
implementation efficiencies for reasoning across time periods. Further, it is
noted various inductive logic programming paradigms [3, 26] utilize
“extensional” predicates that are also unchanging - which could be treated as
“static” in PyReason.

Syntax:

$I(A,\hat{t}):[L,U]$
where, $A$ can be an atom (propositional case) or predicate (first order
logic), $\hat{t}$ is either the time point $T=t$ for which the interpretation
$I$ is valid, or if the interpretation is static, i.e. remains unchanged for
all time-points then $\hat{t}=s$. So,

$\hat{t}=\begin{cases}s,&\text{if}\ I(A,\hat{t})\ \text{is static}\\\ t,&t\in
T\ \text{if}\ I(A,\hat{t})\ \text{is time-variant}\end{cases}$ (1)

Annotation $[L,U]\rightarrow[0,1]$ (or, in propositional case
$[L,U]\in{[0,0],[1,1]}$). We incorporate literals in our system by having
separate interpretations for an atom and its negation. We note that, excepting
the case of static atoms, ground atoms at different time points need not be
dependent upon each other. For example, atom “a” at time $1$ can be annotated
with $[0.5,0.7]$ and annotated with $[0.1,0.2]$ at time 2. There is no
monotonicity requirement between time points.

######  Example 2.3 (Interpretations)

Continuing the previous example,
Initial set of facts regarding student enrollment:

I(student(john),0) = [1,1] (John is enrolled as a student)

I(student(mary),0) = [1,1] (Mary is enrolled as a student)

I(student(phil),0) = [0,0] (Phil is not enrolled as a student)

Static interpretations can be used for always true facts like:

I(class(english), s) = [1,1] (English is a class offered at all time-points)

Using temporal annotation to capture variation over time:

I(takes(john,math),1) = [1,1] (John takes Math class at time $t=1$)

I(takes(john,math),5) = [0,0] (But is no longer taking Math at $t=5$)

All other interpretations, if unspecified at $t=0$, are initialized with
$[0,1]$.

Logical Rules. Rules are the key syntactic construct that enables changes to
atoms formed with non-static predicates. Historically logical rules had mostly
been written by domain experts, until early work like Apriori [27] and FOIL
[28] to learn association rules from data followed by the emergence of rule
mining techniques like causal rule mining [29] and annotated probabilistic
temporal logic [24, 30, 31]. More recently, there has been research on
Differentiable Inductive Logic Programming ($\partial$ILP) - an inductive rule
learning method to learn logical rules from examples [3, 16, 32]. In the below
list $UnaSet$ and $BinSet$ are arbitrarily sets of unary and binary predicates
relevant to the rules while $pred$ is always a non-static predicate. Note that
the total number of atoms in the body is assumed to be $n$ (across all
different conjunctions). The symbol $\exists_{k}$ means there exists at least
$k$ number of constants such that the ensuing logical sentence is satisfied.

  1. 1.

Ground rule for reasoning within a single constant or edge:
$pred(c):f(x_{1},\ldots,x_{n})\leftarrow_{\Delta t}\bigwedge_{pred_{i}\in
UnaSet}pred_{i}(c):x_{i}$

$pred(c,c^{\prime}):f(x_{1},\ldots,x_{n})\leftarrow_{\Delta
t}\bigwedge_{pred_{i}\in BinSet}pred_{i}(c,c^{\prime}):x_{i}$

  2. 2.

Universally quantified non-ground rule for reasoning within a single constant
or edge:
$\forall X:pred(X):f(x_{1},\ldots,x_{n})\leftarrow_{\Delta
t}\bigwedge_{pred_{i}\in UnaSet}pred_{i}(X):x_{i}$

$\forall X,X^{\prime}\ s.t.\ (X,X^{\prime})\in
E:pred(X,X^{\prime}):f(x_{1},\ldots,x_{n})\leftarrow_{\Delta
t}\bigwedge_{pred_{q}\in
BinSet}pred_{q}(X,X^{\prime}):x_{q}\wedge\bigwedge_{pred_{r}\in
UnaSet}pred_{r}(X):x_{r}\wedge\bigwedge_{pred_{s}\in
UnaSet^{\prime}}pred_{s}(X^{\prime}):x_{s}$

  3. 3.

Universally quantified non-ground rule for reasoning across an edge:
$\forall X:pred(X):f(x_{1},\ldots,x_{n})\leftarrow_{\Delta
t}\exists_{k}X^{\prime}:rel(X,X^{\prime}):[1,1]\wedge\bigwedge_{pred_{q}\in
BinSet}pred_{q}(X,X^{\prime}):x_{q}\wedge\bigwedge_{pred_{r}\in
UnaSet}pred_{r}(X):x_{r}\wedge\bigwedge_{pred_{s}\in
UnaSet^{\prime}}pred_{s}(X^{\prime}):x_{s}$

  4. 4.

Non-ground rule with rule based quantifier in the head:
$pred(X):[A_{s}(l_{1},l_{2},\ldots,l_{n}),A_{s}(u_{1},u_{2},\ldots,u_{n})]\leftarrow\bigwedge_{X_{i}\
\text{s.t.}\ (X,X_{i})\in E}pred^{\prime}(X,X_{i}):[l_{i},u_{i}]$

Here, $A_{s,m}^{k}(S)$ could be the $m^{th}$ rule based quantifier defined
over set $S$ such that, $A_{s,m}^{k}(S)=k^{th}\ \text{highest value in set}\
S$.

######  Example 2.4 (Logical Rules)

For the continuing example we can formulate some interesting rules based on
the formats given above as:

  1. 1.

$promoted(X):[T(l_{1},l_{2}),U(u_{1},u_{2})]\leftarrow_{\Delta
t=1}student(X):[l_{1},u_{1}]\wedge gpa(X):[l_{2},u_{2}]$

which says, “If $X$ is a student with bounds $[l_{1},u_{1}]$ and has a gpa
with bounds $[l_{2},u_{2}]$, then $X$ is likely to be promoted, at the next
timestep, with bounds given by a function of $[l_{1},u_{1}]$ and
$[l_{2},u_{2}]$.”

Here, $T$ could be a T-norm. Some well known examples of T-norms are:

    1. (a)

Minimum: $T(a,b)=T_{min}(a,b)=min(a,b)$

    2. (b)

Product: $T(a,b)=T_{prod}(a,b)=a\cdot b$

    3. (c)

Łukasiewicz: $T(a,b)=T_{luk}(a,b)=max(0,a+b-1)$

PyReason also supports other well known logical functions like $T-conorm$,
algebraic functions like $max$, $min$, $average$, among others.

  2. 2.

$\forall X,Y\ expertise(X,Y):[0.6*L,1]\leftarrow_{\Delta
t=0}grade[X,Y]:[L,1]\wedge student(X):[1,1]\wedge class(Y):[1,1]$

which says, “If $X$ is a student who obtains a grade $[L,1]$ in class $Y$,
then we can estimate $X$’s expertise of subject $Y$ by defining an annotation
function $[0.6*L,1]$ over a single annotation $[L,1]$.”

  3. 3.

$gpa(john):[\frac{x_{1}+x_{2}}{2},1]\leftarrow_{\Delta
t=0}\exists_{i=2}C_{i}\in\mathcal{C}:class(C_{i}):[1,1]\wedge
takes(john,C_{i}):[1,1]\wedge grade(john,C_{i}):[x_{i},1]$

which says, “If $john$ takes and earns grades for two classes, then his $gpa$
can be calculated using the algebraic function $avg$ in the head of the given
existentially quantified ground rule.”

  4. 4.

$friend(S,S^{\prime}):[1,1]\leftarrow_{\Delta t=2}takes(S,C):[1,1]\wedge
takes(S^{\prime},C):[1,1]\wedge class(C):[1,1]$

a propositional rule with temporal extension which states, “If two students
$S$ and $S^{\prime}$ take the same class $C$, they develop a friendship after
two timesteps.”

  5. 5.

$\forall S,S^{\prime},S^{\prime\prime}\
friend(S,S^{\prime\prime}):[1,1]\leftarrow_{\Delta
t=1}friend(S,S^{\prime}):[1,1]\wedge
friend(S^{\prime},S^{\prime\prime}):[1,1]$

an universally quantified non-ground rule analogous to the associative rule in
mathematics which encapsulates, “Having a common friend $S^{\prime}$ leads to
friendship between two people $S$ and $S^{\prime\prime}$.”

Fixpoint Operator for Deduction. Central to the deductive process is a
fixpoint operator (denoted by $\Gamma$) which has previously been proven to
produce all atoms entailed by a logic program (rules and facts) in [6, 7] and
these results were extended for the temporal semantics in [9, 8]. It is
noteworthy that this is an exact computation of the fixpoint, and hence
providing the minimal model associated with the logic program allowing one to
easily check for entailment of arbitrary formulae. Further, the result is
fully explainable as well: for any entailment query we would have the series
of inference steps that lead to the result. This differs significantly from
other frameworks that do not provide an explanation for deductive results [18]
though a key difference is that the reasoning framework implemented in
PyReason allows for exact and efficient polynomial time inference, while
others have an intractable inference process.

######  Example 2.5 (Fixpoint Operator($\Gamma$))

Consider we have the following set of initial interpretations in addition to
the ones specified before:

I(takes(john,english),1) = I(takes(john,english),2) = [1,1]

I(takes(mary,english),2) = I(takes(mary,english),3) = [1,1]

(John takes English at t=1,2 and Mary takes English at t=2,3)

I(friend(mary,phil),s) = [1,1]

(Mary and Phil are friends for the entire time considered)

And we consider the rule set $\bm{R}$ to be made of rule 4 and 5 from above.
We initialize:

$\forall$S,S’ I(friend(S,S’),0) = [0,1] (all $friend$ relationships
initialized as unknown)

and then update:

I(friend(mary,phil),s) = [1,1] (from initial interpretations)

Application of $\Gamma$ at T=0 and 1 yields no change in $\bm{I}$ as none of
the rules are fired.

At T=2, rule 4 fires with the following groundings:

$friend(john,mary):[1,1]\leftarrow_{\Delta t=2}takes(john,english):[1,1]\wedge
takes(mary,english):[1,1]\wedge class(english):[1,1]$

$friend(mary,john):[1,1]\leftarrow_{\Delta t=2}takes(mary,english):[1,1]\wedge
takes(john,english):[1,1]\wedge class(english):[1,1]$

This would result in a change in $\bm{I}$ at T = 4, as $\Delta t=2$ for the
rule above and it is fired at T=2.

I(friend(john,mary),4) = [1,1]

I(friend(mary,john),4) = [1,1]

At T=3, as $\bm{I}$ is still unchanged, application of $\Gamma$ does not lead
to any of the rules firing.

At T=4, application of $\Gamma$ with the updated interpretation leads to
firing of grounded rule 5 as:

$friend(john,phil):[1,1]\leftarrow_{\Delta t=1}friend(john,mary):[1,1]\wedge
friend(mary,phil):[1,1]$

And results in:

I(friend(john, phil),5) = [1,1]

The above illustrates how PyReason makes logical inferences by exact
application of the fixpoint operator($\Gamma$). In this example, we are able
to trace how the interpretation I(friend(john, phil),t) changed over time, and
which rules caused these changes. This shows that this process is completely
explainable, and can be leveraged in emerging neuro symbolic applications.

Constant-Predicate Type Checking Constraints. Key to reducing the complexity
and speeding up of the inference process is type-checking. We leverage the
sparsity commonly prevalent in knowledge graphs to significantly cut down on
the search space during the grounding process. We noticed that typically a
graph will have nodes of different types, and predicates typically were
defined only over constants of a specific type. While initializing the
interpretations, type checking takes this into account and only creates ground
atoms for the subset of predicate-constant pairs which are compatible with
each other. However, we note that this is an option, as in some applications
such information may not be available.

######  Example 2.6 (Constant-Predicate Type Checking)

In the continuing example we see that the predicates student, gpa, promoted
are only limited to constants of type student. Similarly, predicates class,
difficulty are exclusive to the constants english and math. Type checking
ensures that we do not consider ground atoms like student(english) or
class(phil).

Likewise for binary predicate takes(S,C), the first variable is always
grounded with a student type constant, and the second with a class type
constant. Even in this miniature example, type checking reduces the number of
ground atoms under consideration from 25 to only 6 - a 76% reduction. Such
gains significantly reduce complexity as size and sparsity of the graph
increases.

Detecting and Resolving Inconsistencies. Inconsistency can occur in the
following cases:

  1. 1.

For some ground atom, a new interpretation is assigned an annotation
$[L^{\prime},U^{\prime}]$ that is not a subset of the current interpretation
$[L,U]$ (we assume $L\leq U$). i.e. if either $U<L^{\prime}$ or
$U^{\prime}<L$.

  2. 2.

When an inconsistency occurs between an atom and its negation like “a” and
“not a”. Or between complementary predicates like “$bachelor(X)$” and
“$married(X)$” which cannot hold simultaneously.
e.g. Literal A has annotation $[L_{1},U_{1}]$ and Literal B is the negation of
literal A with annotation $[L_{2},U_{2}]$. The fixpoint operator attempts to
assign $[L_{1}^{\prime},U_{1}^{\prime}]$ to Literal A, and
$[L_{2}^{\prime},U_{2}^{\prime}]$ to Literal B. But new bounds are
inconsistent, i.e. either $L_{1}^{\prime}>1-L_{2}^{\prime}$ or
$U_{1}^{\prime}<1-U_{2}^{\prime}$.

PyReason flags all such inconsistencies arising during the execution of the
fixpoint operator and reports them. Further, as the fixpoint operator provides
an explainable trace, the user can see the precise cause of the inconsistency.
As an additional, practical feature, PyReason includes an option to reset the
annotation to $[0,1]$ for any identified inconsistency and set the atom to
static for the remainder of the inference process. In this way, such
inconsistencies cannot propagate further. These initial capabilities provide a
solid foundation for more sophisticated consistency management techniques such
as providing for local consistency or iterative relaxation of the initial
logic program.

######  Example 2.7 (Detecting and Resolving Inconsistencies.)

Consider we have the following prior knowledge:

I(takes(phil,math), 4) = [1,1]

I(takes(mary,math), 4) = [1,1]

I(friend(phil,mary), 5) = [0,0]

However, the following logical rule with grounding $S\leftarrow phil$,
$S^{\prime}\leftarrow mary$, $C\leftarrow math$:

$friend(S,S^{\prime}):[1,1]\leftarrow_{1}takes(S,C):[1,1]\wedge
takes(S^{\prime},C):[1,1]$ gets fired at $t=4$.

resulting in:

I(friend(phil,mary), 5) = [1,1]

But clearly this is an inconsistency as I(friend(phil,mary), 5) cannot be both
$[0,0]$ and $[1,1]$ simultaneously. So, we conclude that at least one of those
two interpretations must be incorrect. If there is no way to ascertain which
is correct, we may resolve this logical inconsistency by setting:

I(friend(phil,mary), s) = [0,1] at $t=5$.

##  3 Implementation

We have endeavored to create a modern Python-based framework to support
scalable yet correct reasoning. We allow graphical input via convenient
Graphml format, which is commonly used in knowledge graph architectures. The
python library Networkx is used to load and interact with the graph data. We
are currently in the process of directly supporting Neo4j. The initial
conditions and rules are entered in YAML format and we use memory-efficient
implementation techniques to correctly capture semantic structures. We use the
Numba open-source JIT compiler to translate many key operations into fast,
optimized machine code while allowing the user to interact with Python and the
aforementioned front-ends. Our implementation can support CPU parallelism, as
evidenced by our experiments run on multi-CPU machines.

Our software stores interpretations in a nested dictionary. For computational
efficiency and ease of use, our software allows specification of a range of
time-points $T={t_{1},t_{2},\ldots}$ instead of a single time-point $t$, for
which an interpretation $I$ remains valid. To reduce memory requirements, only
the one set of interpretations (current) are stored at any point in time.
However, past interpretations can be obtained using rule traces, which retains
the change history for each interpretation and the corresponding grounded
logical rules that caused each change. Rule traces make our software
completely explainable, as every inference can be traced back to the cascade
of rules that led to it.

MANCaLog [9] showed the use of the fixpoint operator for both canonical and
non-canonical models. By recomputing interpretations at every time step, we
not only require significantly less memory but also, support both the
canonical and the non-canonical cases. Due to this design, increase in
computation time is observed to be minimal.

Furthermore, we make significant advances on [33] by supporting static
predicates, and having in-built capabilities for non-graph reasoning, and type
checking as detailed in section 2.

Our implementation can be found online as specified in section 1 and detailed
pseudo-code can be found in the supplemental information.

##  4 Experiments

###  4.1 Honda Buyer-Supplier Dataset

We conduct our experiment on a Honda Buyer-Supplier network [21]. The dataset
(network) contains 10,893 companies (nodes) and 47,247 buyer-supplier
relationships between them (edges).

We design an use case, where we assume that operations of all companies from a
particular country are disrupted, and observe the effects that this may have
on companies across the world. We feel this is akin to supply chain issues
faced worldwide during the COVID-19 pandemic. For our tests, we use the
following logical rule which in practice would be either learned or come from
an expert.
$disrupted(Buyer):[1,1]\leftarrow_{\Delta
t=1}\forall_{k}supplies(Sup_{k},Buyer):[1,1],\exists_{k/2}disrupted(Sup_{k}):[1,1]$
It states that, a company is disrupted at a particular timestep if at least
50% of its suppliers are totally disrupted in the previous timestep. We
conduct this experiment for three different countries (USA, Taiwan, and
Australia), having a wide range of proportion of companies in the dataset. We
do not fix the number of inference steps, instead we let the diffusion process
run until it converges (in bold). The results are shown in Table 1.

Table 1: Honda network: How disruption on a country’s industry, caused by a pandemic, may spread worldwide Companies | Companies disrupted across the world at time t= | % of companies disrupted
---|---|---
Based | Count | 0 | 1 | 2 | 3 | 4 | … | 38 | Initial | Final | Change
USA | 1599 | 1599 | 1965 | 2057 | 2203 | 2313 | … | 3336 | 14.68 | 30.75 | 16.07
Taiwan | 603 | 603 | 644 | 647 | 647 | 647 | … | 647 | 5.54 | 5.94 | 0.40
Australia | 128 | 128 | 131 | 131 | 131 | 131 | … | 131 | 1.18 | 1.21 | 0.03

To test if our approach could scale, we use two inference rules which jointly
state, a company is disrupted at a particular timestep if any of its
supplier(s) are completely disrupted in the previous timestep, or if at least
50% of its suppliers are disrupted to at least 50% of their capacity. We
conduct this experiment for different graph sizes, and for different number of
timesteps to show the scaling capability of our software in Table 2.

Table 2: Scalability of our framework Nodes (N) | Edges (E) | Total attributes | Density | Timesteps | Runtime (in s) | Memory (in MB)
---|---|---|---|---|---|---
1000 | 410 | 5012 | 4.10 x $10^{-4}$ | 2 | 0.36 | 4.9
|  |  |  | 5 | 0.42 | 1.8
|  |  |  | 15 | 0.34 | 0.1
2000 | 1640 | 13269 | 4.10 x $10^{-4}$ | 2 | 0.43 | 1.2
|  |  |  | 5 | 0.55 | 2.1
|  |  |  | 15 | 0.81 | 8.2
5000 | 10244 | 57852 | 4.10 x $10^{-4}$ | 2 | 1.54 | 17.2
|  |  |  | 5 | 1.84 | 16.0
|  |  |  | 15 | 3.38 | 54.6
10000 | 41034 | 197752 | 4.10 x $10^{-4}$ | 2 | 4.83 | 80.3
|  |  |  | 5 | 6.29 | 60.3
|  |  |  | 15 | 12.34 | 210.8

The results show that both runtime and memory remain almost constant over
large ranges, and then scale sub-linearly with increase in network size.

###  4.2 Pokec Social Media dataset

Pokec is a popular slovakian social network, and this dataset [22] contains
personal information like gender, age, pets (attributes) of 1.6 million people
(nodes), and 30.6 million connections between them (edges).

We take inspiration from the advertising community to design our use case. We
consider, a small proportion of the population, who has pet(s), to be
customers of a pet food company. The company, using Pokec data, must identify
relevant advertising targets among the population. A realistic strategy can be
captured by two logical rules:

  1. 1.

$\forall X,Yrelevance(X):[0.6,1]\leftarrow_{\Delta
t=1}relevance(Y):[1,1]\wedge friend(X,Y):[1,1]$

Friend of a relevant target or existing customer (always relevant), is at
least 60% relevant.

  2. 2.

$\forall X,Yrelevance(X):[1,1]\leftarrow_{\Delta t=1}relevance(Y):[1,1]\wedge
friend(X,Y):[1,1]\wedge hasPet(X,P):[1,1]\wedge hasPet(Y,P):[1,1]$

Friend of a relevant target is totally relevant if they have pet(s) of same
kind - dog, cat, …

The diffusion process converged after 8 timesteps, took 42 minutes to complete
and used 58.36 GB of memory - which further showcases the scalability of our
framework. The results are shown in Table 3.

Table 3: Pokec social media: How brands may use consumer data to identify prospective customers |  |  | Advertising targets
---|---|---|---
Population size | Current Customers | Timesteps | Fully relevant | Partially relevant
1,632,803 | 2,308 | 0 | 2,308 | 0
|  | 1 | 2,596 | 39,836
|  | 2 | 2,657 | 47,405
|  | 3 | 2,679 | 49,174
|  | 4 | 2,690 | 50,046
|  | 5 | 2,692 | 50,412
|  | 6 | 2,693 | 50,455
|  | 7, 8, … | 2,693 | 50,608

The process of inference is completely explainable, and an user may use rule
traces, an optional output of PyReason, to identify the logical rules that led
to change in each interpretation. An example of a rule trace from the previous
experiment is presented in Table 4.

Table 4: Rule trace for a single node for label relevance. Application of rule 1 above caused the first change from $[0,1]$ to $[0.6,1]$, followed by, an update to $[1,1]$ due to firing of rule 2. A list of node and edge IDs which were used to ground the rule clauses are also provided. t |  Old Bound |  New Bound |  Rule fired | Clause-1 | Clause-2 | Clause-3 | Clause-4
---|---|---|---|---|---|---|---
1 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 | [‘354455’] | [(‘354365’, ‘354455’)] |  |
2 |  [0.6,1.0] |  [1.0,1.0] |  rule_2 | [‘354455’, | [(‘354365’, ‘354455’), | [(‘718503’, | [(‘354365’,
|  |  |  | ‘718503’] | (‘354365’, ‘718503’)] | ‘cat’)] | ‘cat’)]

All experiments were performed on an AWS EC2 container with 96 vCPUs (48
cores) and 384GB memory.

##  5 Related work

In section 1, we discussed how PyReason extends on the early modern logic
programming languages like Prolog [19], Epilog [20] and Datalog [34] by
supporting annotations. Recent neuro symbolic frameworks show great promise in
the ability to learn or modify logic programs to align with historical data
and improve robustness to noise. Many such frameworks rely on an underlying
differentiable, fuzzy, first order logic. For example, logical tensor networks
[1] uses differentiable versions of fuzzy operators to combine ground and non-
ground atomic propositions while logical neural networks [2] associate
intervals of reals with atomic propositions and uses special parameterized
operators. Meanwhile, induction approaches such as differentiable ILP [3]
fuzzy logic programs (using the product t-norm) are learned from data based on
template rule structures in a manner that support recursion and multi-step
inference. In [17], Logical Neural Networks was used interpret learned rules
in a precise manner. Here also, gradient descent was used to train the
parameters of the network. In the last two years, two paradigms have emerged
with much popularity in the neuro symbolic literature. Logical Tensor Networks
(LTN) [1] extend neural architectures through fuzzy, real-valued logic.
Logical Neural Networks (LNN) [2] provide a neuro symbolic framework with
parameterized operators that supports open world reasoning in the logic. As
stated earlier, both can be viewed as a subset of annotated logic. Hence,
PyReason can be used to conduct inference on the logic for both frameworks, in
addition to providing key capabilities such as graph-based and temporal
reasoning, which currently are not present in the logics of those frameworks.

In both the forward pass of various neuro symbolic frameworks [35, 2, 1], as
well as for subsequent problems (e.g., entailment, abductive inference,
planning, etc.), a deduction process is required. PyReason is designed to
provide this precise capability. Generalized annotated programs [6] has been
shown to capture a wide variety of real-valued, temporal, and fuzzy logics as
it associates logical atoms with elements of a lattice structure as opposed to
scalar values. As a result it can capture all the aforementioned logics, while
retaining polynomial-time deduction due to the monotonicity of the lattice.
The use of a lattice structure allows for us to associate logical constructs
with intervals, thus enabling open world reasoning. In our recent work [7], we
provided extensions to [6] that allows for a lower lattice structure for
annotations. This enables the framework to capture paradigms such as LNN [2]
and the MANCALog [9] for graph-based reasoning. However, that work only showed
that analogs to the theorems of [7] for the lower lattice case and did not
provide an implementation or experimental results.

By supporting generalized annotated logic, and its various extensions PyReason
enables system design that is independent of the learning process. As a
result, once a neuro symbolic learning process creates or modifies a logic
program based on data, PyReason can be used to efficiently answer deductive
queries (to include entailment and consistency queries) as well as support
more sophisticated inference such as abductive inference or planning.

Today knowledge graphs are crucial in representing data for reasoning and
analysis. Recent research on creation of knowledge graphs [36, 37] proposes
methods to automatically convert conceptual models into knowledge graphs in
GraphML format for enterprise architecture and a wide range of applications.
PyReason, which supports the graphml format, could be an effective tool to
reason about knowledge graphs obtained from one of these platforms.

##  6 Conclusion and Future Work

In this paper, we presented PyReason: an explainable inference software
supporting annotated, open world, real-valued, graph-based, and temporal
logics. Our modern implementation extends established generalized annotated
logic framework to support scalable and efficient reasoning over large
knowledge graphs and diffusion models. We are currently working on a range of
extensions to this work. This includes adding more temporal logic operators
for specification checking, learning rules from data through induction, and
using the inference process to create new knowledge in non-static graphs
(e.g., adding nodes and edges). We will also look to explore how PyReason can
be used in conjunction with LTN [1], and LNN [2]. In supporting frameworks
such as these, we will look to add capabilities for symbol grounding [38],
leveraging the results of the training process from frameworks such as LTN.
Finally, we also plan on extending PyReason to act as a simulator for
reinforcement learning based agents.

###### Acknowledgements.

The authors are supported by internal funding from the Fulton Schools of
Engineering and portions of this work is supported by U.S. Army Small Business
Technology Transfer Program Office or the Army Research Office under Contract
No.W911NF-22-P-0066.

## References

  * Badreddine et al. [2022] S. Badreddine, A. d’Avila Garcez, L. Serafini, M. Spranger,  Logic tensor networks,  Artificial Intelligence 303 (2022) 103649.
  * Riegel et al. [2020] R. Riegel, A. Gray, F. Luus, N. Khan, N. Makondo, I. Y. Akhalwaya, H. Qian, R. Fagin, F. Barahona, U. Sharma, S. Ikbal, H. Karanam, S. Neelam, A. Likhyani, S. Srivastava, Logical neural networks, 2020\.
  * Evans and Grefenstette [2018] R. Evans, E. Grefenstette,  Learning explanatory rules from noisy data,  J. Artif. Int. Res. 61 (2018) 1–64.
  * Ma et al. [2020] M. Ma, J. Gao, L. Feng, J. Stankovic,  STLnet: Signal temporal logic enforced multivariate recurrent neural networks,  in: Advances in Neural Information Processing Systems, volume 33, Curran Associates, Inc., 2020, pp. 14604–14614.
  * Sen et al. [2022] P. Sen, B. W. Carvalho, I. Abdelaziz, P. Kapanipathi, S. Roukos, A. Gray,  Logical neural networks for knowledge base completion with embeddings & rules,  in: Conference on Empirical Methods in Natural Language Processing, 2022, pp. 3863–3875.
  * Kifer and Subrahmanian [1992] M. Kifer, V. Subrahmanian,  Theory of generalized annotated logic programming and its applications,  J. Log. Program. 12 (1992) 335–367.
  * Shakarian and Simari [2022] P. Shakarian, G. I. Simari,  Extensions to generalized annotated logic and an equivalent neural architecture,  in: 2022 TransAI, 2022, pp. 63–70.
  * Shakarian et al. [2013a] P. Shakarian, G. I. Simari, D. Callahan,  Reasoning about complex networks: A logic programming approach,  Theory Pract. Log. Program. 13 (2013a).
  * Shakarian et al. [2013b] P. Shakarian, G. I. Simari, R. Schroeder,  Mancalog: a logic for multi-attribute network cascades,  in: International conference on Autonomous Agents and Multi-Agent Systems, AAMAS, 2013b, pp. 1175–1176.
  * Höhle [1978] U. Höhle,  Probabilistic uniformization of fuzzy topologies,  Fuzzy Sets and Systems (1978).
  * Alsina et al. [1983] C. Alsina, E. Trillas, L. Valverde,  On some logical connectives for fuzzy sets theory,  Journal of Mathematical Analysis and Applications 93 (1983) 15–26.
  * Vojtáš [2001] P. Vojtáš,  Fuzzy logic programming,  Fuzzy sets and systems 124 (2001) 361–370.
  * Van Emden and Kowalski [1976] M. H. Van Emden, R. A. Kowalski,  The semantics of predicate logic as a programming language,  J. ACM 23 (1976) 733–742.
  * Fitting [1990] M. Fitting, Bilattices in logic programming, City University of New York, Lehman College, Department of Mathematics and Computer Science, 1990.
  * Shakarian et al. [2013] P. Shakarian, M. Broecheler, V. Subrahmanian, C. Molinaro,  Using generalized annotated programs to solve social network diffusion optimization problems,  ACM Transactions on Computational Logic 14 (2013).
  * Shindo et al. [2021] H. Shindo, M. Nishino, A. Yamamoto,  Differentiable inductive logic programming for structured examples,  in: AAAI Conference on Artificial Intelligence, 2021, pp. 5034–5041.
  * Sen et al. [2022] P. Sen, B. W. S. R. d. Carvalho, R. Riegel, A. Gray,  Neuro-symbolic inductive logic programming with logical neural networks,  AAAI conference on Artificial Intelligence (2022).
  * Hohenecker and Lukasiewicz [2020] P. Hohenecker, T. Lukasiewicz,  Ontology reasoning with deep neural networks,  in: Journal of Artificial Intelligence Research, volume 68, 2020, pp. 503–540.
  * Colmerauer [1982] A. Colmerauer,  Prolog and infinite trees,  Logic Programming 16 (1982) 2.
  * Schubert and Hwang [2000] L. K. Schubert, C. H. Hwang,  Episodic logic meets little red riding hood: A comprehensive, natural representation for language understanding,  Natural language processing and knowledge representation: Language for Knowledge and Knowledge for Language (2000).
  * Yan et al. [2015] T. Yan, T. Y. Choi, Y. Kim, Y. Yang,  A theory of the nexus supplier: A critical supplier from a network perspective,  Journal of Supply Chain Management 51 (2015) 52–66.
  * Takac and Zabovsky [2012] L. Takac, M. Zabovsky,  Data analysis in public social networks,  in: International scientific conference and international workshop present day trends of innovations, 2012\.
  * Dekhtyar et al. [1999] A. Dekhtyar, M. I. Dekhtyar, V. S. Subrahmanian,  Temporal probabilistic logic programs,  in: International Conference on Logic Programming, 1999, p. 109–123.
  * Khuller et al. [2007] S. Khuller, M. V. Martinez, D. S. Nau, A. Sliva, G. I. Simari, V. S. Subrahmanian,  Computing most probable worlds of action probabilistic logic programs: scalable estimation for 10${}^{\mbox{30, 000}}$ worlds,  Ann. Math. Artif. Intell. 51 (2007) 295–331.
  * Shakarian et al. [2011] P. Shakarian, A. Parker, G. Simari, V. V. S. Subrahmanian,  Annotated probabilistic temporal logic,  ACM Trans. Comput. Logic 12 (2011).
  * França et al. [2014] M. V. França, G. Zaverucha, A. S. d’Avila Garcez,  Fast relational learning using bottom clause propositionalization with artificial neural networks,  Machine learning 94 (2014).
  * Agrawal et al. [1996] R. Agrawal, H. Mannila, R. Srikant, H. Toivonen, A. I. Verkamo, et al.,  Fast discovery of association rules.,  Advances in knowledge discovery and data mining 12 (1996) 307–328.
  * Quinlan [1990] J. R. Quinlan,  Learning logical definitions from relations,  Machine learning 5 (1990).
  * Stanton et al. [2015] A. Stanton, A. Thart, A. Jain, P. Vyas, A. Chatterjee, P. Shakarian,  Mining for causal relationships: A data-driven study of the islamic state,  in: ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2015, pp. 2137–2146.
  * Shakarian et al. [2011] P. Shakarian, A. Parker, G. Simari, V. V. Subrahmanian,  Annotated probabilistic temporal logic,  ACM Transactions on Computational Logic (TOCL) 12 (2011) 1–44.
  * Shakarian et al. [2012] P. Shakarian, G. I. Simari, V. Subrahmanian,  Annotated probabilistic temporal logic: Approximate fixpoint implementation,  ACM Transactions on Computational Logic (TOCL) 13 (2012) 1–33.
  * Sen et al. [2022] P. Sen, B. W. de Carvalho, R. Riegel, A. Gray,  Neuro-symbolic inductive logic programming with logical neural networks,  in: AAAI Conference on Artificial Intelligence, 2022\.
  * Paredes et al. [2021] J. N. Paredes, G. I. Simari, M. V. Martinez, M. A. Falappa,  Detecting malicious behavior in social platforms via hybrid knowledge- and data-driven systems,  Future Generation Computer Systems 125 (2021) 232–246.
  * Abiteboul et al. [1995] S. Abiteboul, R. Hull, V. Vianu, Foundations of databases, volume 8, Addison-Wesley Reading, 1995\.
  * Yang et al. [2020] Z. Yang, A. Ishay, J. Lee,  Neurasp: Embracing neural networks into answer set programming,  in: International Joint Conference on Artificial Intelligence, IJCAI, 2020.
  * Smajevic and Bork [2021] M. Smajevic, D. Bork,  From conceptual models to knowledge graphs: a generic model transformation platform,  in: 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), IEEE, 2021, pp. 610–614.
  * Glaser et al. [2022] P.-L. Glaser, S. J. Ali, E. Sallinger, D. Bork,  Model-based construction of enterprise architecture knowledge graphs,  in: Enterprise Design, Operations, and Computing: 26th International Conference, Springer, 2022, pp. 57–73.
  * Harnad [1990] S. Harnad,  The symbol grounding problem,  Physica D: Nonlinear Phenomena 42 (1990).
  * Lloyd [1987] J. W. Lloyd, Foundations of logic programming, Springer-Verlag New York, Inc., 1987\.

##  Appendix A Formal Syntax and Semantics.

We now recapitulate the definition of Generalized Annotated Logic programs
(from now on referred to as “GAPs”, for short) from [6] as well as the
extensions that we include in our software.

In [6], the authors assumed the existence of a semilattice. $\mathcal{T}$ (not
necessarily complete) with ordering $\sqsubseteq$. To support contemporary
applications in neuro symbolic reasoning [2, 3, 7, 16, 17] as well as social
network analysis [9, 8] we implemented this as a lower semilattice structure.
Therefore, we have a single element $\bot$ and multiple top elements
$\top_{0},\ldots\top_{i}\ldots\top_{max}$. The notation $height(\mathcal{T})$
is the maximum number of elements in the lattice in a path between $\bot$ and
a top element (including $\bot$ and the top element)222In general, we shall
assume that the lattice consists of finite, discrete elements.. The employment
of a lower semilattice structure allows enables two desirable characteristics.
First, we desire to annotate atoms with intervals of reals in $[0,1]$ as done
in previous work [2, 9, 25]. Second, it allows for reasoning about such
intervals whereby the amount of uncertainty (i.e., for interval $[l,u]$ the
quantity $u-\ell$) decreases monotonically as an operator proceeds up the
lattice structure. Therefore, we define bottom element $\bot=[0,1]$ and a set
of top elements $\\{[x,x]\;|\;[x,x]\subseteq[0,1]\\}$ (see note333N.B. that
when using a semilattice of bounds, the notation “$\sqsubseteq$” loses its
“subset intuition”, as $[0,1]\sqsubseteq[1,1]$ in this case, for example.).
Specifically, we set $\top_{0}=[0,0]$ and $\top_{max}=[1,1]$. An example of
such a semilattice structure is shown in Figure 2.

Figure 2: Example of a lower semilattice structure where the elements are
intervals in $[0,1]$.

As with [6], we assume the existence of a set AVar of variable symbols ranging
over $\mathcal{T}$ and a set $\mathcal{F}$ of function symbols, each of which
has an associated arity. We start by defining annotations.

######  Definition A.1 (Annotation)

(i) Any member of $\mathcal{T}\,\cup\textsf{AVar}$ is an annotation.
(ii) If $f$ is an $n$-ary function symbol over $\mathcal{T}$ and
$t_{1},\ldots,t_{n}$ are annotations, then $f(t_{1},\ldots,t_{n})$ is an
annotation.

One specific function we define is “$\neg$” which is used in semantics of [6]
as well as the more recent interval-based framework used in [2]. For a given
$[l,u]$, $\neg([l,u])=[1-u,1-l]$. Note that we also use the symbol $\neg$ in
our first-order language (following the formalism of [6]). We define a
separate logical language whose constants are members of set $\mathcal{C}$ and
whose predicate symbols are specified by set $\mathcal{P}$. We also assume the
existence of a set $\mathcal{V}$ of variable symbols ranging over the
constants, that no function symbols are present, and terms and atoms are
defined in the usual way (cf. [39]). We shall assume that
$\mathcal{C},\mathcal{P},\mathcal{V}$ are discrete and finite. In general, we
shall use capital letters for variable symbols and lowercase letters for
constants. Similar to previous work [3, 18] shall assume that all elements of
$\mathcal{P}$ have an arity of either 1 or 2 - so we shall denote these
$\mathcal{P}_{una}$ for unary predicates and $\mathcal{P}_{rel}$ for binary
predicates. We shall also denote a subsets of $\mathcal{P}$ to include “target
predicates” written $\mathcal{P}_{tgt}$ that can consist of either binary or
unary predicates ($\mathcal{P}_{tgt\\_rel},\mathcal{P}_{tgt\\_una}$) provided
that they are not reserved words. We shall use the symbol $\mathcal{L}$ to
denote the set of all ground literals and $\mathcal{A}$ for the set of all
ground atoms. We now define the syntactical structure of GAPs that will be
used in this work.

######  Definition A.2 (Annotated atoms, negations, literals)

The core syntactic structures are defined as follows:

  * •

Annotated atom. If $a$ is an atom and $\mu$ is an annotation, then $a:\mu$ is
an _annotated atom_.

  * •

Annotated Negation. If $a$ is an atom and $\mu$ is an annotation, then $\neg
a:\mu$ is an _annotated negation_.

  * •

Annotated Literal. Collectively, atoms and negations are referred to as
_annotated literals_.

######  Definition A.3 (GAP Rule)

If $\ell_{0}:\mu_{0},\ell_{1}:\mu_{1},\ldots,\ell_{m}:\mu_{m}$ are annotated
literals (such that for all $i,j\in 1,m$, $\ell_{i}\not\equiv\ell_{j}$), then

$\displaystyle r\equiv\ell_{0}:\mu_{0}$ $\displaystyle\leftarrow$
$\displaystyle\ell_{1}:\mu_{1}\,\wedge\,\ldots\wedge\,\ell_{m}:\mu_{m}$

is called a _GAP rule_. We will use the notation $head(r)$ and $body(r)$ to
denote $\ell_{0}$ and $\\{\ell_{1},\ldots,\ell_{m}\\}$ respectively. When
$m=0$ ($body(r)=\emptyset$), the above GAP-rule is called a _fact_. A GAP-rule
is _ground_ iff there are no occurrences of variables from either AVar or
$\mathcal{V}$ in it. For ground rule $r$ and ground literal $\ell$,
$bodyAnno(\ell,r)=\mu$ such that $\ell:\mu$ appears in the body of $r$. A
generalized annotated program $\Pi$ is a finite set of GAP rules.

The formal semantics of GAPs are defined as follows. Note that we extend the
notion of an interpretation to allow for a mapping of literals to annotations
(as opposed to atoms). However, we add a requirement on the annotation between
each atom and negation that ensures equivalence to the semantic structure of
[6].

######  Definition A.4 (Interpretation)

An interpretation $I$ is any mapping from the set of all grounds literals to
$\mathcal{T}$ such that for literals $a,\neg a$, we have $I(a)=\neg(I(\neg
a))$. The set $\mathcal{I}$ of all interpretations can be partially ordered
via the ordering: $I_{1}\preceq I_{2}$ iff for all ground literals $a$,
$I_{1}(\ell)\sqsubseteq I_{2}(\ell)$. $\mathcal{I}$ forms a complete lattice
under the $\preceq$ ordering.

Now we present the satisfaction relationship:

######  Definition A.5 (Satisfaction)

An interpretation $I$ _satisfies_ a ground literal $\ell:\mu$, denoted
$I\models\ell:\mu$, iff $\mu\sqsubseteq I(\ell)$. $I$ satisfies the ground
GAP-rule

$\displaystyle\ell_{0}:\mu_{0}$ $\displaystyle\leftarrow$
$\displaystyle\ell_{1}:\mu_{1}\wedge\,\ldots\,\wedge\,\ell_{m}:\mu_{m}$

(denoted
$I\models\ell_{0}:\mu_{0}\leftarrow\ell_{1}:\mu_{1}\,\,\wedge\,\ldots\,\wedge\,\ell_{m}:\mu_{m}$)
iff either

  1. 1.

$I$ satisfies $\ell_{0}:\mu_{0}$ or

  2. 2.

There exists an $1\leq i\leq m$ such that $I$ does not satisfy
$\ell_{i}:\mu_{i}$.

$I$ satisfies a non-ground literal or rule iff $I$ satisfies all ground
instances of it.

We say that an interpretation $I$ is a _model_ of program $\Pi$ if it
satisfies all rules in $\Pi$. Likewise, program $\Pi$ is _consistent_ if there
exists some $I$ that is a model of $\Pi$. We say $\Pi$ _entails_ $\ell:\mu$,
denoted $\Pi\models\ell:\mu$, iff for every interpretation $I$ s.t.
$I\models\Pi$, we have that $I\models\ell:\mu$. As shown by [6], we can
associate a fixpoint operator with any GAP $\Pi$ that maps interpretations to
interpretations.

###### Definition A.6

Suppose $\Pi$ is any GAP and $I$ an interpretation. The mapping
${\mathbf{T}}_{\Pi}$ that maps interpretations to interpretations is defined
as

${\mathbf{T}}_{\Pi}(I)(\ell_{0})=\mathbf{sup}(annoSet_{\Pi,I}(\ell_{0})),$

where
$annoSet_{\Pi,I}(\ell_{0})=\\{I(\ell_{0})\\}\cup\\{\mu_{0}\>\;|\;\>\ell_{0}:\mu_{0}\leftarrow\ell_{1}:\mu_{1}\,\wedge\ldots\wedge\,\ell_{m}:\mu_{m}\textit{
is a ground}$ $\textit{instance of a rule in }\Pi,\textit{ and for all }1\leq
i\leq m,\textit{we have }I\models\ell_{i}:\mu_{i}\\}$

The key result of [6] tells us that $\mathit{lfp}({\mathbf{T}}_{\Pi})$
precisely captures the ground atomic logical consequences of $\Pi$. We show
this is also true (under the condition that $\Pi$ is consistent) even if the
annotations are based on a lower lattice. In [6], the authors also define the
_iteration_ of ${\mathbf{T}}_{\Pi}$ as follows:

  * •

${\mathbf{T}}_{\Pi}\uparrow 0$ is the interpretation that assigns $\bot$ to
all ground literals.

  * •

${\mathbf{T}}_{\Pi}\uparrow(i+1)={\mathbf{T}}_{\Pi}({\mathbf{T}}_{\Pi}\uparrow
i)$.

For each ground $\ell\in\mathcal{L}$, the set $\Pi(\ell)$ is the subset of
ground rules (to include facts) in $\Pi$ where $\ell$ is in the head. We will
use the notation $m_{\ell}$ to denote the number of rules in $\Pi(\ell)$. For
a given ground rule, we will use the symbol $r_{\ell,i}$ to denote that it is
the $i$-th rule with atom $\ell$ in the head.

##  Appendix B Formal Proofs for Results where the Lower Lattice Assumption is
Made.

Please see [7].

##  Appendix C Additional Details on Supply Chain Experiments

Table 5 summarizes the contents of the dataset. 7,396 companies were listed
with a unique GICS, while 3,497 did not have one listed.

Table 5: Overview of the Honda Buyer-Supplier Network Companies (Nodes) | 10,893
---|---
Buey-Supplier Relationships (Edges) | 47,247
Global Industry Classification Standard (GICS) types | 67
Edge Relationship types | 4

To understand the structure of the buyer-supplier network more in-depth, one
industry along with its first and second Tier suppliers are mapped, as shown
in Figure 3. Each node shown in the figure contain an attribute _name_ which
describes the name of the industry and each edge connecting those industries
contain an attribute _cost_ which describes the profit relationship between
those two particular industries connected by an edge.

Figure 3: A snapshot of the network showing link connections with attribute
labels

In Figure 4 a portion of data is mapped out showing the complexity of the
supply network. The figure can help identify a few key nodes which connect
large sections of the network to other major sections - which makes them
critical to operations.

Figure 4: Honda Supply Chain Network. Each node and edge is differently
colored based on the type.

Figure 5 shows the distribution of various industry types. Figure 6 gives
different edge relationships present in the dataset.

Figure 5: Distribution of the nodes in the network based on its GICS type.
Figure 6: Edge relationships in the dataset.

##  Appendix D Additional Details on Social Network Experiments

Table 6 gives an overview of the dataset, and the schema is shown in Fig. 7.
The edge relationship types are enumerated in the figure.

Table 6: Overview of the Pokec Social Media dataset Nodes | 1,632,820
---|---
Edges | 31,633,113
Node attribute types | 5
Edge Relationship types | 4
Figure 7: Schema of Pokec network

Graph density represents the ratio between the edges present in a graph and
the maximum number of edges that the graph can contain. In reality, graphs are
often sparse (not dense). To test the scaling capacity of our approach with
graph density, we re-run the experiment in Table 2 while modifying the density
of the dataset. The results, in Table 7, show that the experiments on Honda
data, which is about 40 times more dense than the Pokec network takes only
about 3 times more memory, and 6 times more runtime to complete. This further
showcases the scaling capability of our framework.

Table 7: Impact of graph density on memory and runtime |  | Honda | Pokec
---|---|---|---
| Density$\rightarrow$ | 4.10 x $10^{-4}$ | 0.11 x $10^{-4}$
Nodes (N) | Timesteps | Runtime (in s) | Memory (in MB) | Runtime (in s) | Memory (in MB)
10000 | 2 | 4.83 | 80.3 | 0.70 | 27.4
| 5 | 6.29 | 60.3 | 0.93 | 19.9
| 15 | 12.34 | 210.8 | 1.73 | 21.2

Finally, to test the scalability of our approach with respect to the number of
attributes (and hence, number of ground atoms) in a graph, we run an
experiment for a simple use-case - once with the original dataset, and then
with the attributes added in. We define the use-case on the social media data
as:
$\forall X,Y~{}~{}infected(X):[1,1]\leftarrow_{\Delta
t=1}infected(Y):[1,1]\wedge friend(X,Y):[1,1]$
which says, “A person contracts the virus if any of their friend(s) is
infected by a virus”. The results are as shown in Table 8.

Table 8: Impact of adding 7 attributes on memory and runtime for 5 timesteps Attributes | Nodes (N) | Edges (E) | Grounded atoms | Runtime (in mins) | Memory (in GB)
---|---|---|---|---|---
Not added | 1,632,803 | 30,622,563 | 3,265,606 | 19.95 | 42.44
Added | 1,632,820 | 31,633,113 | 36,531,539 | 28.26 | 59.39
Change | (+17) | (+1,010,550) | (+33,265,933) | (+8.31) | (+16.95)

##  Appendix E Expanded Rule Traces

A longer version of the rule trace in Table 4, with 10 atoms is presented in
Table 9.

Table 9: A longer version of the rule trace from Table 4 for Label:relevance |  |  | Bound |  |  |  |  |
---|---|---|---|---|---|---|---|---
t |  $\Gamma$ |  Node |  Old |  New |  Rule fired |  Clause-1 |  Clause-2 |  Clause-3 |  Clause-4
1 |  1 |  1273439 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘835886’] |  [(‘1273439’, ‘835886’)] |  [(‘835886’, ‘cat’)] |  [(‘1273439’, ‘cat’)]
1 |  1 |  103308 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘659792’, ‘404372’] |  [(‘103308’, ‘659792’), (‘103308’, ‘404372’)] |  |
2 |  2 |  277684 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘305645’] |  [(‘277684’, ‘305645’)] |  [(‘305645’, ‘fish’)] |  [(‘277684’, ‘fish’)]
2 |  2 |  551249 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘377195’] |  [(‘551249’, ‘377195’)] |  |
3 |  3 |  861455 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘1450147’] |  [(‘861455’, ‘1450147’)] |  [(‘1450147’, ‘spider’)] |  [(‘861455’, ‘spider’)]
3 |  3 |  23197 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘25795’] |  [(‘23197’, ‘25795’)] |  |
3 |  3 |  757646 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘423053’] |  [(‘757646’, ‘423053’)] |  |
4 |  4 |  86436 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘743812’] |  [(‘86436’, ‘743812’)] |  [(‘743812’, ‘cat’)] |  [(‘86436’, ‘cat’)]
4 |  4 |  40242 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘407809’] |  [(‘40242’, ‘407809’)] |  |
4 |  4 |  757646 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘423053’, ‘548848’] |  [(‘757646’, ‘423053’), (‘757646’, ‘548848’)] |  [(‘548848’, ‘cat’)] |  [(‘757646’, ‘cat’)]
5 |  5 |  420093 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘275269’, ‘472129’] |  [(‘420093’, ‘275269’), (‘420093’, ‘472129’)] |  |
5 |  5 |  1334826 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘1486432’] |  [(‘1334826’, ‘1486432’)] |  [(‘1486432’, ‘fish’)] |  [(‘1334826’, ‘fish’)]
5 |  5 |  196947 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘212129’] |  [(‘196947’, ‘212129’)] |  |
6 |  6 |  348252 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘1123497’] |  [(‘348252’, ‘1123497’)] |  [(‘1123497’, ‘cat’)] |  [(‘348252’, ‘cat’)]
6 |  6 |  1144981 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘232110’] |  [(‘1144981’, ‘232110’)] |  |
6 |  6 |  420093 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘275269’, ‘472129’, ‘275337’] |  [(‘420093’, ‘275269’), (‘420093’, ‘472129’), (‘420093’, ‘275337’)] |  [(‘275337’, ‘turtle’)] |  [(‘420093’, ‘turtle’)]
7 |  7 |  354365 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘354455’, ‘718503’] |  [(‘354365’, ‘354455’), (‘354365’, ‘718503’)] |  [(‘718503’, ‘cat’)] |  [(‘354365’, ‘cat’)]
7 |  7 |  420093 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘275269’, ‘472129’, ‘275337’] |  [(‘420093’, ‘275269’), (‘420093’, ‘472129’), (‘420093’, ‘275337’)] |  [(‘275337’, ‘turtle’)] |  [(‘420093’, ‘turtle’)]
7 |  7 |  757646 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘423053’, ‘548848’] |  [(‘757646’, ‘423053’), (‘757646’, ‘548848’)] |  [(‘548848’, ‘cat’)] |  [(‘757646’, ‘cat’)]
7 |  7 |  50219 |  [0.0,1.0] |  [1.0,1.0] |  rule_2 |  [‘2067’, ‘50136’] |  [(‘50219’, ‘2067’), (‘50219’, ‘50136’)] |  [(‘2067’, ‘cat’), (‘50136’, ‘cat’)] |  [(‘50219’, ‘cat’), (‘50219’, ‘cat’)]
7 |  7 |  148995 |  [0.0,1.0] |  [0.6,1.0] |  rule_1 |  [‘140490’] |  [(‘148995’, ‘140490’)] |  |

##  Appendix F Implementation Pseudocode

Algorithm 1 enumerates the data structures in use. Algorithm 2 shows the
initial state, while algorithm 3 details the inference process. During
inference, interpretations are updated as shown in algorithm 4. Logical
consistency is maintained using algorithms 5 and 6.

Algorithm 1 Data Structures Used

1:Nested Dictionary $\bm{I}=[Node/Edge,[Predicate,[Lower,Upper,Static]]]$ to
store current interpretations only. If $Static$ is set to $1$,
bounds:$Lower,Upper$ can no longer change for rest of program.

2:List $\bm{L}=[(Node/Edge,Predicate,Lower,Upper,Static,at\\_t)]$ to store
facts and inferences, before it is used to update the dictionary.

3:List $\textbf{IPL}=[(Predicate_{1},Predicate_{2})]$ containing pairs of
predicates which cannot hold simultaneously, i.e., the bounds must be pairwise
complementary. In the propositional case, if one of the predicates is $true$,
the other must be $false$. We call this “inconsistent predicate list (IPL)”.

4:List $\bm{E}=[(Node/Edge,Predicate)]$ containing list of predicates that
becomes inconsistent in the course of program execution.

Algorithm 2 Program initialization

1:$\bm{I}$ as follows:

2:$\forall$ nodes/edges, use $type\\_checking$ to initialize valid predicates
only.

3:All bounds are initialized to [0,1]. $Static$ set to 0.

4:$\bm{L}\leftarrow[~{}]$ $\triangleright$ Empty list

5:Facts (incl. initial interpretations) are then copied into $\bm{L}$

6:$t\leftarrow 0$

7:$\bm{E}\leftarrow[~{}]$

8:Input: Number of diffusion time-steps $T$, Set of rules $\bm{R}$

Algorithm 3 Program flow

1:while $t\leq T$ do

2: for $i$ in $I$, where ($Static$ is $false$) do

3: reset bounds to [0,1]

4: end for

5: $update\\_req\leftarrow 0$

6: for $l$ in $\bm{L}$, where ($l(at\\_t)==t$) do

7: if check_consistency($l\in\bm{L}$,$l\in\bm{I}$) then

8: update_req += update_interp($l\in\bm{L}$,$l\in\bm{I}$)

9: else

10: resolve_inconsistency($l\in\bm{I}$)

11: if $(l,l^{\prime})\in\textbf{IPL}$, $\forall l^{\prime}$ then

12: resolve_inconsistency($l^{\prime}\in\bm{I}$)

13: end if

14: end if

15: end for

16: if $update\\_req$ then

17: Apply fix-point operator($gamma$) once.

18: for each resulting interpretation do

19: if $Static$ is $false$ in $I$ then

20: Add to $\bm{L}$

21: end if

22: end for

23: Go to line $5$.

24: else

25: $t\leftarrow t+1$.

26: end if

27:end while

Algorithm 4 Updating interpretations

1:procedure update_interp($i^{\prime},i$)

2: $updated\leftarrow 0$

3: if
$i(Lower)!=i^{\prime}(Lower)~{}\text{(}or)~{}i(Upper)!=i^{\prime}(Upper)$ then

4: $i(Lower)\leftarrow f_{l}(i(Lower),i^{\prime}(Lower))$

5:$\triangleright$ by default $f_{l}$ is the $max()$ function, but it can be
user defined.

6: $i(Upper)\leftarrow f_{u}(i(Upper),i^{\prime}(Upper))$

7:$\triangleright$ by default $f_{u}$ is the $min()$ function, but it can be
user defined.

8: $updated\leftarrow 1$

9: end if

10: if $updated~{}\text{(}and)~{}(i,ic)\in\textbf{IPL}$, $\forall ic$ then

11: $ic(Lower)\leftarrow f_{l}(ic(Lower),1-i(Upper))$

12: $ic(Upper)\leftarrow f_{u}(ic(Upper),1-i(Lower))$

13: end if

14: return $updated$

15:end procedure

Algorithm 5 Consistency checking

1:procedure check_consistency($i^{\prime},i$)

2:$\triangleright$ $i^{\prime}$ is new interpretation with
$[L^{\prime},U^{\prime}]$, and, $i$ is current interpretation with $[L,U]$

3: if $L^{\prime}>U~{}\text{(}or)~{}U^{\prime}<L$ then

4: return $False$

5: else

6: return $True$

7: end if

8:end procedure

Algorithm 6 Inconsistency resolution

1:procedure resolve_inconsistency($i\in\bm{I}$)

2: $i(Lower)\leftarrow 0$

3: $i(Upper)\leftarrow 1$

4: $i(Static)\leftarrow 1$

5:end procedure


11institutetext:  Johns Hopkins University, Baltimore, MD, 21218, USA
22institutetext: University of Maryland School of Medicine and R Adams Cowley
Shock Trauma Center, Baltimore, MD, 21201, USA
22email<EMAIL_ADDRESS><EMAIL_ADDRESS>
# FastSAM3D: An Efficient Segment Anything Model for 3D Volumetric Medical
Images

Yiqing Shen 11 Jingxing Li 11 Xinyuan Shao 11 Blanca Inigo Romillo 11 Ankush
Jindal 11 David Dreizin(✉) 22 Mathias Unberath(✉) 11

###### Abstract

Segment anything models (SAMs) are gaining attention for their zero-shot
generalization capability in segmenting objects of unseen classes and in
unseen domains when properly prompted. Interactivity is a key strength of
SAMs, allowing users to iteratively provide prompts that specify objects of
interest to refine outputs. However, to realize the interactive use of SAMs
for 3D medical imaging tasks, rapid inference times are necessary. High memory
requirements and long processing delays remain constraints that hinder the
adoption of SAMs for this purpose. Specifically, while 2D SAMs applied to 3D
volumes contend with repetitive computation to process all slices
independently, 3D SAMs suffer from an exponential increase in model parameters
and FLOPS. To address these challenges, we present FastSAM3D which accelerates
SAM inference to 8 milliseconds per $128\times 128\times 128$ 3D volumetric
image on an NVIDIA A100 GPU. This speedup is accomplished through 1) a novel
layer-wise progressive distillation scheme that enables knowledge transfer
from a complex 12-layer ViT-B to a lightweight 6-layer ViT-Tiny variant
encoder without training from scratch; and 2) a novel 3D sparse flash
attention to replace vanilla attention operators, substantially reducing
memory needs and improving parallelization. Experiments on three diverse
datasets reveal that FastSAM3D achieves a remarkable speedup of $527.38\times$
compared to 2D SAMs and $8.75\times$ compared to 3D SAMs on the same volumes
without significant performance decline. Thus, FastSAM3D opens the door for
low-cost truly interactive SAM-based 3D medical imaging segmentation with
commonly used GPU hardware. Code is available at
https://github.com/arcadelab/FastSAM3D.

###### Keywords:

Foundation Model Segment Anything Model (SAM) Interactive Segmentation Model
Acceleration.

##  1 Introduction

In medical image analysis, object segmentation is a key aspect of diagnosis-
and prognosis-related tasks including lesion localization, tissue
characterization, and volume estimation, among others [8, 21, 29, 14].
Traditionally, deep learning models like U-Net [22] and variants [15, 11] have
excelled in specific tasks and datasets with clear and confined scope, but
often demonstrate limited generalization. While some work considered
interactive segmentation approaches as a means to overcome the limitations of
narrowly scoped, task-specific models [1, 26], the introduction of Segment
Anything Model (SAM) [16] initiated a paradigm shift to prompt-based
interactive segmentation that now provides competitive performance due to the
inherent generalizability of foundation models. SAM is comprised of a pre-
trained Vision Transformer (ViT) encoder [9], a prompt encoder, and a
lightweight decoder that facilitates multi-mask prediction via IoU-based
ranking. Trained on over 1 billion masks and 11 million images, SAM adapts to
new tasks without training [16]. Despite successes on natural images [10, 17],
direct application of SAM to medical segmentation reveals performance gaps
compared to task-specific U-Nets [33].

Table 1:  Comparison of SAM approaches regarding applicability for medical
imaging, suitability for 3D volumetric data, and computational efficiency of
the core components: image encoder, prompt encoder, and mask decoder. The
vanilla SAM [16] lacks in all criteria. MobileSAM [32] improves encoder
efficiency, while TinySAM [24] accelerates all components, but neither
addresses 3D medical imaging data. MedSAM [18] and SAM-Med2D [4] are tailored
for medical 2D data yet do not improve efficiency. SAM-Med3D [27] handles 3D
medical data but inference times for these limit or altogether preclude real-
time interactive use with standard GPU hardware. Our proposed FastSAM3D meets
all criteria, providing a comprehensive solution for efficient interactive
medical image segmentation in volumetric 3D data.

Method | Medical |  Volumetric 3D Data |  Efficient Image Encoder |  Efficient Prompt Encoder |  Efficient Mask Decoder
---|---|---|---|---|---
SAM [16] | ✗ | ✗ | ✗ | ✗ | ✗
MobileSAM [32] | ✗ | ✗ | ✓ | ✗ | ✗
TinySAM [24] | ✗ | ✗ | ✓ | ✓ | ✓
MedSAM [18] | ✓ | ✗ | ✗ | ✗ | ✗
SAM-Med2D [4] | ✓ | ✗ | ✗ | ✗ | ✗
SAM-Med3D [27] | ✓ | ✓ | ✗ | ✗ | ✗
FastSAM3D (ours) | ✓ | ✓ | ✓ | ✓ | ✓

To address this, MedSAM [18] and SAM-Med2D [4] were tailored for 2D medical
data via model fine-tuning. When applied to 3D volumetric data, these
approaches under-perform due to slice-wise processing [19, 3]. They also
suffer from an increased computational cost that is proportional to the number
of slices in the volume, as well as the higher input resolution. Addressing
this gap, SAM-Med3D [27] introduced 3D counterparts of SAM’s components and
end-to-end 3D training.

Existing medical SAMs also face limitations of long inference times and high
computational costs stemming from the Transformer architecture [9]. Prior
efforts accelerated 2D SAMs for natural images via approaches such as FastSAM,
which employs a YOLOv8 as the image encoder [2, 35]. However, this CNN-based
approach exhibits limitations with small object segmentation and deviates from
SAM’s interactive prompting design [32, 35]. Attempts, more aligned with the
SAM value proposition, such as MobileSAM, retain the Transformer encoder while
employing distillation to transition from a larger SAM encoder to a more
lightweight ViT encoder [32]. Following a similar approach, other works have
explored several ViT variants as alternative encoders to balance efficiency
and effectiveness [34, 25]. TinySAM further reduces computational load via
post-distillation quantization [24]. However, these advancements remain
confined to 2D natural images without delving into efficient volumetric
medical segmentation. Table 1 offers a systematic comparison of existing SAMs,
highlighting the capabilities of our proposed method in addressing the demands
of 3D medical image segmentation with enhanced efficiency across all
components.

The contributions of this work are two-fold, summarized as follows: Firstly,
we introduce FastSAM3D, a markedly more efficient 3D SAM for interactive
volumetric medical image segmentation. Rather than costly training from
scratch which also leads to the difficulty in convergence [12], we propose a
layer-wise progressive distillation approach to transfer representational
knowledge from a complex 12-layer ViT-B architecture to an efficient
customized 6-layer ViT-Tiny encoder. This retains segmentation performance
while significantly enhancing computational efficiency. Secondly, we propose a
novel 3D sparse flash attention that replaces the standard self-attention
operator in all SAM components, dramatically reducing memory footprint, and
enabling parallel processing. Together, these innovations address the
efficiency limitations that hinder the implementation of medical SAMs for
real-time prompt-based interactive 3D segmentation.

##  2 Methods

###  2.1 Architecture Overview of FastSAM3D

We introduce FastSAM3D, a computationally efficient adaptation of SAM-Med3D
[27], also designed specifically for efficient interactive 3D medical image
segmentation. Adhering to the standard SAM paradigm [16], FastSAM3D is
comprised of three key modules (Fig. 1): (i) a ViT-based image encoder [9] to
obtain volumetric embeddings; (ii) a prompt encoder; and (iii) a mask decoder
to project representations back to the segmentation mask. To achieve faster
inference, FastSAM3D distills knowledge from a high-powered 12-layer ViT-B
encoder to a streamlined 6-layer ViT-Tiny variant, substantially reducing
computational complexity during encoding. Specifically, aside from having
fewer layers, each Transformer block contains only 6 attention heads, in
contrast to 12 heads per block in SAM-Med3D’s ViT architecture. Moreover, we
retain the feed-forward network (FFN) within the first two transformer blocks
and omit attention operations [9], incurring minimal impact on performance
while amplifying speed [31]. This design choice further contributes to shorter
training by requiring fewer layers to align with the teacher during our
progressive distillation process.

Figure 1: The overall framework of FastSAM3D, comprising a 6-layer ViT-Tiny
variant image encoder distilled from a capable 12-layer ViT-B teacher encoder,
a lightweight prompt encoder, and a mask decoder. All the self attention
operators are replaced by the proposed 3D sparse attention for better
efficiency.

###  2.2 Layer-wise Progressive Distillation for the Image Encoder

As the image encoder accounts for a major portion of SAM’s computational load,
our first focus is transferring knowledge from the heavy ViT-B architecture to
a lightweight ViT-Tiny model for efficiency gains. To avoid costly training
from scratch, we follow the teacher-student distillation paradigm [12] by
designating the 12-layer ViT-B as the teacher model, $f_{\text{teacher}}$, and
the 6-layer ViT-Tiny variant as the student model, $f_{\text{student}}$.
Unlike traditional logit-level distillation [12] with which all our
experiments failed to converge, we propose a novel layer-wise progressive
distillation method. This approach allows for a more granular and effective
knowledge transfer between the student and teachers by matching the
intermediate representation progressively across layers, thus making it easier
for optimization. Formally, let $f_{\text{teacher}}^{(i)}(\mathbf{x})$ and
$f_{\text{student}}^{(j)}(\mathbf{x})$ denote layer $i=1,\cdots,12$ and
$j=1,\cdots,6$ outputs for an input $\mathbf{x}\in\mathbb{R}^{128\times
128\times 128}$ from the 12-layer teacher and 6-layer student respectively.
The objective of our layer-wise progressive distillation becomes:

$\mathcal{L}=\mathbb{E}_{\mathbf{x}}\Big{(}\frac{1}{k}\sum_{i=1}^{k}\|f_{\text{teacher}}^{(2i)}(\mathbf{x})-f_{\text{student}}^{(i)}(\mathbf{x})\|\Big{)},$
(1)

where $\|\cdot\|$ denotes the L2-norm, $k$ varies from 1 to 6 based on current
and total training iterations:

$k=\lceil\frac{\\#(\text{Current Iteration})\times 6}{\\#(\text{Total
Iterations})}\rceil,$ (2)

where $\lceil\cdot\rceil$ is the upper rounding operator. This enables
progressive alignment of student and teacher intermediate representations.
After finishing layer-wise distillation, we perform logit-level distillation
to fit predictions further. In Eq. 1, $\mathbb{E}(\cdot)$ represents the
expectation over all possible images.

###  2.3 3D Sparse Flash Attention

As we observe that the attention operators take up the largest proportion of
computation, we introduce a 3D sparse flash attention operator to further
enhance efficiency. Specifically, our 3D sparse flash attention scheme
supplants the traditional self-attention operation in both the encoder and
decoder, integrating extended receptive fields inspired by dilated
convolutions [30] with the computational agility achieved by flash attention
[6, 5].

####  2.3.1 3D Sparse Attention

The 3D sparse attention mechanism aims to expand the receptive field across
volumetric data while effectively managing the computational load. Traditional
attention mechanisms tend to escalate in computational demand proportional to
the increase in data volume, particularly challenging for 3D volumetric data
due to its large number of tokens [9, 23]. To address this, our approach
segments the input token sequence into equally sized partitions of $w$ and
applies a strategic sparsification across these segments [7]. This involves
selectively sampling data points at the determined intervals with length $r$,
thereby diminishing the overall number of tokens subjected to the attention
process. This allows for more efficient computation by focusing attention on
fewer yet representative tokens. Formally, the 3D sparse attention mechanism
can be formulated as computing the attention over each segment as follows:

$\hat{S}_{i}=[S_{i},S_{i+r},\ldots,S_{i+(w-1)r}],$ (3)

where $\hat{S}_{i}$ represents the selectively sampled segment, ensuring that
the model’s attention is distributed across a sparse set of points, thereby
reducing computational demands without sacrificing the depth of contextual
analysis.

####  2.3.2 Enhancing Efficiency through Parallel Processing with Flash
Attention

We enhance efficiency by processing each segment in 3D sparse attention
independently, enabling parallel operations that significantly boost
computational throughput. By incorporating flash attention [6, 5], our model
optimizes the functionality of parallel attention heads, substantially
reducing the time and memory overhead associated with simultaneous processing
activities.

####  2.3.3 Overall Processing Procedure

The 3D sparse flash attention operator, integral to both the image encoder and
mask decoder, operates through a sequence of orchestrated steps as follows.
The process starts with the sparsification step, wherein the input sequence
undergoes partitioning into sparse segments. Subsequently, the attention
operation ensues, wherein the previous segments are subjected to the flash
attention for parallelization [6, 5]. The focus of this stage is on harnessing
the reduced sequential computation and memory optimization capabilities of
flash attention. The final phase is recomposition [7], where the discrete
outputs procured from the flash attention are reassembled to form the final
encoded representation. This stage ensures that the final encoded
representation has an identical dimension to its input.

##  3 Experiments

Table 2:  Performance comparison of 2D and 3D SAM approaches in terms of Dice
score. We measure the performance at 1, 3, 5, and 10 point prompts (pt). SAM-
Med3D and our FastSAM3D are evaluated in a 3D context, whereas SAM, MobileSAM,
TinySAM, MedSAM and SAM-Med2D are applied independently to all 2D slices of
the entire 3D volume. Notably, FastSAM3D demonstrates competitive performance
with SAM-Med3D and shows enhanced Dice scores relative to all its 2D
counterparts, highlighting the effectiveness of our approach. The best
performance is shown in red and boldface, while the second best is in blue.

Dim | Method | AMOS [13] | TotalSegmentator [28] | BraTS [20]
---|---|---|---|---
1pt | 3pt | 5pt | 10pt | 1pt | 3pt | 5pt | 10pt | 1pt | 3pt | 5pt | 10pt
2D |  SAM [16] | $0.049$ | $0.093$ | $0.114$ | $0.145$ | $0.202$ | $0.279$ | $0.311$ | $0.348$ | $0.108$ | $0.192$ | $0.217$ | $0.237$
MobileSAM [32] | $0.041$ | $0.056$ | $0.063$ | $0.070$ | $0.149$ | $0.170$ | $0.182$ | $0.212$ | $0.079$ | $0.132$ | $0.156$ | $0.186$
TinySAM [24] | $0.049$ | $0.077$ | $0.089$ | $0.101$ | $0.171$ | $0.225$ | $0.243$ | $0.262$ | $0.103$ | $0.165$ | $0.187$ | $0.211$
MedSAM [18] | $0.004$ | $0.051$ | $0.060$ | $0.074$ | $0.006$ | $0.069$ | $0.090$ | $0.111$ | $0.008$ | $0.059$ | $0.064$ | $0.071$
SAM-Med2D [4] | $0.097$ | $0.127$ | $0.129$ | $0.132$ | $0.008$ | $0.081$ | $0.100$ | $0.128$ | $0.013$ | $0.076$ | $0.082$ | $0.084$
3D |  SAM-Med3D [27] | $0.289$ | $0.386$ | $0.418$ | $0.448$ | $0.252$ | $0.400$ | $0.463$ | $0.522$ | $0.328$ | $0.395$ | $0.418$ | $0.446$
FastSAM3D | $0.273$ | $0.368$ | $0.402$ | $0.437$ | $0.250$ | $0.378$ | $0.445$ | $0.519$ | $0.333$ | $0.401$ | $0.421$ | $0.445$

####  3.0.1 Implementation Details

Our method as well as all baseline methods are implemented in Python 3.9 and
PyTorch 2.1.0. The computational environment for our experiments is
standardized across all methods, utilizing an NVIDIA A100 GPU with 40Gb of
memory. For the layer-wise progressive distillation, we set the total training
iteration number in Eq. (2) to $36$. Training is facilitated by the Adam
optimizer, with a learning rate of $5\times 10^{-3}$ and a batch size of 16.
For evaluation metrics, we use the Dice score to measure segmentation
performance. We also report inference time, floating point operations (FLOPs),
and memory cost to quantify the computational complexity.

####  3.0.2 Datasets

Our evaluation incorporates three diverse datasets that span two modalities,
namely computed tomography (CT) and magnetic resonance imaging (MRI), where we
follow the dataset splits of previous work [27]. (1) The AMOS dataset [13] is
a substantial and varied clinical collection designed for abdominal organ
segmentation with 500 CT and 100 MRI scans. (2) The TotalSegmentator dataset
[28] consists of 1228 CT studies each with 117 anatomical structures acquired
from different pathologies, scanners, series, and institutions. (3) The BraTS
2021 dataset [20] assembles a total number of 1251 multi-institutional MRI
scans.

Table 3:  Comparison of the computational efficiency with respect to the
encoder and decoder. We report the time (ms), FLOPs (G), and memory (Gb),
alongside acceleration factors relative to 2D SAM [16] and 3D SAM-Med3D [27].
For 2D SAMs, we compute the time to process all the slices within volumetric
data. The best results are highlighted in bold if statistically different from
the second best result ($p<0.01$).

Dim | Method | Resolution | Encoder | Decoder | Acceleration
---|---|---|---|---|---
Time (ms)$\downarrow$ |  FLOPs (G)$\downarrow$ |  Memory (Gb)$\downarrow$ |  Time (ms)$\downarrow$ |  FLOPs (G)$\downarrow$ |  Memory (Gb)$\downarrow$ | To 2D $\uparrow$ | To 3D $\uparrow$
2D |  SAM [16] | $1024\times 1024$ | $3980$ | $369.0$ | $7.87$ | $239$ | $3.0$ | $5.57$ | $1.00\times$ | /
MobileSAM [32] | $1024\times 1024$ | $584$ | $36.7$ | $5.48$ | $233$ | $3.0$ | $5.27$ | $5.16\times$ | /
TinySAM [24] | $1024\times 1024$ | $609$ | $36.7$ | $5.48$ | $246$ | $3.0$ | $5.27$ | $4.93\times$ | /
MedSAM [18] | $1024\times 1024$ | $3983$ | $369.0$ | $7.87$ | $241$ | $2.9$ | $5.57$ | $1.00\times$ | /
SAM-Med2D [4] | $256\times 256$ | $1063$ | $32.0$ | $6.32$ | $216$ | $0.21$ | $5.55$ | $3.30\times$ | /
3D |  SAM-Med3D [27] | $128\times 128\times 128$ | $70$ | $89.5$ | $6.58$ | $20$ | $2.8$ | $5.53$ | $60.27\times$ | $1.00\times$
FastSAM3D | $128\times 128\times 128$ | $3$ | $21.9$ | $0.78$ | $5$ | $2.8$ | $0.71$ | $527.38\times$ | $8.75\times$

Table 4:  Ablation study for the contribution of 3D sparse attention (‘Sparse
Attn.’) and flash attention (‘Flash Attn.’) to the performance and efficiency
of FastSAM3D. Best scores are highlighted in bold, if statistically different
from the second best result ($p<0.01$). 3D sparse attention and flash
attention contribute to substantial improvements in time and memory
requirements without statistically significant performance decline.

Sparse Attn. |  Flash Attn. | AMOS [13] | TotalSegmentator [28] | BraTS [20] | Encoder
---|---|---|---|---|---
1pt | 3pt | 5pt | 10pt | 1pt | 3pt | 5pt | 10pt | 1pt | 3pt | 5pt | 10pt | Time | FLOPs | Memory
✗ | ✗ | $0.282$ | $0.375$ | $0.403$ | $0.436$ | $0.243$ | $0.371$ | $0.442$ | $0.516$ | $0.335$ | $0.404$ | $0.422$ | $0.444$ | $10$ | $23.1$ | $1.16$
✗ | ✓ | $0.276$ | $0.366$ | $0.398$ | $0.432$ | $0.247$ | $0.374$ | $0.438$ | $0.516$ | $0.331$ | $0.402$ | $0.421$ | $0.445$ | $6$ | $21.9$ | $1.15$
✓ | ✗ | $0.277$ | $0.370$ | $0.402$ | $0.433$ | $0.255$ | $0.381$ | $0.450$ | $0.520$ | $0.328$ | $0.403$ | $0.422$ | $0.445$ | $9$ | $23.1$ | $0.79$
✓ | ✓ | $0.273$ | $0.368$ | $0.402$ | $0.437$ | $0.250$ | $0.378$ | $0.445$ | $0.519$ | $0.333$ | $0.401$ | $0.421$ | $0.445$ | $3$ | $21.9$ | $0.78$

####  3.0.3 Performance Comparison

Table 2 compares segmentation performance for FastSAM3D with various 2D and 3D
SAM approaches. Fig. 2 provides an illustrative visualization for samples
segmented by different methods. FastSAM3D not only demonstrates competitive
segmentation performance in comparison to its teacher model, SAM-Med3D, but
also surpasses all 2D efficient SAM models, especially when the number of
point prompts is increased. For example, FastSAM3D achieves a Dice score of
$0.437$ on the AMOS dataset with 10 point prompts, which is a significant
improvement over the $0.306$ score from the best-performing 2D model
($p<0.01$). This trend is consistent across the TotalSegmentator and BraTS
datasets, underscoring the robustness of FastSAM3D across different datasets,
modalities, and organs. Additionally, 2D SAM methods require intensive per-
slice prompting as opposed to FastSAM3D which only involves volume-level
interactions.

####  3.0.4 Computational Efficiency Comparison

Regarding the computational efficiency, Table 3 reveals that FastSAM3D reduces
the inference time for the encoder to 3 milliseconds and decoder to 5
milliseconds for 3D volumetric images, a substantial improvement from the
$3980$ milliseconds required by the vanilla SAM employed in a slice-by-slice
manner. Moreover, FastMed3D requires fewer FLOPs and less memory than all
counterparts, achieving a $527.38\times$ acceleration compared to the vanilla
SAM and $8.75\times$ acceleration compared to SAM-Med3D.

Figure 2: Representative segmentation results from all methods across three
datasets. FastSAM3D demonstrates accurate contour delineation comparable to
SAM-Med3D.

####  3.0.5 Ablation Study

Table 4 illustrates the effectiveness of both sparse and flash attention in
optimizing computational efficiency. Specifically, when neither 3D sparse nor
flash attention mechanisms were applied, the model achieved a Dice score of
$0.436$ on the AMOS dataset with 10 prompts. The introduction of 3D sparse
attention marginally reduces the Dice score to $0.433$ from $0.436$ on AMOS
but substantially reduces memory consumption from $1.06$ Gb to $0.79$ Gb.
Flash attention alone improves inference time from $10$ ms to $6$ ms,
underscoring its impact on computational efficiency. Moreover, the concurrent
implementation of both sparse and flash attention yields the most substantial
improvements. For instance, the Dice score on the AMOS dataset with 10 prompts
increases to $0.437$, and the encoder time is reduced to 3 ms, Memory
requirements are also minimized to $0.78$ Gb, suggesting an optimized model
footprint.

##  4 Conclusion

We present FastSAM3D, an innovative adaptation of SAM for efficient
segmentation of volumetric medical imaging data. This model addresses the
critical challenges of high inference time and the substantial computational
cost associated with previous 3D SAM methods. Through a novel layer-wise
progressive distillation and 3D sparse flash attention integration, we
significantly reduce computational demands while maintaining high segmentation
performance. Our experiments across different modalities and organs
demonstrate that FastSAM3D not only accelerates inference by factors of
$527.38\times$ compared to 2D SAMs and $8.75\times$ to 3D SAMs but also
retains the flexibility of SAM’s interactivity, making it a promising and
powerful tool for clinical deployment. FastSAM3D opens up the possibility of
real-time human-machine interaction by facilitating rapid prompting volumetric
segmentation, thereby potentially maximizing user agency and trust while
minimizing effort, workload, and wait time-related frustration. With the speed
and efficiency of FastSAM3D, another possible direction includes the
development of mixed reality (MR) applications for surgical planning and
guidance.

####  4.0.1 Acknowledgements.

This work was supported in part by grants from the National Institutes of
Health (NIH R01 GM148987-01).

## References

  * [1] Amrehn, M., Gaube, S., Unberath, M., Schebesch, F., Horz, T., Strumia, M., Steidl, S., Kowarschik, M., Maier, A.: Ui-net: Interactive artificial neural networks for iterative image segmentation based on a user model. arXiv preprint arXiv:1709.03450 (2017)
  * [2] Bolya, D., Zhou, C., Xiao, F., et al.: Yolact: Real-time instance segmentation. In: Proceedings of the IEEE/CVF international conference on computer vision. pp. 9157–9166 (2019)
  * [3] Bui, N.T., Hoang, D.H., Tran, M.T., et al.: Sam3d: Segment anything model in volumetric medical images. arXiv preprint arXiv:2309.03493 (2023)
  * [4] Cheng, J., Ye, J., Deng, Z., et al.: Sam-med2d. arXiv preprint arXiv:2308.16184 (2023)
  * [5] Dao, T.: Flashattention-2: Faster attention with better parallelism and work partitioning. arXiv preprint arXiv:2307.08691 (2023)
  * [6] Dao, T., Fu, D., Ermon, S., et al.: Flashattention: Fast and memory-efficient exact attention with io-awareness. Advances in Neural Information Processing Systems 35, 16344–16359 (2022)
  * [7] Ding, J., Ma, S., Dong, L., et al.: Longnet: Scaling transformers to 1,000,000,000 tokens. arXiv preprint arXiv:2307.02486 (2023)
  * [8] Dora, L., Agrawal, S., Panda, R., et al.: State-of-the-art methods for brain tissue segmentation: A review. IEEE reviews in biomedical engineering 10, 235–249 (2017)
  * [9] Dosovitskiy, A., Beyer, L., Kolesnikov, A., et al.: An image is worth 16x16 words: Transformers for image recognition at scale. arXiv preprint arXiv:2010.11929 (2020)
  * [10] Gao, H., Li, Y., Long, K., et al.: A survey for foundation models in autonomous driving. arXiv preprint arXiv:2402.01105 (2024)
  * [11] He, Z., Unberath, M., Ke, J., et al.: Transnuseg: A lightweight multi-task transformer for nuclei segmentation. In: International Conference on Medical Image Computing and Computer-Assisted Intervention. pp. 206–215. Springer (2023)
  * [12] Hinton, G., Vinyals, O., Dean, J.: Distilling the knowledge in a neural network. arXiv preprint arXiv:1503.02531 (2015)
  * [13] Ji, Y., Bai, H., Ge, C., et al.: Amos: A large-scale abdominal multi-organ benchmark for versatile medical image segmentation. Advances in Neural Information Processing Systems 35, 36722–36732 (2022)
  * [14] Jiang, H., Diao, Z., Yao, Y.D.: Deep learning techniques for tumor segmentation: a review. The Journal of Supercomputing 78(2), 1807–1851 (2022)
  * [15] Ke, J., Lu, Y., Shen, Y., et al.: Clusterseg: A crowd cluster pinpointed nucleus segmentation framework with cross-modality datasets. Medical Image Analysis 85, 102758 (2023)
  * [16] Kirillov, A., Mintun, E., Ravi, N., et al.: Segment anything. arXiv preprint arXiv:2304.02643 (2023)
  * [17] Liu, X., Zhou, T., Wang, Y., et al.: Towards the unification of generative and discriminative visual foundation model: A survey. arXiv preprint arXiv:2312.10163 (2023)
  * [18] Ma, J., He, Y., Li, F., et al.: Segment anything in medical images. Nature Communications 15(1), 654 (2024)
  * [19] Mazurowski, M.A., Dong, H., Gu, H., et al.: Segment anything model for medical image analysis: an experimental study. Medical Image Analysis 89, 102918 (2023)
  * [20] Menze, B.H., Jakab, A., Bauer, S., et al.: The multimodal brain tumor image segmentation benchmark (brats). IEEE transactions on medical imaging 34(10), 1993–2024 (2014)
  * [21] Mirikharaji, Z., Abhishek, K., Bissoto, A., et al.: A survey on deep learning for skin lesion segmentation. Medical Image Analysis p. 102863 (2023)
  * [22] Ronneberger, O., Fischer, P., Brox, T.: U-net: Convolutional networks for biomedical image segmentation pp. 234–241 (2015)
  * [23] Shen, Y., Guo, P., Wu, J.a.: Movit: Memorizing vision transformers for medical image analysis. In: International Workshop on Machine Learning in Medical Imaging. pp. 205–213. Springer (2023)
  * [24] Shu, H., Li, W., Tang, Y., Zhang, Y., Chen, Y., Li, H., Wang, Y., Chen, X.: Tinysam: Pushing the envelope for efficient segment anything model. arXiv preprint arXiv:2312.13789 (2023)
  * [25] Wang, A., Chen, H., Lin, Z., et al.: Repvit-sam: Towards real-time segmenting anything. arXiv preprint arXiv:2312.05760 (2023)
  * [26] Wang, G., Li, W., Zuluaga, M.A., Pratt, R., Patel, P.A., Aertsen, M., Doel, T., David, A.L., Deprest, J., Ourselin, S., et al.: Interactive medical image segmentation using deep learning with image-specific fine tuning. IEEE transactions on medical imaging 37(7), 1562–1573 (2018)
  * [27] Wang, H., Guo, S., Ye, J., et al.: Sam-med3d. arXiv preprint arXiv:2310.15161 (2023)
  * [28] Wasserthal, J., Breit, H.C., Meyer, M.T., et al.: Totalsegmentator: Robust segmentation of 104 anatomic structures in ct images. Radiology: Artificial Intelligence 5(5) (2023)
  * [29] Wu, J., Xu, Q., et al.: Swin transformer improves the idh mutation status prediction of gliomas free of mri-based tumor segmentation. Journal of Clinical Medicine 11(15), 4625 (2022)
  * [30] Yu, F., Koltun, V.: Multi-scale context aggregation by dilated convolutions. arXiv preprint arXiv:1511.07122 (2015)
  * [31] Yu, W., Luo, M., Zhou, P., Si, C., Zhou, Y., Wang, X., Feng, J., Yan, S.: Metaformer is actually what you need for vision. In: Proceedings of the IEEE/CVF conference on computer vision and pattern recognition. pp. 10819–10829 (2022)
  * [32] Zhang, C., Han, D., Qiao, Y., et al.: Faster segment anything: Towards lightweight sam for mobile applications. arXiv preprint arXiv:2306.14289 (2023)
  * [33] Zhang, Y., Shen, Z., Jiao, R.: Segment anything model for medical image segmentation: Current applications and future directions. arXiv preprint arXiv:2401.03495 (2024)
  * [34] Zhang, Z., Cai, H., Han, S.: Efficientvit-sam: Accelerated segment anything model without performance loss. arXiv preprint arXiv:2402.05008 (2024)
  * [35] Zhao, X., Ding, W., An, Y., et al.: Fast segment anything. arXiv preprint arXiv:2306.12156 (2023)