# High Curie Temperature Ferromagnetic Semiconductor: Bimetal Transition
Iodide V2Cr2I9

Yulu Ren  State Key Laboratory of Metastable Materials Science and Technology
& Key Laboratory for Microstructural Material Physics of Hebei Province,
School of Science, Yanshan University, Qinhuangdao 066004, China  Qiaoqiao Li
State Key Laboratory of Metastable Materials Science and Technology & Key
Laboratory for Microstructural Material Physics of Hebei Province, School of
Science, Yanshan University, Qinhuangdao 066004, China  Wenhui Wan  State Key
Laboratory of Metastable Materials Science and Technology & Key Laboratory for
Microstructural Material Physics of Hebei Province, School of Science, Yanshan
University, Qinhuangdao 066004, China  Yong Liu  State Key Laboratory of
Metastable Materials Science and Technology & Key Laboratory for
Microstructural Material Physics of Hebei Province, School of Science, Yanshan
University, Qinhuangdao 066004, China  Yanfeng Ge<EMAIL_ADDRESS>State Key
Laboratory of Metastable Materials Science and Technology & Key Laboratory for
Microstructural Material Physics of Hebei Province, School of Science, Yanshan
University, Qinhuangdao 066004, China

###### Abstract

Bimetal transition iodides in two-dimensional scale provide an interesting
idea to combine a set of single-transition-metal ferromagnetic semiconductors
together. Motivated by structural engineering on bilayer CrI3 to tune its
magnetism and works that realize ideal properties by stacking van der Waals
transitional metal dichalcogenides in a certain order. Here we stack monolayer
VI3 onto monolayer CrI3 with a middle-layer I atoms discarded to construct
monolayer V2Cr2I9. Based on this crystal model, the stable and metastable
phases are determined among 7 possible phases by first-principles
calculations. It is illustrated that both the two phases have Curie
temperature $\sim$ 6 (4) times higher than monolayer CrI3 and VI3. The reason
can be partly attributed to their large magnetic anisotropy energy (the
maximum value reaches 412.9 $\mu$eV/atom). More importantly, the Curie
temperature shows an electric field and strain dependent character and can
even surpass room temperature under a moderate strain range. At last, we
believe that the bimetal transition iodide V2Cr2I9 monolayer would support
potential opportunities for spintronic devices.

††preprint: APS/123-QED

##  I INTRODUCTION

The intrinsic ferromagnetic semiconductors (FMSs) in atomically thin scale
have exerted serious interests in spintronic devices and data storage area in
recent years, when the traditional bulk materials are hard to satisfy the
pursuit of nano-sized spintronic devices with high integration Huang2020 ;
Huang2017 ; Dietl2014 ; McGuire2015 ; Zhong2017 ; MacDonald2005 ; Dietl2010 .
Likewise, FMSs can also be used for spin injection, generation, manipulation,
and detection with the help of nowadays well-developed semiconductor
technology Li2016 . Different from bulk magnets, two-dimensional (2D)
magnetism though has long been at the heart of numerous experimental and
technological advances Hellman2017 ; Burch2018 ; Zak1990 ; Arnold1997 , is
rare for its vulnerability to thermal energy. Therefore, ferromagnetism in 2D
scale is conditional and should possess such fundamentals: (i) magnetic
anisotropy, (ii) exchange interaction Gong2019 ; Mermin1966 . Along with the
fact that ferromagnetism and semiconductivity are not very well compatible,
the amounts of FMSs in atomically thin are limited, let alone those with high
Curie temperature ($T_{c}$) Feng2017 .

A series of ferroelectric magnets are reported with high $T_{c}$ observed in
experiment such as layered metallic Fe3GeTe2 ($\sim$ 225 K) Fei2018 , VSe2
($\sim$ 300 K) Bonilla2018  and V doped WSe2 ($\sim$ 360K) Yun2020  but they
all show an absence of semiconductivity. In addition, although theoretical
works have predicted FMSs with high $T_{c}$ such as GdI2 monolayer ($\sim$ 241
K) Wang2020 , CrX (X = P, As, $\sim$ 232 and 855 K) Ma2020 , zinc-blende CrC
($\sim$ 1900 K) Huang2019  and Fe2Si ($\sim$ 780 K Sun2017 ), the
ferromagnetism in 2D FMSs can only be observed at a relatively low temperature
in experiment. Such as recently synthesized layered CrI3 ($\sim$ 45 K)
Huang2017 ; PJiang2018 ; Soriano2019 , VI3 ($\sim$ 51 K) Kong2019 ; Tian2019 ,
Cr2Ge2Te6 ($\sim$ 67.9 K) Gong2017  and Cr2Si2Te6 ($\sim$ 33 K) Lin2016 . So,
efforts have been devoted to tune the ferromagnetism and enhance $T_{c}$ by
electrons doping, tunable gate and stacking Deng2018 ; Yan2020 ; Frey2019 ;
Jiang2018 ; Wang2018 . For example, the magnetic phase can be switched in
bilayer CrI3, and $T_{c}$ can also be elevated in monolayer CrI3 by switching
iron gate Huang2017 ; Huang2018 ; McGuire2015 . Whose effect is also observed
in Cr2Ge2Te6 Verzhbitskiy2020 . Besides, breaking long-range out-of-plane
symmetry and employing tensile strain can also effectively affect the
magnetism, according to recent works Ren2020 ; Leon2020 ; Hu2020 ; Cui2020 ;
Abdollahi2020 .

Inspired by the layer-number dependent magnetic phase switch in FMSs CrI3
Huang2017 , we try to build a bilayer VI3 model [left panel of Fig. 1(a)] and
investigate magnetic behavior different with its prototype. Unfortunately, it
is found that no significant change in magnetic anisotropy or $T_{c}$ compared
with monolayer VI3 supply . Then we try to break out-of-plane symmetry by
substitute one V atoms layer with Cr atoms [middle panel of Fig. 1(a)], but
the calculation of phonon frequency reveals that this bilayer crystal is
dynamically unstable with a large imaginary frequency. Finally, also inspired
by a set of crystal models such as ferroelectrics layered In2Se3 Ding2017 , we
peel one I layer off to combine the bilayer compound into monolayer bimetal
transition iodide V2Cr2I9 [right panel of Fig. 1(a)]. It is rather interesting
that the imaginary frequency is eliminated after the structural alteration.
Therefore, this work is discussed mainly in three parts. Firstly, we give a
systematical investigation on wither the structural alteration is
theoretically feasible by using first-principles calculations to confirm the
stable and metastable states form 7 different phases of monolayer V2Cr2I9.
Next, we discuss that the two feasible phases show an enhancement on
ferromagnetism and higher $T_{c}$ compared to their prototypes. At last,
efforts are devoted to further tune the $T_{c}$ by external electric field and
strain. According to the results, V2Cr2I9 monolayer is likely to be
synthesized and shows a certain perspective in spintronic field as a member of
layered van der Waals FMSs family.

##  II RESULTS AND DISCUSSION

The monolayer V2Cr2I9 in Fig. 1(a) is obtained from monolayer CrI3 (P3112,
No.151) and VI3 (R$\overline{3}$, No.148). The calculated lattice constants of
monolayer CrI3 and VI3 is a1 = b1= 6.907 Å and a2 = b2 = 6.824 Å,
respectively, consistent with the experiments McGuire2015 ; Tian2019 . So a
1.05 % ($<$ 5 %) mismatch in ab lattice constants is obtained [(a1-a2)/a1].
Figures 1 (a) and 1 (b) show a honeycomb monolayer with V-Cr arraying parallel
with c axial. According to different polyhedron types formed by each Cr and V
atoms with their nearest six I atoms, four possible phases named P1 $\sim$ P4
are obtained as shown in Fig. 1c. In P1 model, each Cr-V unit shows an ABB
stacking with a V-I6 octahedron and a Cr-I6 trigonal prism. Not only the
discrepancy in stacking order, but a relative displacement along ab plane is
likely to obtain interesting phases. So, we give the whole V layer a small
rigid shift within ab plane based on ABB stacking Zollner2019 , followed by
atomic relaxation. It shows the distances between V1 and Cr1 $d_{V1-Cr1}$ are
right equal to $d_{V1-Cr2}$. That is, by moving V layer of P1 to [1/3 0 0],
[1/3 1/3 0] and [0 1/3 0], another three phases named P5, P6 and P7, are
confirmed respectively [Figs. 1(d), 1(e) and 1(f)].

Figure 1: (a) Structural evolution from bilayer VI3 to monolayer V2Cr2I9. (b)
Top view of the optimized structure of P1. The rhomboid area donates a
primitive cell containing two Cr, two V and nine I atoms, while the hexagon
area denotes a V-Cr unit. Red, gray and violet balls denote V, I and Cr atom,
respectively. (c) Schematic diagram for side view of a V-Cr unit for P1 $\sim$
P4. (d) Top view of optimized structure of P5, red and blue areas denote
hexagons formed by V and Cr hexagons, respectively. (e) Side view of crystal
structure for P5 $\sim$ P7. (f) Corresponding top-view schematics for P5
$\sim$ P7. The solid and hollow circles denote transition metal and I atoms,
respectively. Details for lattice parameters, bond lengths and angles are
shown in supporting materials supply .

We next check the stability and further determine stable or metastable phases.
Among P1 to P4, only P1 shows an absence of imaginary frequency while P2
$\sim$ P4 are dynamically unstable with imaginary frequency such as -2.815 THz
in P3. Among P5 to P7, we find P6 also shows dynamic stability (Fig. 2).
Furthermore, the ab initial molecular dynamic (AIMD) simulations lasting 8000
fs at room temperature are employed on P1 and P6. The total potential energy
shows a small fluctuation range in P1 and P6 and the final structures remain
basically honeycomb lattice, indicating thermal stable.

Figure 2: (a, c) Crystal temperature as a function of time by AIMD simulations
at 300 K for P1 and P6, respectively. (b, d) Total potential energy as a
function of time for P1 and P6, respectively. The green and red points mark
the maximum and minimum after 430 fs (grey area). The left insert figures are
corresponding phonon frequency band structures along high-symmetry points,
while the right inserts are corresponding top and side view of crystal
structures after 8000 fs AIMD simulations. Red, blue and silver bulls denote
V, Cr and I atoms, respectively.

Then, we set P1 as initial state while P5 $\sim$ P7 as final states to
investigate the potential barriers among them. Seven transient states onto the
reaction paths are linearly interpolated. The evolution of reaction energy
shows that the final states are 0.77 $\sim$ 0.87 eV/primitive cell lower than
initial P1 (Fig. 3). Among them, P6 is the most energetically favorable. It
also shows large potential barriers all in the three cases as 7.17 eV, 6.31 eV
and 8.04 eV/primitive cell for P5, P6 and P7, respectively. It can be partly
attributed to: (i) the movement of V layer in P1 should overcome exchange
interaction from the sublayer Cr atoms . The nearest-neighboring Cr atom is
only one for each V atom with a distance $d_{V-Cr}$ = 4.183 Å. It is boosting
before moving to final states whose nearest-neighboring Cr atoms are doubled
($d_{V-Cr}$ = 4.381 Å); (ii) the octahedron units formed by V-I6 are destroyed
during the moving process, which results in elevated energy; (iii) the
movement of top I layer should also overcome interaction from sublayer Cr
atoms. Anyway, such large potential barrier is desired because it hinders
transition between P1 and P6 due to moderate thermal effect, strain induced
from substrate or other external factors.

Figure 3:  (a) The transition path and the activation energy per primitive
cell from initial P1 to final states P5, P6 and P7, respectively, as a
function of step number. The inset is zoom-in figure for dotted oval area. Red
hexagon denotes V hexagons while blue denotes Cr hexagons. Note that I atoms
are hidden in the schematics.

The band structure of P6 shows a $\sim$ 0.15 eV direct band gap whose valence
band maximum (VBM) and conduction band minimum (CBM) both occur at M point
[Fig. 4(b)]. Relatively, in P1 it shows an indirect type but with a larger gap
of 1.15 eV. In both cases, I atoms mainly occupy lower states less than -1.23
eV, while states of V atoms locate mainly near the fermi level. The main
discrepancy is, Cr atoms take up only empty state and are highly localized at
$\sim$ 1.00 eV and $\sim$ 1.56 eV in P6 [Fig. 4(b)], while in P1, they occupy
fully filled band states from -1.4 eV to -2 eV [Fig. 4(a)], indicating a
strong hybridization between Cr and I atoms. Meanwhile, the VBM and CBM mainly
originate from V and I atoms in P1 while from I atoms in P6.

Figure 4: (a, b) Projected band structures on Cr, I and V atoms for P1 and P6
of monolayer V2Cr2I9, respectively. The insert in (b) shows the zoom-in figure
for black oval area. The green area in (a) and (b) denote band gaps.

The magnetic anisotropy energy (MAE) is considered as a requisite in 2D
materials according to Mermin-Wagner theorem Mermin1966 . To investigate the
ferromagnetism that exists in V2Cr2I9 monolayer, we calculate the angular-
dependent MAE for P1 and P6 (Fig. 5), defined as
MAE=$E_{\theta,\varphi}-E_{0,180}$, where $\theta$ and $\varphi$ denote polar
angle and azimuth angle in polar coordinate system [Fig. 5(d)]. In P1, it
displays that heavy coloration basically locates at the boundary of the
cookie-like MAE distribution as shown in Fig. 5(a). Meanwhile, the ring-shaped
distribution means MAE remains unchanged when spin vector S switches from
$\varphi=0^{\circ}$ to $\varphi=360^{\circ}$ in ab plane [Fig. 5(b)]. But when
it rotates from $\theta=0^{\circ}$ to $\theta=90^{\circ}$, a clear out-of-
plane anisotropy is demonstrated with the MAE elevating from 0 to 234.7
$\mu$eV per Cr (V) atom. In P6, it shows a lower symmetry with MAE
concentrating on [0 0 1] direction [Fig. 5(c)]. Furthermore, there exist not
only in-plane anisotropy but also out-of-plane anisotropy [Fig. 5(e)]. When
$\theta$ increases from 0 to $180^{\circ}$, the MAE declines from maximum as
412.9 $\mu$eV per Cr (V) atom in [0 0 1] to 0 in [0 0 $\overline{1}$]
direction. Therefore, the out-of-plane MAE possesses major contribution to
anisotropy in P6. Additionally, the MAE declines with distinct tendency when
$\theta$ increases with different $\varphi$. It probably results from the
breaking rotational symmetry by in-plane shift of V layer of P1.

Figure 5: (a, c) Angular dependence of MAE with the direction of magnetization
lying on the whole space for P1 and P6, respectively. (b, e) The whole-space
MAE projected onto polar coordinates for P1 and P6, respectively. The vertical
coordinates denote $\theta$ and circle coordinates denote $\varphi$. (d) The
spin vector S on the x, y, and z planes rotated with angles out-of-plane
$\theta$ and in-plane $\varphi$. Note that heavier coloration indicates the
increase in MAE in (a, c) and inversely, heavier coloration indicates the
decrease in (b, e). The calculation of MAE takes spin-orbital coupling (SOC)
effect into consideration.

We estimate $T_{c}$ by using Monte Carlo simulation with Heisenberg model
supply . The in-plane nearest-neighboring exchange constant J1⊥, next-nearest-
neighboring exchange constant J2⊥ and out-of-plane nearest-neighboring
exchange constant J1∥ are considered. J1⊥ is estimated to be -25.30 (-16.93)
meV for P1 (P6), which is 8 (5) times higher than monolayer CrI3. According to
the results, $T_{c}$ for ground-state P1 (P6) is calculated as $\sim$ 272 K
($\sim$ 194 K, Fig. 6). It shows a significant enhancement compared to the
prototypes e.g. monolayer CrI3 and VI3. The reason for boosted $T_{c}$ can be
mainly attributed to: (i) large MAE per Cr (V) atom, which means more thermal
energy is requisite to disorder long-range spin arrays. So the energy
difference between antiferromagnetism and ferromagnetism configurations is
expanded; (ii) The amount of near-90∘ I-Cr(V)-I bond angles per primitive cell
is doubled from CrI3 and VI3 compounds to V2Cr2I9 monolayer, leading to an
enhancement of superexchange interaction and a more stabilized parallel spin
configuration Goodenough1955 ; Goodenough1958 ; Kanamori1960 ; Anderson1959 .
Although direct exchange interaction is meanwhile moderately enhanced, it is
more sensitive to the distance between V-V (Cr) than superexchange interaction
Ren2020 .

Inspired by recent works on gate-dependence CrI3, we also employ
experimentally accessible longitudinal electric field of a few V/nm for P1 and
P6, as displayed in Figs. 6(a) and 6(c). Unlike quite narrow tunable range of
$T_{c}$ in P1 (i.e. from 266 K to 280 K), it shows a moderate change range of
$T_{c}$ in P6: When the electric field is tuned from positive to negative
values, it enables a variation of $T_{c}$ between 177 K and 208 K. Besides,
$T_{c}$ is elevated by switching electric field from negative to positive in
P1 while in P6 it declines.

Strain effect ($\varepsilon$), directly affects the bond lengths which possess
significant influence on exchange interaction in d-orbital honeycomb crystal.
Therefore, the strain effect on monolayer V2Cr2I9 is investigated as shown in
Figs. 6(b) and 6(d). A rather different ferromagnetism tuning behaviors are
found in P1 and P6. In the former, tensile and compressive strain both enable
an enhancement of $T_{c}$, which is more sensitive to tensile strain. In the
latter, $T_{c}$ is drastically elevated from 193 K to 328 K as $\varepsilon$
changing from 0 to $-4\%$. But for $0\leq\varepsilon\leq 4\%$, $T_{c}$ remains
just a slightly decrease from 193 K to 182 K. In addition, it is rather
fascinating that $T_{c}$ surpasses room temperature when $|\varepsilon|$
$\geq$ 2 % in P1 and $\varepsilon=-4\%$ in P6.

Figure 6: (a, c) Normalized magnetization as a function of temperature under
electric field ranging from -4 V/nm to 4 V/nm for P1 and P6, respectively. The
insets with colored curves are zoom-in figures for dashed oval area. While the
single-black curve inserts display $T_{c}$ as a function of electric field.
Additionally, at the bottom panel of (c) it shows a schematic of a 2D
magnetoelectric device with a longitudinal electric field. (b, d)
Magnetization as a function of biaxial strain from -4 % to 4 % for P1 and P6,
respectively. Similarly, the inserts show $T_{c}$ as a function of strain.
Note that the results are all calculated with SOC.

##  III Conclusion

By using first-principles calculations, we first combine the monolayer VI3 and
CrI3 into the newly constructed bimetal transition iodide V2Cr2I9 monolayer
and investigate the stability for a set of possible phases, which are obtained
by switching the stacking order of I atoms and by giving a rigid shift to V-I3
layer to [1/3 0 0], [1/3 1/3 0] and [0 1/3 0]. Among the 7 phases, it is
determined that only P6 is stable while P1 is metastable. By band structure
calculations, it shows a larger band gap for P1 while direct-type band gap for
P6. Next, crucial for the ferromagnetism exhibiting in dimensionality $\leq$
2, is the MAE estimated as a large value especially in P6. After that, we have
discussed that $T_{c}$ is 6 (4) times larger than monolayer CrI3 and VI3 in
ground state P1 (P6). Furthermore, $T_{c}$ is highly dependent on biaxial
electric field and strain, we can achieve an alteration of $T_{c}$ by
switching direction of electric field and by employing external strain. It is
believed that this work supports a new idea to combine two transition metal
elements into bimetal transition iodide monolayer by structure engineering.
Meanwhile, monolayer V2Cr2I9 probably possesses potential application in
spintronic devices as FMSs with the $T_{c}$ near room temperature.

##  IV METHODS

The first-principles calculations were performed using the projected
augmented-wave method Kresse1999 ; Blochl1994  as implemented in the Vienna Ab
initio Simulation Package (VASP) Kresse1996  based on Perdew-Burke-Ernzerhof
(PBE) functional. In our global calculations, we used a 450 eV cut-off energy,
0.05 eV width of smearing and a $7\times 7\times 1$ grid of the first
Brillouin-zone integration. Also, we remained the thickness of vacuum spacing
unchanged as 20 Å to reduce the interlayer interactions due to the periodic
boundary conditions. In most parts of the calculations, the Hellman-Feynman
force and total energy convergence criteria were employed less than $10^{-2}$
meV/Å and $10^{-6}$ eV. Note that the phonon-frequency and MAE calculations
require rather high precision, so the two convergence criteria were set to
$10^{-3}$ meV/Å and $10^{-8}$ eV to suffice the high accuracy of the results.
With regard to the crystal volume, a $3\times 3\times 1$ supercell model (117
atoms in total) was applied to perform phonon-frequency calculations and a
$2\times 2\times 1$ supercell model (52 atoms in total) in molecular-dynamic
simulations. Also, a $2\times 2\times 1$ supercell model was used to simulate
different spin configurations (e.g. Néel antiferromagnetic configuration). In
addition, the band structures were given by Heyd-Scuseria-Ernzerhof (HSE06)
functional including 25% non-local Hartree-Fock exchange Heyd2003 . The non-
collinear calculations were given by considering SOC effect SOC  in MAE and
electric field simulations. The phonon frequency calculations were carried out
by using DFT perturbation theory as implemented in the PHONOPY code Togo2008 .
And the AIMD simulations in the canonical (NVT) ensemble were performed at 300
K with a Nosé thermostat.

###### Acknowledgements.

This work was supported by National Natural Science Foundation of China
(No.11904312 and 11904313), the Project of Hebei Education Department, China
(No.ZD2018015 and QN2018012), and the Natural Science Foundation of Hebei
Province (No.A2019203507). Thanks to the High Performance Computing Center of
Yanshan University.

##  V References

## References

  * (1) P. Huang, P. Zhang, S. Xu, H. Wang, X. Zhang, and H. Zhang, Recent Advances in Two-Dimensional Ferromagnetism: Materials Synthesis, Physical Properties and Device Applications, Nanoscale 12, 2309 (2020).
  * (2) B. Huang, G. Clark, E. Navarro-Moratalla, D. R. Klein, R. Cheng, K. L. Seyler, D. Zhong, E. Schmidgall, M. A. McGuire, D. H. Cobden, W. Yao, D. Xiao, P. Jarillo-Herrero, and X. Xu, Layer-Dependent Ferromagnetism in a van Der Waals Crystal down to the Monolayer Limit, Nature 546, 7657 (2017).
  * (3) T. Dietl and H. Ohno, Dilute Ferromagnetic Semiconductors: Physics and Spintronic Structures, Rev. Mod. Phys. 86, 187 (2014).
  * (4) M. A. McGuire, H. Dixit, V. R. Cooper, and B. C. Sales, Coupling of Crystal Structure and Magnetism in the Layered, Ferromagnetic Insulator CrI3, Chem. Mater. 27, 2 (2015).
  * (5) D. Zhong, K. L. Seyler, X. Linpeng, R. Cheng, N. Sivadas, B. Huang, E. Schmidgall, T. Taniguchi, K. Watanabe, M. A. McGuire, W. Yao, D. Xiao, K.-M. C. Fu, and X. Xu, Van Der Waals Engineering of Ferromagnetic Semiconductor Heterostructures for Spin and Valleytronics, Sci. Adv. 3, e1603113 (2017).
  * (6) A. H. MacDonald, P. Schiffer, and N. Samarth, Ferromagnetic Semiconductors: Moving beyond (Ga, Mn) As, Nature Mater. 4, 195 (2005).
  * (7) T. Dietl, A Ten-Year Perspective on Dilute Magnetic Semiconductors and Oxides, Nat. Mater. 9, 965 (2010).
  * (8) X. Li and J. Yang, First-Principles Design of Spintronics Materials, Natl. Sci. Rev. 3, 365 (2016).
  * (9) F. Hellman, A. Hoffmann, Y. Tserkovnyak, G. S. D. Beach, E. E. Fullerton, C. Leighton, A. H. MacDonald, D. C. Ralph, D. A. Arena, H. A. Dürr, P. Fischer, J. Grollier, J. P. Heremans, T. Jungwirth, A. V. Kimel, B. Koopmans, I. N. Krivorotov, S. J. May, A. K. Petford-Long, J. M. Rondinelli, N. Samarth, I. K. Schuller, A. N. Slavin, M. D. Stiles, O. Tchernyshyov, A. Thiaville, and B. L. Zink, Interface-Induced Phenomena in Magnetism, Rev. Mod. Phys. 89, 025006 (2017).
  * (10) K. S. Burch, D. Mandrus, and J.-G. Park, Magnetism in Two-Dimensional van Der Waals Materials, Nature 563, 47 (2018).
  * (11) J. Zak, E. R. Moog, C. Liu, and S. D. Bader, Universal Approach to Magneto-Optics, J. Magn. Magn. Mater. 89, 107 (1990).
  * (12) C. S. Arnold, M. Dunlavy, and D. Venus, Magnetic Susceptibility Measurements of Ultrathin Films Using the Surface Magneto-Optic Kerr Effect: Optimization of the Signal-to-Noise Ratio, Rev. Sci. Instrum. 68, 4212 (1997).
  * (13) C. Gong and X. Zhang, Two-Dimensional Magnetic Crystals and Emergent Heterostructure Devices, Science 363, 6428 (2019).
  * (14) N. D. Mermin and H. Wagner, Absence of Ferromagnetism or Antiferromagnetism in One-or Two-Dimensional Isotropic Heisenberg Models, Phys. Rev. Lett. 17, 1133 (1966).
  * (15) Y. P. Feng, L. Shen, M. Yang, A. Wang, M. Zeng, Q. Wu, S. Chintalapati, and C.-R. Chang, Prospects of Spintronics Based on 2D Materials: Spintronics Based on 2D Materials, WIREs Comput. Mol. Sci. 7, e1313 (2017).
  * (16) Z. Fei, B. Huang, P. Malinowski, W. Wang, T. Song, J. Sanchez, W. Yao, D. Xiao, X. Zhu, A. F. May, W. Wu, D. H. Cobden, J.-H. Chu, and X. Xu, Two-Dimensional Itinerant Ferromagnetism in Atomically Thin Fe3GeTe2, Nature Mater. 17, 9 (2018).
  * (17) M. Bonilla, S. Kolekar, Y. Ma, H. C. Diaz, V. Kalappattil, R. Das, T. Eggers, H. R. Gutierrez, M.-H. Phan, and M. Batzill, Strong Room-Temperature Ferromagnetism in VSe2 Monolayers on van Der Waals Substrates, Nature Nanotech. 13, 289 (2018).
  * (18) S. J. Yun, D. L. Duong, D. M. Ha, K. Singh, T. L. Phan, W. Choi, Y. Kim, and Y. H. Lee, Ferromagnetic Order at Room Temperature in Monolayer WSe2 Semiconductor via Vanadium Dopant, Adv. Sci. 7, 1903076 (2020).
  * (19) B. Wang, X. Zhang, Y. Zhang, S. Yuan, Y. Guo, S. Dong, and J. Wang, Prediction of a Two-Dimensional High-$T_{C}$ f-Electron Ferromagnetic Semiconductor, Mater. Horiz. 7, 1623 (2020).
  * (20) A. N. Ma, P. J. Wang, and C. W. Zhang, Intrinsic Ferromagnetism with High Temperature, Strong Anisotropy and Controllable Magnetization in the CrX (X = P, As) Monolayer, Nanoscale 12, 5464 (2020).
  * (21) C. Huang, J. Feng, J. Zhou, H. Xiang, K. Deng, and E. Kan, Ultra-High-Temperature Ferromagnetism in Intrinsic Tetrahedral Semiconductors, J. Am. Chem. Soc. 141, 31 (2019).
  * (22) Y. Sun, Z. Zhuo, X. Wu, and J. Yang, Room-Temperature Ferromagnetism in Two-Dimensional Fe2 Si Nanosheet with Enhanced Spin-Polarization Ratio, Nano Lett. 17, 5 (2017).
  * (23) P. Jiang, L. Li, Z. Liao, Y. X. Zhao, and Z. Zhong, Spin Direction-Controlled Electronic Band Structure in Two-Dimensional Ferromagnetic CrI3, Nano Lett. 18, 6 (2018).
  * (24) H. Yan, Z. Feng, P. Qin, X. Zhou, H. Guo, X. Wang, H. Chen, X. Zhang, H. Wu, C. Jiang, and Z. Liu, Electric-Field-Controlled Antiferromagnetic Spintronic Devices, Adv. Mater. 32, 1905603 (2020).
  * (25) N. C. Frey, A. Bandyopadhyay, H. Kumar, B. Anasori, Y. Gogotsi, and V. B. Shenoy, Surface-Engineered MXenes: Electric Field Control of Magnetism and Enhanced Magnetic Anisotropy, ACS Nano 13, 2831 (2019).
  * (26) Z. Wang, T. Zhang, M. Ding, B. Dong, Y. Li, M. Chen, X. Li, J. Huang, H. Wang, X. Zhao, Y. Li, D. Li, C. Jia, L. Sun, H. Guo, Y. Ye, D. Sun, Y. Chen, T. Yang, J. Zhang, S. Ono, Z. Han, and Z. Zhang, Electric-Field Control of Magnetism in a Few-Layered van Der Waals Ferromagnetic Semiconductor, Nature Nanotech. 13, 554 (2018).
  * (27) D. Soriano, C. Cardoso, and J. Fernández-Rossier, Interplay between Interlayer Exchange and Stacking in CrI3 Bilayers, Solid State Commun. 299, 113662 (2019).
  * (28) T. Kong, K. Stolze, E. I. Timmons, J. Tao, D. Ni, S. Guo, Z. Yang, R. Prozorov, and R. J. Cava, VI3-a New Layered Ferromagnetic Semiconductor, Adv. Mater. 7 (2019).
  * (29) S. Tian, J.-F. Zhang, C. Li, T. Ying, S. Li, X. Zhang, K. Liu, and H. Lei, Ferromagnetic van Der Waals Crystal VI3, J. Am. Chem. Soc. 141, 13 (2019).
  * (30) C. Gong, L. Li, Z. Li, H. Ji, A. Stern, Y. Xia, T. Cao, W. Bao, C. Wang, Y. Wang, Z. Q. Qiu, R. J. Cava, S. G. Louie, J. Xia, and X. Zhang, Discovery of Intrinsic Ferromagnetism in Two-Dimensional van Der Waals Crystals, Nature 546, 7657 (2017).
  * (31) M.-W. Lin, H. L. Zhuang, J. Yan, T. Z. Ward, A. A. Puretzky, C. M. Rouleau, Z. Gai, L. Liang, V. Meunier, B. G. Sumpter, P. Ganesh, P. R. C. Kent, D. B. Geohegan, D. G. Mandrus, and K. Xiao, Ultrathin Nanosheets of CrSiTe3: A Semiconducting Two-Dimensional Ferromagnetic Material, J. Mater. Chem. C 4, 2 (2016).
  * (32) Y. Deng, Y. Yu, Y. Song, J. Zhang, N. Z. Wang, Z. Sun, Y. Yi, Y. Z. Wu, S. Wu, J. Zhu, J. Wang, X. H. Chen, and Y. Zhang, Gate-Tunable Room-Temperature Ferromagnetism in Two-Dimensional Fe3GeTe2, Nature 563, 7729 (2018).
  * (33) S. Jiang, L. Li, Z. Wang, K. F. Mak, and J. Shan, Controlling Magnetism in 2D CrI3 by Electrostatic Doping, Nature Nanotech. 13, 7 (2018).
  * (34) B. Huang, G. Clark, D. R. Klein, D. MacNeill, E. Navarro-Moratalla, K. L. Seyler, N. Wilson, M. A. McGuire, D. H. Cobden, D. Xiao, W. Yao, P. Jarillo-Herrero, and X. Xu, Electrical Control of 2D Magnetism in Bilayer CrI3, Nature Nanotech. 13, 7 (2018).
  * (35) I. A. Verzhbitskiy, H. Kurebayashi, H. Cheng, J. Zhou, S. Khan, Y. P. Feng, and G. Eda, Controlling the Magnetic Anisotropy in Cr2Ge2Te6 by Electrostatic Gating, Nat. Electron. 3, 460 (2020).
  * (36) Y. Ren, Q. Li, W. Wan, Y. Liu, and Y. Ge, High-Temperature Ferromagnetic Semiconductors: Janus Monolayer Vanadium Trihalides, Phys. Rev. B 101, 134421 (2020).
  * (37) A. M. León, J. W. González, J. Mejía-López, F. Crasto de Lima, and E. Suárez Morell, Strain-Induced Phase Transition in CrI3 Bilayers, 2D Mater. 7, 035008 (2020).
  * (38) X. Hu, Y. Zhao, X. Shen, A. V. Krasheninnikov, Z. Chen, and L. Sun, Enhanced Ferromagnetism and Tunable Magnetism in Fe3GeTe2 Monolayer by Strain Engineering, ACS Appl. Mater. Interfaces 12, 26367 (2020).
  * (39) Q. Cui, J. Liang, Z. Shao, P. Cui, and H. Yang, Strain-Tunable Ferromagnetism and Chiral Spin Textures in Two-Dimensional Janus Chromium Dichalcogenides, Phys. Rev. B 102, 094425 (2020).
  * (40) M. Abdollahi and M. Bagheri Tagani, Tuning Intrinsic Ferromagnetic and Anisotropic Properties of the Janus VSeS Monolayer, J. Mater. Chem. C 8, 13286 (2020).
  * (41) W. Ding, J. Zhu, Z. Wang, Y. Gao, D. Xiao, Y. Gu, Z. Zhang, and W. Zhu, Prediction of Intrinsic Two-Dimensional Ferroelectrics in In2Se3 and Other III2-VI3 van Der Waals Materials, Nat. Commun. 8, 1 (2017).
  * (42) K. Zollner, P. E. Faria Junior, and J. Fabian, Proximity Exchange Effects in MoSe2 and WSe2 Heterostructures with CrI2: Twist Angle, Layer, and Gate Dependence, Phys. Rev. B 100, 8 (2019).
  * (43) J. B. Goodenough, Theory of the Role of Covalence in the Perovskite-Type Manganites [La, M(II)]MnO3, Phys. Rev. 100, 564 (1955).
  * (44) J. B. Goodenough, J. An interpretation of the magnetic properties of the perovskite-type mixed crystals La1-xSrxCoO3-λ, Phys. Chem. Solids. 6, 287 (1958).
  * (45) J. Kanamori, Crystal Distortion in Magnetic Compounds, J. Appl. Phys. 31, S14 (1960).
  * (46) P. W. Anderson, New Approach to the Theory of Superexchange Interactions, Phys. Rev. 115, 2 (1959).
  * (47) G. Kresse and D. Joubert, From Ultrasoft Pseudopotentials to the Projector Augmented-Wave Method, Phys. Rev. B 59, 1758 (1999).
  * (48) P. E. Blöchl, Projector Augmented-Wave Method, Phys. Rev. B 50, 24 (1994).
  * (49) G. Kresse and J. Furthmüller, Efficient iterative schemes for ab initio total-energy calculations using a plane-wave basis set, Phys. Rev. B 54, 11169 (1996).
  * (50) J. Heyd, G.E. Scuseria, and M. Ernzerhof, Hybrid functionals based on a screened Coulomb potential, J. Chem. Phys. 118, 8207 (2003).
  * (51) A. Togo, F. Oba, and I. Tanaka, First-principles calculations of the ferroelastic transition between rutile-type and CaCl2 \- type SiO2 at high pressures, Phys. Rev. B 78, 134106 (2008).
  * (52) R. Pincak, J. Smotlacha, and M. Pudlak, Spin-orbit interaction in the graphitic nanocone, Eur. Phys. J. B 88, 17 (2015).
  * (53) Supporting material is available that contains details for crystal information, phonon dispersion relations for the other phases, estimation of $T_{c}$ and so on.


#  ViCAR: Visualizing Categories with
Automated Rewriting in Coq

Bhakti Shah*††Equal contribution William Spencer* Laura Zielinski*
Ben Caldwell Adrian Lehmann Robert Rand University of Chicago
Chicago, USA

###### Abstract

Abstract. We present ViCAR, a library for working with monoidal categories in
the Coq proof assistant. ViCAR provides definitions for categorical structures
that users can instantiate with their own verification projects. Upon
verifying relevant coherence conditions, ViCAR gives a set of lemmas and
tactics for manipulating categorical structures. We also provide a visualizer
that can display any composition and tensor product of morphisms as a string
diagram, showing its categorical structure. This enables graphical reasoning
and automated rewriting for Coq projects with monoidal structures.

##  1 Introduction

Just as category theory provides a unifying framework for diverse concepts in
mathematics, category theory can be used in formal verification as a basis for
generalization. We can abstract away common structural patterns to yield
reusable tactics, lemmas, and techniques for proof assistants. Many constructs
that appear in program verification resemble symmetric monoidal categories.
ViCAR, a library for Visualizing Categories with Automated Rewriting, takes
advantage of the shared structure across symmetric monoidal instances to
understand and manipulate morphisms in Coq.

ViCAR emerged from VyZX, an effort to verify the ZX-calculus, a graphical
reasoning system for quantum programs [17]. The ZX-calculus [6] forms a
symmetric monoidal category whose morphisms are the ZX-diagrams which make up
the language. ViCAR generalizes the tools developed in VyZX to assist Coq
verification for all concrete monoidal categories. ViCAR consists of three
parts: typeclasses for categorical structures in Coq, a visualizer to
represent morphisms using string diagrams, and a set of tactics for
manipulating typeclass instances.

Other popular examples of monoidal categories include the calculus of
relations and matrices. The former is the category whose objects are types and
morphisms are binary relations. The latter has matrices as its morphisms
between vector spaces. The similarities between these examples are initially
unclear. Reframing each categorically, however, reveals their shared structure
and hints at how the verification of one could help another. To explore and
justify this claim, we implemented each of these instances in Coq then applied
ViCAR’s monoidal category framework. We found that for a well-developed
project, we could easily instantiate the relevant categorical definitions. The
tactics and visualization gained were valuable and helped project-specific
proofs by removing proof and cognitive overhead. We discuss these examples in
more detail in Section 6.

ViCAR’s key contributions are as follows:

  * •

We define symmetric monoidal categories in Coq, easily instantiable by user-
created structures.

  * •

We present an automatic morphism visualizer. While working on a Coq proof, the
visualizer will parse the monoidal structure of the current proof state,
producing an image of its string diagram representation.

  * •

We provide a set of powerful automation tactics that users can access once
they have proven the necessary coherence conditions. They include foliate,
which automatically rewrites diagrams to common useful structures; assoc_rw,
which performs rewriting modulo associativity; and cat_simpl, a simplification
tactic for commonly occurring patterns.

We describe ViCAR’s contributions in detail, how to use them, and how they fit
into VyZX and other projects with categorical structure. We conclude the paper
with some discussion of the next steps for ViCAR. Our work is open source and
on GitHub: https://github.com/inQWIRE/VICaR.

##  2 Background

#### Formal verification and the Coq proof assistant

Formal verification is grounded in the idea that we can mathematically prove
that a computer program satisfies a specification. This guarantees that a
given piece of software performs as expected on all possible inputs. Formal
verification research focuses on developing new and more effective techniques
for these kinds of proofs. One approach uses proof assistants, which are
software (usually programming languages) that allow users to express and prove
various constructs, often mathematical, in code.

Among the most widely-used proof assistants is Coq [8]. It allows for writing
definitions in the style of a dependently-typed programming language and
proving statements in the style of mathematical proof. One powerful Coq
mechanism is custom tactics, written in the Ltac language, which automate
repetitive tasks across proofs. Often, Coq libraries offer a set of tactics to
abstract away technical details and perform complex actions. ViCAR aims to
provide such tactics for users verifying projects which have categorical
structure.

#### Symmetric monoidal categories

${{(A\otimes 1)\otimes B}}$${{A\otimes(1\otimes B)}}$${{(A\otimes
B)\otimes(C\otimes D)}}$${{((A\otimes B)\otimes C)\otimes
D}}$${{A\otimes(B\otimes(C\otimes D))}}$${{A\otimes B}}$${{(A\otimes(B\otimes
C))\otimes D}}$${{A\otimes((B\otimes C)\otimes
D)}}$$\scriptstyle{\alpha_{A,1,B}}$$\scriptstyle{\mathrm{id}_{A}\otimes\lambda_{B}}$$\scriptstyle{\rho_{A}\otimes\mathrm{id}_{B}}$$\scriptstyle{\alpha_{A\otimes
B,C,D}}$$\scriptstyle{\alpha_{A,B,C\otimes
D}}$$\scriptstyle{\alpha_{A,B,C}\otimes\mathrm{id}_{D}}$$\scriptstyle{\alpha_{A,B\otimes
C,D}}$$\scriptstyle{\mathrm{id}_{A}\otimes\alpha_{B,C,D}}$ Figure 1: The
triangle identity (left) and the pentagon identity (right)

Following the definition of Selinger [20], a (planar) monoidal category
consists of a base category $\mathcal{C}$ equipped with a bifunctor
$\otimes:\mathcal{C}\times\mathcal{C}\rightarrow\mathcal{C}$ called the tensor
product. The tensor product is required to be unital and associative, which
means there are natural isomorphisms whose components are, for objects
$A,B,C\in\mathcal{C}$,

$\displaystyle\lambda_{A}$ $\displaystyle:1\otimes A\xrightarrow{\sim}A,$
(left unitor) $\displaystyle\rho_{A}$ $\displaystyle:A\otimes
1\xrightarrow{\sim}A,$ (right unitor) $\displaystyle\alpha_{A,B,C}$
$\displaystyle:(A\otimes B)\otimes C\xrightarrow{\sim}A\otimes(B\otimes C).$
(associator)

These natural isomorphisms are required to be coherent. Concretely, this means
any diagram of a certain formal class made only of associators and unitors
must commute (for details, see Selinger [20]). This requirement boils down to
proving the commutativity of just two types of diagrams [10]. Specifically, a
monoidal category $\mathcal{C}$ is coherent if and only if the diagrams in
Figure 1 commute for all $A,B,C,D\in\mathcal{C}$ [10]

A monoidal category can further be braided, meaning that there is a natural
isomorphism whose components are, for objects $A,B\in\mathcal{C}$,

$\beta_{A,B}:A\otimes B\xrightarrow{\sim}B\otimes A.$ (braiding)

Again, two diagrams called the hexagon identities, which this time involve
braiding, must commute. Finally, a braided monoidal category is symmetric if,
for all $A,B\in\mathcal{C}$,

$\beta_{A,B}\circ\beta_{B,A}\simeq 1.$ (symmetry)

Essentially, symmetric monoidal categories have an almost-commutative tensor
product. We choose to focus on monoidal and symmetric monoidal categories
because of their prevalence and natural correspondence to string diagrams
[20]. String diagrams are a graphical way to represent morphisms, useful for
parsing complex structure. One of our goals is to unify verification, which is
almost always text-based, with visual reasoning. String diagrams are the
platform for doing so for monoidal categories. We define them concretely in
Section 4.

#### Categories in verification

In mathematics and computer science, symmetric monoidal categories are
everywhere. Commonly seen examples include the category of sets, the category
of finite vector spaces, and the simply-typed lambda calculus. In
verification, active projects whose core structure is a symmetric monoidal
category include the verification of the ZX-calculus [17] and that of causal
separation diagrams [4]. The ZX-calculus is a graphical language for
expressing quantum computation, while causal separation diagram allow us to
reason about parallel processes. Both constructs independently satisfy the
definitions of a symmetric monoidal category, though this fact is not directly
used in their verification.

Despite being in completely different domains, because of their shared
structure, the ZX-calculus and causal separation diagram have properties in
common that should be exploited to ease their verification. This is the idea
that inspired ViCAR and the gap in formal verification that we wanted to
address111We note that VyZX and causal separation diagrams are implemented in
different proof assistants, Coq and Agda, respectively. We chose to use Coq
for ViCAR.. We bridge this gap with our framework for instantiating monoidal
categories, our generalized rewriting tactics, and our morphism visualizer. We
prioritize automation and ease—we want users to be able to use ViCAR’s
features in their own proofs with minimal additional effort.

Other projects attempt to unify categorical reasoning, proof assistants, and
visualization. The Chyp proof assistant, for one, allows users to state
rewrite rules axiomatically and produces string diagrams to visualize the
rules in action [16]. ViCAR takes the alternative approach of requiring users
to prove their structures are instances of predefined category typeclasses. In
exchange for this effort, ViCAR proofs can be used within the greater context
of the Coq proof assistant and augment existing Coq projects. ViCAR’s approach
allows us to use categorical reasoning to verify existing software, while Chyp
is able to more easily handle rewrites modulo associativity.

##  3 Constructively defining categories in Coq

There are several preexisting examples of implementing category theory in Coq
[11, 13]. Though many of these libraries have significant developments, we
found they did not align with all of our goals. For instance, we want to
separate structural definitions from coherence conditions to enable easy
visualization of category instances, independent of their semantics. Moreover,
when working with categories in practice, some notion of morphism equivalence
is assumed, so we benefit by making this explicit in formal verification. For
ViCAR, we are interested in category theory as a means to generalize shared
structure. Our library is to be instantiated by active verification projects
across a range of domains. We made a number of technical decisions to reflect
this purpose.

We implement our categorical definitions using a hierarchy of Coq typeclasses
[21], a mechanism similar to interfaces in object-oriented programming.
Typeclasses specify and label a collection of types, possibly dependent on
each other, and instances of that typeclass must provide a concrete term for
each type. For example, LABEL:fig:coherence gives the part of the typeclass
for monoidal categories which translates the coherence conditions from Figure
1. Typeclasses can also inherit from each other. ViCAR’s typeclass hierarchy
starts with the base category, then monoidal category, braided monoidal, and
finally symmetric monoidal. A project may instantiate as many typeclasses as
is suitable for its purposes.

⬇

Class MonoidalCategoryCoherence {C : Type} {cC : Category C}

{cCh : CategoryCoherence cC} (mC : MonoidalCategory cC) : Type :$=$ {

triangle (A B : C) :

Î±_ A, I, B â (id_ A â Î»_ B)

â Ï_ A â id_ B;

pentagon (A B M N : C) :

(Î±_ A, B, M â id_ N) â Î±_ A, (B Ã M), N â (id_ A â Î±_ B, M, N)

â Î±_ (A Ã B), M, N â Î±_ A, B, (M Ã N);

(*Remainder omitted*)

}.

Listing 1: The triangle and pentagon identities in the
MonoidalCategoryCoherence typeclass.

A benefit of using typeclasses is Coq’s inference mechanism, which
automatically searches for typeclass instances [21]. This avoids having to
reference a particular instance every time one of its terms is used. For
example, suppose an instance catC of our category typeclass has been declared
whose objects have type $C$. Then, if $A,B$ and $M$ are terms of type $C$ and
f and g have types $A\leadsto B$ and $B\leadsto M$, the expression f $\circ$ g
would type check without the user having to explicitly point to the particular
instance. Coq would automatically retrieve it, determining that morphism
composition $\circ$ should be taken as defined by catC.

One important way ViCAR differs from existing formalizations of category
theory is its separation of structural definitions from coherence conditions.
Each abstract category has a typeclass containing just the necessary
structures, such as identity or the associator, and a different typeclass
specifying its coherence conditions. There are two separate hierarchies
accordingly. The benefit is that users can access the visualizer without
having to prove coherence, which may be more demanding. Instantiating a
structural typeclass with existing definitions is enough to begin using our
visualizer. Of course, without proving coherence, one has no guarantee that
the provided structure actually satisfies the criteria of an abstract
category, and therefore cannot use our automation.

Another way ViCAR diverges from other formalizations is by requiring users to
supply an explicit equivalence relation for morphisms, denoted $\simeq$,
instead of always using built-in equality. Using such an equivalence relation
is necessary for many standard constructions because Coq does not support
performing a quotient by an equivalence relation. By working over the supplied
morphism equivalence, we maintain this flexibility that many implementations
rely on. We also chose to use a diagrammatic compose for the notation $\circ$,
as our project focuses on visualization.

##  4 Visualization

#### Categorical String Diagrams

Reasoning about morphisms in categories is assisted by the use of string
diagrams, an associated graphical language. String diagrams visually represent
monoidal categories that are ordinarily represented in text form. Their
notation focuses on morphisms rather than objects, and can therefore very
concisely represent complicated expressions. We visualize our categories as
string diagrams to reduce cognitive overhead during proof.

Traditional string diagrams omit details such as associativity, so both
$f\circ(g\circ h)$ and $(f\circ g)\circ h$ are visualized as Figure 2, for
example. This is useful for pen-and-paper proofs but not for proof
assistants—formal proofs require each “obvious” detail to be addressed. In
Coq, $f\circ(g\circ h)$ and $(f\circ g)\circ h$ are two distinct terms,
equivalent only via rewriting (applying a theorem which states they are
equal). Identifying necessary rewrites is essential to the proof engineering
workflow, so we tweaked ViCAR’s string diagram notation to maintain all
parenthesizing explicitly. We represent these parentheses by circumscribing
boxes, and the differences can be easily identified as in Figure 3.

$f$$g$$h$ Figure 2: Visualization of both $f\circ(g\circ h)$ and $(f\circ
g)\circ h$ in traditional string diagrams.

(a) ViCAR visualization of (f $\circ$ g) $\circ$ h.

(b) ViCAR visualization of f $\circ$ (g $\circ$ h).

Figure 3: How ViCAR renders parentheses.

Our visualizations, while convenient for formal proof, are more verbose and
add layers of complexity over the simpler diagrams. Future extensions of ViCAR
hope to solve this problem, by automatically handling structure. This would
allow for diagrams to be canonically represented and for proof engineers to no
longer focus on structural rewrites. While work has been done on rewriting in
Coq modulo associativity and commutativity, we found none of it sufficient for
what ViCAR needs [3]. The current gap between existing modulo associativity
rules and this project relates to rules that depend on the interactions
between two operators, like $(f\circ g)\otimes(h\circ t)\simeq(f\otimes
h)\circ(g\otimes t)$. There are promising directions being developed on top of
e-graph based equality saturation, as we discuss in Section 7.

#### Visualization semantics and workflow

ViCAR allows for visualization of morphisms and morphism equivalences over
base category instances up to symmetric monoidal ones. We unlock functionality
as we deal with more expressive categories.

  * •

A morphism $f:A\leadsto B$ is visualized as a quadrilateral, marked with $A$
on the left and $B$ on the right.

  * •

The identity morphism for $A$ is denoted by a wire (horizontal line) with $A$
annotating the input and output positions.

  * •

Morphisms are composed by placing them side-by-side horizontally.

  * •

In monoidal categories, morphisms are tensored by placing them side-by-side
vertically.

  * •

Taking the inverse of the morphism is rendered in a box attached to left of
the morphism.

  * •

An isomorphism is a morphism with an emphasized bounding box.

  * •

Category-specific terms, such as the associator, are identified as such (with
the notation from Section 2).

  * •

In braided monoidal categories, the braiding is rendered as a big cross.

An example which uses several of these features can be seen in Figure 4, which
displays the statement of the triangle identity from LABEL:fig:coherence.

Figure 4: A visualization of the triangle identity.

One of ViCAR’s most convenient features is its integration into the Coq proof-
writing workflow. ViCAR is connected to the coq-lsp VSCode extension [9],
which type checks dynamically and prints the current goal state (hypotheses
and statements yet to be proved) based on cursor position within a proof. The
visualizer renders a string-diagrammatic goal state, alongside the printed
one, and updates automatically as the goal changes. The user’s setup can be
seen in Figure 5.

Because of this integration, the visualizer is able to use real-time
hypothesis information to inform rendering choices. This is useful for
distinguishing overloaded notation or opaque variables. For example, if the
variable f in a proof state is a morphism from A to B, the visualizer will
make this clear while the goal may not show it explicitly. Association and the
effect of braiding may also be unclear from the proof state. The visualizer
consults the hypothesis to check the type of each morphism and uses this
information to label the inputs and outputs of each morphism’s box.

Figure 5: User’s proof-writing IDE state

##  5 Automation

Categorical structure gives a well-defined domain on which we can develop
partial proof automation. Specifically, we can automate proofs of statements
that two morphisms are equivalent. This is the form of many theorems in
verification projects with monoidal structure. For example, theorems about
matrices take the form that certain matrices are equal, and theorems about the
ZX-calculus take the form that diagrams are proportional. These types of
proofs generally consist of rewrites and share common techniques, such as
manipulation of the underlying categorical structure. In this section, we
explain ViCAR’s tactics and how they can help with these proofs.

#### Coercing to categories

Coq will often fail to apply general categorical lemmas to proofs about
specific typeclass instances because it cannot recognize which terms
correspond to categorical structures. For example, suppose the category of
matrices (defined in full in Section 6.3) has been declared as a typeclass
instance, with composition and identity given by matrix multiplication and the
identity matrix. It would not be possible to rewrite the term I_n $\times$ A
with the lemma whose statement is id_ A $\circ$ f $\simeq$ f. Coq fails to
recognize that $\times$ is the composition of a declared category instance and
I_n is the identity.

To address this gap, we provide the tactic categorify. It performs setup
necessary for our automation to identify the structure of the goal. For the
category of matrices, calling categorify would replace each instance A
$\times$ B of matrix multiplication with categorical composition, A $\circ$ B,
and the same for all other terms used to define to the instance. In practice,
when using ViCAR, this serves as a setup tactic. At the beginning of the
proof, categorify is called, which unlocks all the functionality of the
visualizer and automation, provided the relevant structural and coherence
instances have been defined.

#### Foliation

A common representation of a morphism is a foliation [7]. A foliation is a
composition of “stacks,” each of which is the tensor of identity morphisms and
a single non-identity morphism. Such a representation exists for any diagram
and can be considered a standard form and useful for proofs [7]. Formally
proving this result for categorical instances, however, requires the complex
notion that some morphisms are atomic with respect to this decomposition. For
example, in the category of matrices, it is hard to define when a matrix
should be decomposable with respect to matrix multiplication and Kronecker
product (the tensor product). Our tactic foliate computes a foliation of a
given morphism from any monoidal categorical instance, proves they are
equivalent, and replaces the morphism with its foliation. Often, a full
foliation is undesirable, and a more concise form is preferable. The
weak_foliate tactic performs a partial foliation that allows multiple non-
identity morphisms in a stack, but still ensures no stack contains a
composition. An example of weak_foliate and foliate is given in Figure 6 on (f
$\circ$ g) $\otimes$ h. Its partial foliation is f $\otimes$ h $\circ$ g
$\otimes$ id_ M and its full foliation is f $\otimes$ id_ A $\circ$ (id_ B
$\otimes$ h $\circ$ g $\otimes$ id_ M).

(a) Initial state.

(b) Weak foliation.

(c) Foliation.

Figure 6: Visualization of foliation tactics on (f $\circ$ g) $\otimes$ h.

#### Associativity: partnering and rewriting

A recurring task in many Coq projects is dealing with associativity. Coq
expressions have explicit association, so to rewrite a subterm of a sequence
of compositions, it is often necessary to perform several rewrites using
associativity rules. Even the expression g $\circ$ f $\circ$ f^-1 cannot be
rewritten to g directly, requiring first a rewrite using the associativity
condition. In larger expressions, the reassociations which must be performed
can be quite laborious to specify manually. We provide several tactics to
automate this work.

First, we define the partner tactic, which takes two terms as arguments and
attempts to reassociate the goal to make these terms syntactically adjacent.
After calling partner f g, we get (f $\circ$ g) as a subterm of the goal,
assuming it can isolated by reassociation.

Building on this technique, we also define the assoc_rw tactic, which takes a
lemma as an argument and attempts to reassociate the goal such that the lemma
can be rewritten. This works for any lemma whose conclusion, possibly
quantified over arguments, has the form $F\simeq g$, where $F$ is some
sequence of compositions and $g$ is any morphism. This tactic allows a user to
entirely ignore the association of the goal, and simply rewrite according to
the sequence of morphisms present in the goal. For example, given a lemma f
$\circ$ g $\simeq$ h, assoc_rw would rewrite its occurrence in the expression
i $\otimes$ (e $\circ$ f $\circ$ g), even though this requires reassociation
within the argument to the tensor product.

These tactics together entirely obviate the need for manual association of the
goal. This delivers on one part of the motivation for using string diagram
representations of morphisms: such representations implicitly encode the
coherence conditions of monoidal categories by means of topological
irrelevance [20]. While full topological irrelevance is hard both to define
and to prove within Coq, suppressing the consideration of association is a
first step in this direction.

#### Simplifying the goal state

Building on these tactics, we provide a number of tactics to simplify the goal
state. The tactic cancel_isos will cancel any isomorphism adjacent to its
inverse, independent of associativity. This is particularly useful for
eliminating structural morphisms that accumulate by applications of naturality
properties. The tactic cat_simpl combines this cancellation with the removal
of identity morphisms. These tactics give a quick way to perform common
simplifications of a goal without having to consider association. The tactic
cat_easy attempts to solve goals that are fundamentally structural, and not
too complicated. It will cancel isomorphisms and identities, right-associate
the goal, and perform weak foliation until the goal is solvable by
reflexivity.

⬇

Lemma assoc_rw_example {A B M N : Cobj}

(f : A $\sim$> B) (g : M $\sim$> N) :

(Î²_ A, M)^-1 â f â g â Î²_ B, N

â g â f.

Proof.

assoc_rw braiding_natural. (*apply braiding lemma*)

cancel_isos. (*cancellation*)

reflexivity.

Qed.

Listing 2: ViCAR’s tactics being used to easily solve an example lemma.

(a) Initial goal state.

(b) Applying a braiding lemma.

(c) Canceling.

Figure 7: Visualization at each step of LABEL:fig:tactic.

LABEL:fig:tactic and Figure 7 give an example of these tactics in action to
almost completely automate a proof. The assoc_rw tactic automatically
associates the goal to apply the given lemma, a braiding coherence condition.
cancel_isos then reassociates and cancels out the braiding and its inverse.
These tactics can be applied to any proof for a concrete instance, after first
calling categorify.

##  6 Example uses of ViCAR

###  6.1 VyZX

The ZX-calculus is a graphical language to represent quantum operations [6].
Each ZX-diagram represents a linear transformation between qubits and consists
of red and green nodes connected by wires. ZX’s appeal is that its rewrite
rules are easily visualized as graph manipulations. ZX-diagrams can be
visually transformed into any equivalent diagram using a finite set of
rewrites. The ZX-calculus has been used for simulation [15], circuit
optimization [14], and fault tolerance [2] work. For a deeper introduction to
the ZX-calculus, refer to one of these surveys [22, 5].

VyZX (Verifying the ZX-Calculus) is an effort to formalize the ZX-calculus in
Coq [17]. It gives inductive definitions for diagrams and interprets them
through standard matrix semantics for the ZX-calculus. The ZX-calculus
corresponds to a symmetric monoidal category whose objects are natural numbers
(representing the number of input and output wires) and whose morphisms are
ZX-diagrams. Horizontal composition of morphisms (connecting the input and
output wires of two diagrams) is associative. The tensor product is given by
vertically stacking diagrams, corresponding to addition on natural numbers
with identity object $0$. The morphism identity given for a natural number $n$
is $n$ wires with no nodes, since composition with this object does not affect
any diagram.

As VyZX is a well-developed verification library, most of these categorical
structures and necessary lemmas already existed. As a result, the coherence
conditions for these morphisms were straightforward to prove. The braiding was
easily implemented, but proving naturality was a significant task.
Fortunately, this task was made easier by proving naturality of braiding for
matrices, as discussed in 6.3.

The VyZX visualizer, ZXViz, displays ZX-diagrams by parsing an expression into
its building blocks and generating a string diagram. We modified ZXViz to work
for general category instances, abstracting the specific display style used
for ZX-diagrams and significantly reworking the foundation of the visualizer
to work in the context of a general category. Figure 8 gives an example of
ViCAR’s visualizer for a ZX-specific lemma, where zx0 and zx1 are ZX-diagrams.
Its string diagram makes clear this lemma is really just a structural result.

ViCAR grew out of VyZX in an attempt to separate rules specific to the ZX-
calculus from rules which are common to any symmetric monoidal category.
Typical ZX-calculus literature does not reason about such structure but rather
about ZX-diagrams as graphs. Therefore, future VyZX development can benefit
from ViCAR’s automation by being able to better ignore structural manipulation
of ZX-diagrams.

Figure 8: Visualization of the statement (zx0 $\leftrightarrow$ zx1)
$\updownarrow$ n_wire p $\propto$ (zx0 $\updownarrow$ n_wire p)
$\leftrightarrow$ (zx1 $\updownarrow$ n_wire p).

###  6.2 Calculus of Relations

In contrast to the previous implementation, the calculus of relations is not a
pre-existing Coq project. Its implementation follows the book _Picturing
Quantum Processes_ [7]. To adapt this work to Coq, we define the objects of
our category to be types, and we define morphisms between types T and S to
have type T $\rightarrow$ S $\rightarrow$ Prop. As this is defined over any T
and S, it can be easily applied to any specific example. By defining base
relations such as sibling and parent over a type person, we can construct and
visualize relations such as uncle in Figure 9. While relations are a toy
example, they do demonstrate some insights.

Our implementation of relations was made with ViCAR in mind, and so all proofs
are intended for our typeclasses. However, categorical structure is far from a
complete description of the properties of relations. For example, it is
natural to want to describe the transitive closure of a relation R : T
$\rightarrow$ T $\rightarrow$ Prop. There is no clear way to do this solely
using categorical construction. Instead, we are able to use Coq’s built-in
capabilities to describe a very similar construct: given R : T $\rightarrow$ T
$\rightarrow$ Prop, we define R^n, the repeated application of R $n$ times. We
can then construct the transitive closure diagrammatically as $\rho$_ A
$\circ$ (id_ A $\otimes$ any_nat) $\circ$ R^n, where any_nat is a relation
that relates unit to any nat. By having ViCAR embedded in an existing proof
assistant, we gain the ability to easily create new morphisms as needed and
can reason about both structure and properties specific to a particular
instance, together.

Figure 9: Visualizing the “uncle” relation between two people, parent $\circ$
brother. (Note that this is diagrammatic composition; parent precedes
brother.)

###  6.3 Matrices

The collection of vector spaces over a field $k$ form the category
$\textrm{Vect}_{k}$ whose morphisms are linear transformations of spaces. This
is a monoidal category with respect to the tensor product of vector spaces,
with identity element $k$. Moreover, this monoidal category is braided, as
$V\otimes W\cong W\otimes V$.

A commonly-used subcategory of $\textrm{Vect}_{k}$ is the category
$\textrm{FinDimVect}_{k}$ of finite-dimensional vector spaces, which is a
braided monoidal category in exactly the same way. $\textrm{FinDimVect}_{k}$
has a skeleton given by vector spaces of the form $k^{n}$ for
$n\in\mathbb{N}$. This skeleton is isomorphic to the category whose objects
are natural numbers and whose morphisms from $n$ to $m$ are the $n\times m$
matrices over $k$, representing linear transformations $k^{n}\rightarrow
k^{m}$. We implement that category for $k=\mathbb{C}$ based on the matrices in
the QuantumLib library [12], which provides verified mathematics for quantum
computing in Coq. VyZX defines its semantics in terms of QuantumLib matrices.

QuantumLib already implements most of the definitions and lemmas required to
instantiate a category. Matrices in QuantumLib are defined as functions
$\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{C}$. The dimensions of
QuantumLib matrices are not enforced by the type checker, but instead given as
“phantom types” to guide the programmer [19]. This lack of strict dimensions
makes the construction and use of the associator and unitors very
straightforward.

We implement our category instances using bounded equivalence ($\equiv$) as
our morphism equivalence, which says that matrices $A,B$ of dimension $n\times
m$ are equivalent if they are equal on all entries within their bounds. The
majority of the work in showing matrices are a braided monoidal category
involves showing the naturality condition of the braiding. In this category,
the braiding is given by the commutation matrices $K_{n,m}$, which have the
property that for any $n\times m$ matrix $A$ and $p\times q$ matrix $B$, we
have $K_{p,n}(A\otimes B)=(B\otimes A)K_{q,m}$ [18]. Due to phantom types, the
associator and unitor can be defined as the identity matrix interpreted with
the appropriate dimensions. In proofs, these matrices can be immediately
canceled, which makes the coherence conditions easy to prove.

A diagrammatic representation of matrix expressions involving the Kronecker
can reveal facts which textual representations obscure. For instance, Figure
10 shows the distributivity of the Kronecker product over matrix
multiplication. The diagrammatic depiction of this equality highlights the
structure of the vector spaces on which these matrices act, making a non-
obvious equation more believable.

Figure 10: Visualization of the Kronecker mixed-product, $(A\otimes
C)\times(B\otimes D)\equiv(A\times B)\otimes(C\times D)$.

##  7 Future Directions

ViCAR provides a framework for visualization and automated rewriting by
defining typeclasses for categorical and monoidal structure. The language of
string diagrams can further describe rigid symmetric monoidal categories, with
the unit and counit of the category depicted as half turns [20]. ViCAR can be
extended with this structure, allowing it to capture a wide variety of process
theories.

The coherence conditions in our typeclass definitions have been proven
sufficient to show the coherence of the respective categorical structures. If
formalized in Coq, these results could enable much stronger diagrammatic
reasoning by allowing large purely structural rewrites to be performed
immediately, rather than having to manually prove the specific instance of
coherence necessary to perform the replacement.

Many symmetric monoidal categories are interpreted using a semantics function.
In fact, the semantics are often used to define morphism equivalence. We aim
to provide infrastructure within ViCAR to allow translation between different
symmetric monoidal categories for semantic interpretation. This would greatly
simplify constructs in categories equipped with a ViCAR-based semantics by
lifting them.

Seeing the advantage that the assoc_rw tactic gives us, we want to further
expand the capabilities of rewriting structure. In fact, we would like to
completely be able to rewrite without worrying about structure. To achieve
this goal, we are working on an e-graph equality saturation-based solver for
different structural configurations. The solver will work by ingesting Coq
statements into a custom AST and then the e-graph solver will use the
structural rewrite rules in ViCAR. Once a proof is found, it will be exported
into Coq and checked.

## References

  * [1]
  * [2] Hector Bombin, Daniel Litinski, Naomi Nickerson, Fernando Pastawski & Sam Roberts (2023): _Unifying flavors of fault tolerance with the ZX calculus_.  arXiv:2303.08829.
  * [3] Thomas Braibant & Damien Pous (2011): _Tactics for reasoning modulo AC in Coq_.  In: International Conference on Certified Programs and Proofs, Springer, pp. 167–182.
  * [4] Jonathan Castello, Patrick Redmond & Lindsey Kuper (2023): _Inductive diagrams for causal reasoning_.  arXiv:2307.10484.
  * [5] Bob Coecke (2023): _Basic ZX-calculus for students and professionals_.  arXiv:2303.03163.
  * [6] Bob Coecke & Ross Duncan (2008): _Interacting Quantum Observables_.  In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir & Igor Walukiewicz, editors: Automata, Languages and Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 298–310, 10.1007/978-3-540-70583-3_25.
  * [7] Bob Coecke & Aleks Kissinger (2017): _Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning_.  Cambridge University Press, 10.1017/9781316219317.
  * [8] The Coq Development Team (2012): _The Coq Reference Manual, version 8.4_.  Available electronically at http://coq.inria.fr/doc.
  * [9] The Coq LSP Developers (2023): _GitHub - ejgallego/coq-lsp: Visual Studio Code Extension and Language Server Protocol for Coq — github.com_.  https://github.com/ejgallego/coq-lsp.
  * [10] Samuel Eilenberg & G Max Kelly (1966): _Closed categories_.  In: Proceedings of the Conference on Categorical Algebra: La Jolla 1965, Springer, pp. 421–562.
  * [11] Jason Gross, Adam Chlipala & David I Spivak (2014): _Experience implementing a performant category-theory library in Coq_.  In: Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings 5, Springer, pp. 275–291.
  * [12] INQWIRE Developers (2022): _INQWIRE QuantumLib_.  Available at https://github.com/inQWIRE/QuantumLib.
  * [13] John Wiegley (2022): _Category Theory in Coq_.  Available at https://github.com/jwiegley/category-theory.
  * [14] Aleks Kissinger & John van de Wetering (2020): _PyZX: Large Scale Automated Diagrammatic Reasoning_.  In Bob Coecke & Matthew Leifer, editors: Proceedings 16th International Conference on Quantum Physics and Logic, Chapman University, Orange, CA, USA., 10-14 June 2019, Electronic Proceedings in Theoretical Computer Science 318, Open Publishing Association, pp. 229–241, 10.4204/EPTCS.318.14.
  * [15] Aleks Kissinger & John van de Wetering (2022): _Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions_.  Quantum Science and Technology 7(4), p. 044001.
  * [16] Alex Kissinger (2023): _GitHub - akissinger/chyp: An interactive theorem prover for string diagrams — github.com_.  https://github.com/akissinger/chyp.
  * [17] Adrian Lehmann, Ben Caldwell, Bhakti Shah & Robert Rand (2023): _VyZX: Formal Verification of a Graphical Quantum Language_.  arXiv:2311.11571.
  * [18] Jan R. Magnus & H. Neudecker (1979): _The Commutation Matrix: Some Properties and Applications_.  The Annals of Statistics 7(2), pp. 381–394.  Available at http://www.jstor.org/stable/2958818.
  * [19] Robert Rand, Jennifer Paykin & Steve Zdancewic (2018): _Phantom Types for Quantum Programs_.  Available at https://popl18.sigplan.org/event/coqpl-2018-phantom-types-for-quantum-programs.  Talk at The Fourth International Workshop on Coq for Programming Languages (CoqPL ’18).
  * [20] P. Selinger (2010): _A Survey of Graphical Languages for Monoidal Categories_.  In: New Structures for Physics, Springer Berlin Heidelberg, pp. 289–355, 10.1007/978-3-642-12821-9_4.
  * [21] Matthieu Sozeau & Nicolas Oury (2008): _First-Class Type Classes_.  In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’08, Springer-Verlag, Berlin, Heidelberg, p. 278–293, 10.1007/978-3-540-71067-7_23.  Available at https://doi.org/10.1007/978-3-540-71067-7_23.
  * [22] John van de Wetering (2020): _ZX-calculus for the working quantum computer scientist_.  arXiv:2012.13966.


# Polyp-SAM++: Can A Text Guided SAM Perform Better for Polyp Segmentation?

Risab Biswas R. Biswas is with Optiks Innovations Pvt. Ltd (P360), Mumbai,
Maharashtra 400066, India. (e-mail: risab.biswas@p360.com).

###### Abstract

Meta recently released SAM (Segment Anything Model) which is a general-purpose
segmentation model. SAM has shown promising results in a wide variety of
segmentation tasks including medical image segmentation. In the field of
medical image segmentation, polyp segmentation holds a position of high
importance, thus creating a model which is robust and precise is quite
challenging. Polyp segmentation is a fundamental task to ensure better
diagnosis and cure of colorectal cancer. As such in this study, we will see
how Polyp-SAM++, a text prompt-aided SAM, can better utilize a SAM using text
prompting for robust and more precise polyp segmentation. We will evaluate the
performance of a text-guided SAM on the polyp segmentation task on benchmark
datasets. We will also compare the results of text-guided SAM vs unprompted
SAM. With this study, we hope to advance the field of polyp segmentation and
inspire more, intriguing research. The code and other details will be made
publically available soon at https://github.com/RisabBiswas/Polyp-SAM++.

###### Index Terms:

Medical Image Segmentation, Polyp Segmentation, Segment Anything Model

##  1 Introduction

Transformer-based vision models like ViT [1] have been in the field for quite
some time now and have performed well in tasks like medical image
segmentation, image enhancement, object detection, classification, etc. In
recent years, large language models like Chatgpt [2] and GPT-4 [3] like models
have gained quite popularity. This is mostly due to the fact that they are
general-purpose and can be adapted easily for a wide variety of tasks. This is
mostly due to the fact that they are trained on a large amount of data. LLMs
provide the advantage of cross-modal learning and utilizing extensive data but
may not be optimally used for image segmentation tasks. For such tasks, CNN
and ViT-based models are still a preferred choice by researchers. Meta
released the Segment Anything Model (SAM) [4], a universal segmentation model
that utilizes the capabilities of ”prompting” for image segmentation. SAM is
trained on the Segment Anything 1-Billion mask dataset (SA-1B), which is also
publically released by Meta. Prompts could be points on the image, a bounding
box, text, or, more generally, any information suggesting what to segment in
an image. SAM’s main goal is to decrease the demand for task-specific modeling
knowledge, training computing power, and customized data annotation for image
segmentation problems. So far, SAM has gained promising results in
segmentation tasks and more and more application areas are having
implementation and experimental analysis of SAM. Tao et al. [5] proposed a
SAM-based image inpainting model, for removing/replacing/filling any object in
an input image. SAM incorporated with stable diffusion also opened doors for
more interesting projects with applications in image inpainting. SAMCOD [6],
proposed by Tang et al. evaluated the performance of SAM for the Camouflaged
object detection (COD) task. Works proposed by Yao et al. [7] and Li et al.
[8] are more focused on using SAM for image matting tasks.

SAM has also found promising applications in the field of medical image
segmentation. For example, Deng et al. [9] proposed a detailed assessment of
SAM on the zero-shot digital pathological segmentation task. Ma et al.were
among the ones to propose the foundational models of using SAM for a universal
medical image segmentation model, called MedSAM [10]. They utilized various
prompting to generate their results. MedSAM opened doors for further
investigation of SAM’s ability to perform well in more specific segmentation
tasks.

##  2 Related Works Based on SAM

Specifically for polyp segmentation, works done by Zhou et al. [11] and Chen
et al. [12] present promising results using an unprompted SAM and a domain-
adapted SAM respectively. Additionally, Polyp-SAM [13] used SAM for the same
task. Roy et al. [14] evaluated the zero-shot capabilities of SAM on the organ
segmentation task. Inspired by these works on medical imaging, we performed an
experiment to see how well a text-guided SAM (Polyp-SAM++) can segment polyps
in colonoscopy images under various difficult circumstances. Particularly we
provided a definition of a polyp with details about shape, color, position,
etc. Our approach is very simple and robust. This report mainly evaluates the
effectiveness of a text-guided SAM in segmenting polyps. Since Meta has not
officially released the text prompting capabilities in SAM, we utilized
Language Segment-Anything, which uses grounded-DINO to generate the bounding
box based on the text prompt, which is eventually fed to the SAM for final
segmentation mask generation. Fig. 1, illustrates graphically how the Polyp-
SAM++ model works.

##  3 Experiments and Results

In this report, we compared the outcomes of Polyp-SAM++ both quantitatively
and qualitatively, with other state-of-the-art models on the polyp
segmentation task as well as with previous outcomes when using SAM for polyp
segmentation. In this section, we will discuss briefly the evaluation metrics,
datasets, methods used for comparison, and implementation details of Polyp-
SAM++.

Figure 1: Overview of the Polyp-SAM++ Architecture

###  3.1 Datasets

To evaluate the outcomes of Polyp-SAM++, we performed both qualitative and
quantitative experiments on four benchmark colonoscopy datasets:

  * •

Kvasir-SEG [15]: This dataset contains 1000 pairs of images from inside the
gastrointestinal tract, during colonoscopy of patients, where the polyp is
present along with the ground truth segmentation mask. The dataset has images
with varied resolutions. The dataset is collected by Vestre Viken Health
Trust, Norway.

  * •

CVC-300 [16]: This dataset contains 60 images containing polyp. The dataset
contains images with a resolution of $500\times 574$.

  * •

CVC-ClinicDB [17]: This dataset contains 612 images collected from various
colonoscopy videos with a resolution of $288\times 384$.

###  3.2 Evaluation Metrics

In our experiment, we used the three most commonly used metrics for image
segmentation to evaluate the effectiveness of Polyp-SAM++ and other methods.
We used the Mean dice score($\rm mDice$), Mean intersection over union ($\rm
mIoU$), and F-measure ($\rm Fm$) [18].

###  3.3 Implementation Details

We begin our evaluation by handcrafting a text prompt that acts as a guide to
the segment anything model. In our experiment for polyp segmentation, we are
only concerned about generating the segmentation map of the polyp in the
colonoscopy images. As discussed in the earlier sections, SAM is capable of
handling a variety of prompts for generating specific segmentation maps in an
image. One of them is by utilizing a bounding box around the objects of
concern. Based on this idea, we are using our text-guided evaluation. The text
prompt is crafted in a way that it defines a polyp which acts as a guide to
the segmentation model. The text prompt creates a bounding box using
GroundingDINO [19] which is a zero-shot approach. Fig. 2 illustrates the
resultant bounding boxes. These bounding box helps the SAM model to generate a
precise segmentation map of the object within the bounding box. During our
evaluation, we noticed that when using SAM with text prompts, there were
occurrences where it generated multiple bounding boxes in an image, resulting
in more than one segmentation mask. In such situations, we devised a strategy
to select the best mask based on the corresponding ground truth. Since we are
not changing the text prompt at all throughout our experiment, it makes the
overall evaluation more faster and robust. Though, we agree that in some cases
where Polyp-SAM++ did not generate good results or completely failed to
produce a segmentation mask, input prompt engineering might overcome the
shortcomings. We will provide some good examples of the failed scenarios as
well in the later sections.

Example Text Prompt = ”A polyp is an anomalous oval-shaped small bump-like
structure, a relatively small growth or mass that develops on the inner lining
of the colon or other organs. Multiple polyps may exist in one image.”

TABLE I: Quantitative Evaluation on the Benchmark Datasets for Polyp
Segmentation.

Methods | CVC-ClinicDB [17] | Kvasir-SEG [15] | CVC-300 [16]
---|---|---|---
$\rm mDice$$\uparrow$ |  $\rm mIoU$$\uparrow$ |  $\rm Fm$$\uparrow$ |  $\rm mDice$$\uparrow$ |  $\rm mIoU$$\uparrow$ |  $\rm Fm$$\uparrow$ |  $\rm mDice$$\uparrow$ |  $\rm mIoU$$\uparrow$ |  $\rm Fm$$\uparrow$
UNet [20] | 0.82 | 0.75 | 0.81 | 0.81 | 0.746 | 0.79 | 0.71 | 0.62 | 0.68
UNet++ [21] | 0.79 | 0.72 | 0.78 | 0.82 | 0.74 | 0.80 | 0.70 | 0.62 | 0.68
SFA [22] | 0.70 | 0.60 | 0.64 | 0.72 | 0.61 | 0.67 | 0.46 | 0.32 | 0.34
PraNet [23] | 0.89 | 0.84 | 0.89 | 0.89 | 0.84 | 0.88 | 0.87 | 0.79 | 0.84
ACSNet [24] | 0.88 | 0.82 | 0.87 | 0.89 | 0.83 | 0.88 | 0.86 | 0.78 | 0.82
MSEG [25] | 0.90 | 0.86 | 0.90 | 0.89 | 0.83 | 0.88 | 0.87 | 0.80 | 0.85
DCRNet [26] | 0.89 | 0.84 | 0.89 | 0.88 | 0.82 | 0.86 | 0.85 | 0.78 | 0.83
EU-Net [27] | 0.90 | 0.84 | 0.89 | 0.90 | 0.85 | 0.89 | 0.83 | 0.76 | 0.80
SANet [28] | 0.91 | 0.85 | 0.90 | 0.90 | 0.84 | 0.89 | 0.88 | 0.81 | 0.80
MSNet [29] | 0.91 | 0.86 | 0.91 | 0.90 | 0.84 | 0.89 | 0.86 | 0.79 | 0.84
C2FNet [30] | 0.91 | 0.87 | 0.90 | 0.88 | 0.83 | 0.87 | 0.87 | 0.80 | 0.92
LDNet [31] | 0.88 | 0.82 | 0.87 | 0.88 | 0.82 | 0.86 | 0.86 | 0.79 | 0.84
FAPNet [32] | 0.92 | 0.87 | 0.91 | 0.90 | 0.84 | 0.89 | 0.89 | 0.82 | 0.87
CFA-Net [33] | 0.93 | 0.88 | 0.92 | 0.91 | 0.86 | 0.90 | 0.89 | 0.82 | 0.87
Polyp-PVT [34] | 0.94 | 0.90 | 0.95 | 0.91 | 0.86 | 0.91 | 0.90 | 0.93 | 0.88
HSNet [35] | 0.93 | 0.88 | 0.93 | 0.92 | 0.87 | 0.91 | 0.90 | 0.83 | 0.88
Polyp-SAM [13] | 0.92 | 0.87 | - | 0.90 | 0.86 | - | 0.92 | 0.88 | -
SAM-H [11] | 0.54 | 0.50 | 0.54 | 0.77 | 0.70 | 0.76 | 0.65 | 0.60 | 0.65
SAM-L [11] | 0.57 | 0.52 | 0.56 | 0.78 | 0.71 | 0.77 | 0.72 | 0.67 | 0.72
Polyp-SAM++ | 0.91 | 0.86 | 0.91 | 0.90 | 0.86 | 0.92 | 0.73 | 0.69 | 0.73

|  |  |  |
---|---|---|---|---
Figure 2: Bounding Box created based on the Text-Prompt by GroundingDINO.
Figure 3: Qualitative Assessment of Segmentation Outcomes on Kvasir-SEG,
CVC-300 and CVC-ClinicDB Datasets using Polyp-SAM++. Figure 4: Qualitative
Analysis on the Segmentation Outcomes and Comparison using Polyp-SAM++.

|  |  |
---|---|---|---
|  |  |
|  |  |

Figure 5: Cases where Polyp-SAM++ failed on generating accurate segmentation
masks.

For the quantitative evaluation, we have randomly chosen 100 images from the
Kvasir-SEG dataset, and 60 random images from the CVC-ClinicDB. For
evaluation, all the images from CVC-300 are used.

###  3.4 Methods for Comparison

For our study, we compared the results produced by Polyp-SAM++ and compared
them with the outcomes of various CNN, ViT, and even other recent SAM-based
techniques for polyp segmentation. The CNN based models include - UNet [20],
UNet++ [21], SFA [22], PraNet [23], ACSNet [24], MSEG [25], DCRNet [26], EU-
Net [27], SANet [28], MSNet [29], and CFA-Net [33] . For the Transformer based
models, we assessed Polyp-PVT [34] and HSNet [35]. And finally, we assessed
the work done by Tao et al. [11] and Polyp-SAM [13], where they evaluated the
performance of SAM for polyp segmentation.

###  3.5 Quantitative Results and Comparison

In this section, we will look into how Polyp-SAM++ performs in polyp
segmentation tasks from a quantitative evaluation perspective. We compared the
outcomes with the methods mentioned in 3.4 on the three datasets mentioned in
the 3.1 based on the metrics discussed in 3.2. The results of the model and a
comparative analysis are presented in Table LABEL:Tab:Table1. The best results
are highlighted in bold and the second best is underlined. The Polyp-SAM model
which is a SAM-based architecture fine-tuned specifically for polyp
segmentation and SAM-H/SAM-L are also compared with the Polyp-SAM++ results.
We can evidently see that using simple text guidance to generate the bounding
box helped improve the SAM model to better understand what to segment, which
improved the overall segmentation performance. The text guidance is helping in
the localization while the SAM is performing the segmentation. Based on the
analysis we can understand that the shortcoming of using a model like SAM is
on the localization objective because once the localization is achieved, SAM
is effectively able to segment that. The text guidance is not only helping in
the localization of a polyp in the input image but also aids in generating a
better segmentation map.

###  3.6 Qualitative Results and Comparison

In this section, we will look into how Polyp-SAM++ performs in polyp
segmentation tasks from a qualitative evaluation perspective. The Fig. 4 shows
the results of the text-guided SAM on polyp segmentation on the three chosen
benchmark datasets. We can see how the model effectively understands the text
prompt and segments the region of interest. The Polyp-SAM++ performs
segmentation well in diverse settings without making changes in the prompt,
this shows the robustness of the GroundingDINO and the SAM methods. Next we
compared the outcomes with the results of the other state-of-the art methods
mentioned in 3.4. Based on the outcomes illustrated in Fig. 3, it is evident
that the text guidance is helping the segmentation model overcome the
challenges faced by the SAM outcomes without any prompting about the object of
interest. And overall the model is quite competitive to the current polyp
segmentation models. However, even with the text guidance SAM fails to segment
the polyps in certain cases. A few examples are shown in Fig. 5. We will
discuss how can we overcome this challenge in the next section 4.

##  4 Future Work

Even though Polyp-SAM++ has shown impressive performance as a strong
competitor in the field of cutting-edge models for polyp segmentation, there
are still exciting opportunities to make it even better. In this part, we’ll
explore potential ways to enhance and fine-tune the Polyp-SAM++ model for even
more remarkable results.

  * •

Evaluation on Other Datasets: It is essential to subject Polyp-SAM++ to
evaluation using the CVC-ColonDB [36] and ETIS [37] datasets, both of which
serve as benchmark datasets in this domain. This evaluation process will
provide crucial insights into the model’s performance and its ability to
handle these established and recognized datasets effectively.

  * •

Zero-shot Bounding Box Generator Enhancement: A significant opportunity for
enhancement involves improving the zero-shot bounding box generator within
Polyp-SAM++. By refining this component using a broader collection of
annotated polyp images, the model’s skill in generating precise bounding boxes
within colonoscopic images can be substantially improved. This advancement
would establish a more resilient initial localization of potential polyps,
subsequently resulting in heightened accuracy during the subsequent
segmentation process.

  * •

Fine-Tuning SAM: Similar to the approach adopted for the original Polyp-SAM
model, the Polyp-SAM++ model can benefit from fine-tuning its underlying SAM
model. This process involves training the model on a specialized dataset of
annotated polyps to better adapt its capabilities to the unique
characteristics of polyp segmentation tasks. This fine-tuning can enable the
model to capture the nuances of polyp appearances and further enhance its
segmentation accuracy.

  * •

Prompt Engineering for Human-Like Supervision: Exploring prompt engineering
offers an intriguing way for refining the Polyp-SAM++ model. By crafting
specialized prompts for different datasets or scenarios, the model’s
performance can be guided more effectively. This approach essentially
introduces a form of human-like supervision to guide the model’s decision-
making, potentially improving its understanding of polyp-specific features and
characteristics.

  * •

Performance Evaluation with Meta’s Text Prompts: Once Meta officially releases
their text prompting capability in SAM, an evaluation of the Polyp-SAM++
model’s performance using these prompts can provide insights into the model’s
adaptability and versatility. This assessment can guide further refinements
and adaptations to leverage the benefits of the Meta text prompts for polyp
segmentation.

##  5 Conclusion

This report provides an investigation of the performance of SAM using a text-
guided input prompt for the polyp segmentation task. We tested Polyp-SAM++ on
three standard polyp-segmentation datasets, and the outcomes presented a
quantitative and qualitative evaluation and comparison respectively. Based on
the results and our analysis, we see by taking a simple approach of
incorporating text prompts to SAM can increase the overall performance
significantly. We discussed that a general-purpose model like SAM can still be
used for a specific task like polyp segmentation by providing SAM the relevant
context, in this case, a bounding box to find the region of interest as the
localization step in the overall task. We also show quantitatively and
qualitatively how the text guidance improves upon the SAM without any
prompting for polyp segmentation. We discussed the failed cases as well as the
model and eventually discussed how we can further improve the model. We are
hoping this paper will encourage more curiosity in the subject of polyp
segmentation and that further research will be carried out using SAM to make
progress in this field of study.

##  6 Acknowledgment

The author would like to extend a heartfelt appreciation to Luca Medeiros, the
author and creator of the repository ”lang-segment-anything” available at
https://github.com/luca-medeiros/lang-segment-anything. The remarkable work
done by the author has been instrumental in making our project possible and
has greatly contributed to its success.

## References

  * [1] A. Dosovitskiy, L. Beyer, A. Kolesnikov, D. Weissenborn, X. Zhai, T. Unterthiner, M. Dehghani, M. Minderer, G. Heigold, S. Gelly, J. Uszkoreit, and N. Houlsby, “An image is worth 16x16 words: Transformers for image recognition at scale,” _CoRR_ , vol. abs/2010.11929, 2020. [Online]. Available: https://arxiv.org/abs/2010.11929
  * [2] T. Brown, B. Mann, N. Ryder, M. Subbiah, J. D. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herbert-Voss, G. Krueger, T. Henighan, R. Child, A. Ramesh, D. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner, S. McCandlish, A. Radford, I. Sutskever, and D. Amodei, “Language models are few-shot learners,” in _Advances in Neural Information Processing Systems_ , H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, Eds., vol. 33. Curran Associates, Inc., 2020, pp. 1877–1901. [Online]. Available: https://proceedings.neurips.cc/paper_files/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf
  * [3] OpenAI, “Gpt-4 technical report,” _ArXiv_ , vol. abs/2303.08774, 2023. [Online]. Available: https://api.semanticscholar.org/CorpusID:257532815
  * [4] A. Kirillov, E. Mintun, N. Ravi, H. Mao, C. Rolland, L. Gustafson, T. Xiao, S. Whitehead, A. C. Berg, W.-Y. Lo, P. Dollár, and R. Girshick, “Segment anything,” 2023.
  * [5] T. Yu, R. Feng, R. Feng, J. Liu, X. Jin, W. Zeng, and Z. Chen, “Inpaint anything: Segment anything meets image inpainting,” 2023.
  * [6] L. Tang, H. Xiao, and B. Li, “Can sam segment anything? when sam meets camouflaged object detection,” 2023.
  * [7] J. Yao, X. Wang, L. Ye, and W. Liu, “Matte anything: Interactive natural image matting with segment anything models,” 2023.
  * [8] J. Li, J. Jain, and H. Shi, “Matting anything,” 2023.
  * [9] R. Deng, C. Cui, Q. Liu, T. Yao, L. W. Remedios, S. Bao, B. A. Landman, L. E. Wheless, L. A. Coburn, K. T. Wilson, Y. Wang, S. Zhao, A. B. Fogo, H. Yang, Y. Tang, and Y. Huo, “Segment anything model (sam) for digital pathology: Assess zero-shot segmentation on whole slide imaging,” 2023.
  * [10] J. Ma, Y. He, F. Li, L. Han, C. You, and B. Wang, “Segment anything in medical images,” 2023.
  * [11] T. Zhou, Y. Zhang, Y. Zhou, Y. Wu, and C. Gong, “Can sam segment polyps?” 2023\.
  * [12] T. Chen, L. Zhu, C. Ding, R. Cao, Y. Wang, Z. Li, L. Sun, P. Mao, and Y. Zang, “Sam fails to segment anything? – sam-adapter: Adapting sam in underperformed scenes: Camouflage, shadow, medical image segmentation, and more,” 2023.
  * [13] Y. Li, M. Hu, and X. Yang, “Polyp-sam: Transfer sam for polyp segmentation,” 2023\.
  * [14] S. Roy, T. Wald, G. Koehler, M. R. Rokuss, N. Disch, J. Holzschuh, D. Zimmerer, and K. H. Maier-Hein, “Sam.md: Zero-shot medical image segmentation capabilities of the segment anything model,” 2023.
  * [15] D. Jha, P. H. Smedsrud, M. A. Riegler, P. Halvorsen, T. de Lange, D. Johansen, and H. D. Johansen, “Kvasir-seg: A segmented polyp dataset,” in _International Conference on Multimedia Modeling_. Springer, 2020, pp. 451–462.
  * [16] D. Vázquez, J. Bernal, F. J. Sánchez, G. Fernández-Esparrach, A. M. López, A. Romero, M. Drozdzal, and A. Courville, “A benchmark for endoluminal scene segmentation of colonoscopy images,” _Journal of Healthcare Engineering_ , pp. 1–9, 2017.
  * [17] J. Bernal, F. J. Sánchez, G. Fernández-Esparrach, D. Gil, C. Rodríguez, and F. Vilariño, “Wm-dova maps for accurate polyp highlighting in colonoscopy: Validation vs. saliency maps from physicians,” _Computerized Medical Imaging and Graphics_ , vol. 43, pp. 99–111, 2015.
  * [18] R. Achanta, S. Hemami, F. Estrada, and S. Susstrunk, “Frequency-tuned salient region detection,” in _2009 IEEE Conference on Computer Vision and Pattern Recognition_ , 2009, pp. 1597–1604.
  * [19] S. Liu, Z. Zeng, T. Ren, F. Li, H. Zhang, J. Yang, C. Li, J. Yang, H. Su, J. Zhu, and L. Zhang, “Grounding dino: Marrying dino with grounded pre-training for open-set object detection,” 2023.
  * [20] O. Ronneberger, P. Fischer, and T. Brox, “U-net: Convolutional networks for biomedical image segmentation,” 2015.
  * [21] Z. Zhou, M. M. R. Siddiquee, N. Tajbakhsh, and J. Liang, “Unet++: A nested u-net architecture for medical image segmentation,” 2018.
  * [22] Y. Fang, C. Chen, Y. Yuan, and K.-y. Tong, “Selective feature aggregation network with area-boundary constraints for polyp segmentation,” in _Medical Image Computing and Computer Assisted Intervention – MICCAI 2019: 22nd International Conference, Shenzhen, China, October 13–17, 2019, Proceedings, Part I_. Berlin, Heidelberg: Springer-Verlag, 2019, p. 302–310. [Online]. Available: https://doi.org/10.1007/978-3-030-32239-7_34
  * [23] D.-P. Fan, G.-P. Ji, T. Zhou, G. Chen, H. Fu, J. Shen, and L. Shao, “Pranet: Parallel reverse attention network for polyp segmentation,” 2020.
  * [24] R. Zhang, G. Li, Z. Li, S. Cui, D. Qian, and Y. Yu, “Adaptive context selection for polyp segmentation,” 2023.
  * [25] C.-H. Huang, H.-Y. Wu, and Y.-L. Lin, “Hardnet-mseg: A simple encoder-decoder polyp segmentation neural network that achieves over 0.9 mean dice and 86 fps,” 2021.
  * [26] Z. Yin, K. Liang, Z. Ma, and J. Guo, “Duplex contextual relation network for polyp segmentation,” 2022.
  * [27] K. Patel, A. M. Bur, and G. Wang, “Enhanced u-net: A feature enhancement network for polyp segmentation,” 2021.
  * [28] J. Wei, Y. Hu, R. Zhang, Z. Li, S. K. Zhou, and S. Cui, “Shallow attention network for polyp segmentation,” 2021.
  * [29] X. Zhao, L. Zhang, and H. Lu, “Automatic polyp segmentation via multi-scale subtraction network,” in _International Conference on Medical Image Computing and Computer-Assisted Intervention_ , 2021. [Online]. Available: https://api.semanticscholar.org/CorpusID:236976302
  * [30] Y. Sun, G. Chen, T. Zhou, Y. Zhang, and N. Liu, “Context-aware cross-level fusion network for camouflaged object detection,” 2021.
  * [31] R. Zhang, P. Lai, X. Wan, D.-J. Fan, F. Gao, X.-J. Wu, and G. Li, “Lesion-aware dynamic kernel for polyp segmentation,” 2023.
  * [32] T. Zhou, Y. Zhou, C. Gong, J. Yang, and Y. Zhang, “Feature aggregation and propagation network for camouflaged object detection,” _IEEE Transactions on Image Processing_ , vol. 31, pp. 7036–7047, 2022. [Online]. Available: https://doi.org/10.1109%2Ftip.2022.3217695
  * [33] T. Zhou, Y. Zhou, K. He, C. Gong, J. Yang, H. Fu, and D. Shen, “Cross-level feature aggregation network for polyp segmentation,” _Pattern Recognition_ , vol. 140, p. 109555, 2023. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0031320323002558
  * [34] B. Dong, W. Wang, D.-P. Fan, J. Li, H. Fu, and L. Shao, “Polyp-pvt: Polyp segmentation with pyramid vision transformers,” 2023.
  * [35] W. Zhang, C. Fu, Y. Zheng, F. Zhang, Y. Zhao, and C.-W. Sham, “Hsnet: A hybrid semantic network for polyp segmentation,” _Computers in Biology and Medicine_ , vol. 150, p. 106173, 2022. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0010482522008812
  * [36] N. Tajbakhsh, S. R. Gurudu, and J. Liang, “Automated polyp detection in colonoscopy videos using shape and context information,” _IEEE Transactions on Medical Imaging_ , vol. 35, no. 2, pp. 630–644, 2015.
  * [37] J. Silva, A. Histace, O. Romain, X. Dray, and B. Granado, “Toward embedded detection of polyps in wce images for early diagnosis of colorectal cancer,” _International Journal of Computer Assisted Radiology and Surgery_ , vol. 9, no. 2, pp. 283–293, 2014.