Deep Embedding v.s Shallow Embedding]Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding

[1]Zhongye<EMAIL_ADDRESS>1]Qinxiang<EMAIL_ADDRESS>1]Yichen<EMAIL_ADDRESS>
[1]Shanghai Jiao Tong University, Shanghai, China

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic.
Their program logics, their assertion languages, and their underlying programming languages can be formalized by either a shallow embedding or a deep embedding.
Tools like Iris and early versions of Verified Software Toolchain (VST) choose different shallow embeddings to formalize their program logics.
But the pros and cons of these different embeddings were not yet well studied.
Therefore, we want to study the impact of the program logic's embedding on logic's proof rules in this paper.

This paper considers a set of useful extended proof rules, and four different logic embeddings: one deep embedding and three common shallow embeddings.
We prove the validity of these extended rules under these embeddings and discuss their main challenges.
Furthermore, we propose a method to lift existing shallowly embedded logics to deeply embedded ones to greatly simplify proofs of extended rules in specific proof systems.
We evaluate our results on two existing verification tools.
We lift the originally shallowly embedded VST to our deeply embedded VST to support extended rules, and we implement Iris-CF and deeply embedded Iris-Imp based on the Iris framework to evaluate our theory in real verification projects.

§ STATEMENTS AND DECLARATIONS

§.§ Funding

This research is sponsored by National Natural Science Foundation of China (NSFC) Grant No. 61902240.

§.§ Competing interests

* The authors have no relevant financial or non-financial interests other than those declared in the Funding section.

* The authors have no competing interests to declare that are relevant to the content of this article.

#1ISBN #1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1<https://doi.org/#1>et al.#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1<><#>1#1#1#1#1#1#1#1#1#1#1#1#1#1PreBibitemsHook

[1]

Barras, B.,
Boutin, S.,
Cornes, C.,
Courant, J.,
Coscoy, Y.,
Delahaye, D.,
de Rauglaudre, D.,
Filliâtre, J.-C.,
Giménez, E.,
Herbelin, H., et al.:
The coq proof assistant reference manual.
INRIA, version

[2]

Nipkow, T.,
Wenzel, M.,
Paulson, L.C.:
Isabelle/HOL: a Proof Assistant for Higher-order Logic.
Berlin Heidelberg

[3]

Paulson, L.C.:
Isabelle: A Generic Theorem Prover.
Berlin Heidelberg

[4]

Appel, A.W.:
Verified software toolchain.
In: Proceedings of the 20th European Conference on Programming
Languages and Systems: Part of the Joint European Conferences on Theory and
Practice of Software,
pp. 1–17

[5]

Cao, Q.,
Beringer, L.,
Gruetter, S.,
Dodds, J.,
Appel, A.W.:
Vst-floyd: A separation logic tool to verify correctness of c
Journal of Automated Reasoning

[6]

Jung, R.,
Krebbers, R.,
Jourdan, J.-H.,
Bizjak, A.,
Birkedal, L.,
Dreyer, D.:
Iris from the ground up: A modular foundation for higher-order
concurrent separation logic.
Journal of Functional Programming

[7]

Sanán, D.,
Zhao, Y.,
Hou, Z.,
Zhang, F.,
Tiu, A.,
Liu, Y.:
Csimpl: A rely-guarantee-based framework for verifying concurrent
In: Tools and Algorithms for the Construction and Analysis of Systems:
23rd International Conference, TACAS 2017, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden,
April 22-29, 2017, Proceedings, Part I 23,
pp. 481–498

[8]

Guéneau, A.,
Myreen, M.O.,
Kumar, R.,
Norrish, M.:
Verified characteristic formulae for cakeml.
In: Programming Languages and Systems: 26th European Symposium on
Programming, ESOP 2017, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29,
2017, Proceedings 26,
pp. 584–610

[9]

Cook, S.A.:
Soundness and completeness of an axiom system for program
SIAM Journal on Computing

[10]

Wang, Z.,
Tao, Y.,
Cao, Q.:
Coq Formalization of Verifying Programs with Logic and Extended Proof Rules:
Deep Embed V.s. Shallow Embed.

[11]

Sergey, I.,
Nanevski, A.,
Banerjee, A.:
Mechanized verification of fine-grained concurrent programs.
In: Proceedings of the 36th ACM SIGPLAN Conference on Programming
Language Design and Implementation,
pp. 77–87

[12]

Pierce, B.C.,
Casinghino, C.,
Gaboardi, M.,
Greenberg, M.,
Hriţcu, C.,
Sjöberg, V.,
Yorgey, B.:
Software foundations.

[13]

Schirmer, N.:
Verification of sequential imperative programs in isabelle/hol.
PhD thesis,
Technische Universität München

[14]

Yu, D.,
Hamid, N.A.,
Shao, Z.:
Building certified libraries for pcc: Dynamic storage allocation.
In: Programming Languages and Systems: 12th European Symposium on
Programming, ESOP 2003 Held as Part of the Joint European Conferences on
Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003
pp. 363–379

[15]

Ni, Z.,
Shao, Z.:
Certified assembly programming with embedded code pointers.
In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages,
pp. 320–333

[16]

Xu, F.,
Fu, M.,
Feng, X.,
Zhang, X.,
Zhang, H.,
Li, Z.:
A practical verification framework for preemptive os kernels.
In: International Conference on Computer Aided Verification,
pp. 59–79

[17]

Brookes, S.:
A semantics for concurrent separation logic.
Theoretical Computer Science

[18]

Bulwahn, L.,
Krauss, A.,
Haftmann, F.,
Erkök, L.,
Matthews, J.:
Imperative functional programming with isabelle/hol.
In: International Conference on Theorem Proving in Higher Order
pp. 134–149

[19]

Lammich, P.,
Meis, R.:
A separation logic framework for imperative hol.
Archive of Formal Proofs,

[20]

Zhan, B.:
Verifying imperative programs using auto2.
Archive of Formal Proofs

[21]

Zhan, B.:
Auto2, a saturation-based heuristic prover for higher-order logic.
In: International Conference on Interactive Theorem Proving,
pp. 441–456

[22]

Nipkow, T.:
Hoare logics in isabelle/hol.
Proof and system-reliability,

[23]

Lammich, P.,
Nipkow, T.:
Purely functional, simple, and efficient implementation of prim and dijkstra.
Archive of Formal Proofs

[24]

Tarski, A.:
A lattice-theoretical fixpoint theorem and its applications.

[25]

Witt, E.:
Beweisstudien zum satz von m. zorn. herrn erhard. schmidt zum 75.
geburtstag gewidmet.
Mathematische Nachrichten

[26]

Bourbaki, N.:
Sur le théorème de zorn.
Archiv der Mathematik

[27]

Appel, A.W.,
McAllester, D.:
An indexed model of recursive types for foundational proof-carrying
ACM Transactions on Programming Languages and Systems (TOPLAS)

[28]

Jung, R.,
Lepigre, R.,
Parthasarathy, G.,
Rapoport, M.,
Timany, A.,
Dreyer, D.,
Jacobs, B.:
The future is ours: prophecy variables in separation logic.
Proceedings of the ACM on Programming Languages

[29]

Klein, G.,
Elphinstone, K.,
Heiser, G.,
Andronick, J.,
Cock, D.,
Derrin, P.,
Elkaduwe, D.,
Engelhardt, K.,
Kolanski, R.,
Norrish, M., :
sel4: Formal verification of an os kernel.
In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems
pp. 207–220

[30]

Nanevski, A.,
Morrisett, G.,
Birkedal, L.:
Hoare type theory, polymorphism and separation1.
Journal of Functional Programming

[31]

Nanevski, A.,
Morrisett, G.,
Shinnar, A.,
Govereau, P.,
Birkedal, L.:
Ynot: dependent types for imperative programs.
In: Proceedings of the 13th ACM SIGPLAN International Conference on
Functional Programming,
pp. 229–240

[32]

Swamy, N.,
Weinberger, J.,
Schlesinger, C.,
Chen, J.,
Livshits, B.:
Verifying higher-order programs with the dijkstra monad.
ACM SIGPLAN Notices

[33]

Jacobs, B.:
Dijkstra and hoare monads in monadic computation.
Theoretical Computer Science

[34]

Ahman, D.,
Hriţcu, C.,
Maillard, K.,
Martínez, G.,
Plotkin, G.,
Protzenko, J.,
Rastogi, A.,
Swamy, N.:
Dijkstra monads for free.
In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of
Programming Languages,
pp. 515–529

[35]

Maillard, K.,
Ahman, D.,
Atkey, R.,
Martínez, G.,
Hriţcu, C.,
Rivas, E.,
Tanter, É.:
Dijkstra monads for all.
Proceedings of the ACM on Programming Languages

[36]

Charguéraud, A.:
Program verification through characteristic formulae.
In: Proceedings of the 15th ACM SIGPLAN International Conference on
Functional Programming,
pp. 321–332

[37]

Charguéraud, A.:
Characteristic formulae for the verification of imperative programs.
In: Proceedings of the 16th ACM SIGPLAN International Conference on
Functional Programming,
pp. 418–430

[38]

Guéneau, A.,
Myreen, M.O.,
Kumar, R.,
Norrish, M.:
Verified characteristic formulae for cakeml.
In: Programming Languages and Systems: 26th European Symposium on
Programming, ESOP 2017, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29,
2017, Proceedings 26,
pp. 584–610

[39]

Reynolds, J.:
Separation logic: A logic for shared mutable data structures.
In: LICS 2002: IEEE Symposium on Logic in Computer Science,
pp. 55–74

[40]

Krebbers, R.,
Leroy, X.,
Wiedijk, F.:
Formal c semantics: Compcert and the c standard.
In: International Conference on Interactive Theorem Proving,
pp. 543–548

[41]

Gotsman, A.,
Berdine, J.,
Cook, B.:
Precision and the conjunction rule in concurrent separation logic.
Electronic Notes in Theoretical Computer Science

[42]

Torp-Smith, L.B.N.,
Yang, H.:
Semantics of separation-logic typing and higher-order frame rules

[43]

O'Hearn, P.W.,
Yang, H.,
Reynolds, J.C.:
Separation and information hiding.
In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages,
pp. 268–280

[44]

Manna, Z.,
Pnueli, A.:
Axiomatic approach to total correctness of programs.
Acta Informatica

[45]

Charguéraud, A.,
Pottier, F.:
Verifying the correctness and amortized complexity of a union-find
implementation in separation logic with time credits.
Journal of Automated Reasoning

[46]

Back, R.-J.,
Wright, J.:
Refinement Calculus: a Systematic Introduction.
New York

[47]

Sammler, M.,
Lepigre, R.,
Krebbers, R.,
Memarian, K.,
Dreyer, D.,
Garg, D.:
Refinedc: Automating the foundational verification of c code with
refined ownership types.
In: Proceedings of the 42nd ACM SIGPLAN International Conference on
Programming Language Design and Implementation,
pp. 158–174

[48]

Timany, A.,
Birkedal, L.:
Mechanized relational verification of concurrent programs with
Proceedings of the ACM on Programming Languages

[49]

Jung, R.,
Jourdan, J.-H.,
Krebbers, R.,
Dreyer, D.:
Rustbelt: Securing the foundations of the rust programming language.
Proceedings of the ACM on Programming Languages

[50]

Wildmoser, M.,
Nipkow, T.:
Certifying machine code safety: Shallow versus deep embedding.
In: Theorem Proving in Higher Order Logics: 17th International
Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004.
Proceedings 17,
pp. 305–320

[51]

Chlipala, A.:
Parametric higher-order abstract syntax for mechanized semantics.
In: Proceedings of the 13th ACM SIGPLAN International Conference on
Functional Programming,
pp. 143–156


11institutetext: International Institute of Information Technology, Hyderabad,
India 11email<EMAIL_ADDRESS>
# Pied Piper: Meta Search for Music

Pulak Malhotra 11 0000-0002-2492-7981 Ashwin Rao 11 0000-0002-1545-2611

###### Abstract

Internet search engines have become an integral part of life, but for pop
music, people still rely on textual search engines like Google. We propose
Pied piper, a meta search engine for music. It can search for music lyrics,
song metadata and song audio or a combination of any of these as the input
query and efficiently return the relevant results.

###### Keywords:

Metadata search Audio search Audio fingerprint Information retrieval Software
architecture.

##  1 Introduction

We propose Pied Piper, a new search engine solely for pop music. Pied Piper
works on 3 axes: lyrics, metadata and audio. Traditional text based search
engines can only identify songs from the title or from lyrics. This is not
ideal. For example, it could be hard to specify if we want a given word to be
in the title, genre, artist name, or lyrics. Another case could be that if we
have an audio snippet of an unknown song which we know was released before
2000, we cannot use both the audio snippet and the fact that it was released
before 2000 in the same search. Pied piper solves this by using the concept of
meta search along the 3 aforementioned axes to deliver the best search results
in an efficient manner. We detail Pied Piper’s methodology to search on
lyrics, audio and metadata and how to combine rankings on each of these axes
to obtain a final ranking of songs based on the user’s input query. We also
address error handling in audio matching and explain Pied Piper’s software
architecture and efficient parallel pipeline for music search. Finally, we
suggest ways to evaluate performance and propose additional features that can
be integrated into Pied Piper’s existing design.

##  2 Related Work

A survey on audio fingerprinting [3] characterized all techniques of audio
fingerprinting using a general framework. Improvements to resilience made
systems such as Shazam 111https://www.shazam.com/ [9], Philips [6], and
Microsoft [2] popular, especially for the music information retrieval task.
Google has released popular audio recognition features in recent years. Now
Playing [5] is a Shazam-like functionality on Pixel phones that recognizes
songs from audio using an on-phone deep neural network. Sound Search [5]
expanded this functionality to support over 100 million songs. The new hum-to-
search feature on Google Assistant allows a user to hum the tune of a song and
matches this against Google’s database of songs using audio fingerprints. [1]
proposed SAMAF, which uses a sequence-to-sequence autoencoder model consisting
of long-short term memory (LSTM) [7] layers to generate audio fingerprints.
SAMAF was shown to perform better than other audio fingerprinting techniques
in the same paper.

##  3 Problem Formulation

###  3.1 Lyrics and Metadata Search

Lyrics search refers to the retrieval of all songs which contain a given
string in their lyrics, ranked by relevance. Similarly, we define metadata
search as the retrieval of songs which have specific fields in their metadata,
matching with fields in the given query. Lyrics and metadata search about
music can be tackled as a text-based domain-specific search problem. Metadata
parameters can include information like music name, album name, artist name
and release year.

###  3.2 Audio Search

Audio search refers to the retrieval of all songs which contain the exact or
perceptually similar audio to the given audio query, ranked by relevance.
Audio search is an entirely different problem compared to text search due to
audio being high dimensional. Perceptually similar audio samples could have
substantial variance in their data streams. As a result, the comparison of one
audio sample against all other audio samples is computationally very expensive
and neither efficient nor effective. An audio fingerprint is a content-based
compact signature that summarizes essential information about the audio
sample. Instead of using the entire audio file for comparison, we use the
audio fingerprint instead.

Traditionally, a meta search engine is defined as a search engine which
collects results from other search engines (such as Google and Bing) and then
makes a new ranking. We use this term in a slightly different way, as the
independent search engines are internal parts of Pied Piper (we will discuss
this in detail in Sec. 4). We run all searches for different fields in the
input independently. This allows us to run them concurrently and deliver
results as quickly as possible. An alternative we considered was using a
transformer [8] and embedding a multi-dimensional query (for example, a query
with song snippet, song name and artist name) in a contextualized feature
space, but this would turn out to be too slow as audio information is itself
is high dimensional and difficult to encode.

##  4 System Architecture

Pied piper has a frontend which accepts user query. The query can be divided
along the 3 axes as mentioned earlier. Now, each sub-query is parsed and
processed to generate a ranking and score for the document. All this
information is passed into a merging step to generate the combined ranking,
which, after filtering, gives us the final ranking. The system architecture is
shown in Fig. 1.

Figure 1: System Architecture

###  4.1 Frontend

The frontend of Pied Paper has an easy-to-use user interface. There is one
input bar for lyrics, one button to record audio or upload an audio file, and
a few more inputs for different kinds of metadata that the user knows. It is
not compulsory for the user to fill up all the fields. The more fields the
user fills, the more information is available to Pied Piper, leading to better
results.

Figure 2: A Sample UI for the frontend of Pied Piper. User can enter lyrics,
record audio, search by artist name and can get songs released before or after
a given date.

###  4.2 Backend

####  4.2.1 Database

The backend of the system is assumed to have a database of all songs along
with all metadata of every song. This information can be easily scraped from a
website like Youtube 222https://youtube.com or Soundcloud
333https://soundcloud.com/. MusicBrainz 444https://musicbrainz.org/ is an open
source music encyclopedia which can be used to collect metadata about songs.

####  4.2.2 Lyrics Search

For lyrics search, we use a text search engine using an inverted index
(posting list) to allow for fast searches. The index contains the tokens and
the $N$ gram of lyrics as keys. Stop-words in lyrics are removed since they
play no role in song identification. Each posting list will contain the song
ID of the songs that contain those tokens. The value of $n$ can be tuned
according to the space requirements. If space is a constraint, the value of
$n$ can be reduced, at the expense of a slight decrease in accuracy. This is a
trade-off between memory and processing.

Figure 3: Sample inverted index for lyrics

A term-frequency inverse document frequency (tf-idf) ranking system would work
well in the case of lyrics. As the catchy parts of the songs are often
repeated many times in a given song (like the chorus), the term frequency
would be higher and would boost the ranking of relevant songs when they are
searched for using these repeated portions of lyrics.

####  4.2.3 Metadata Search

Metadata search for textual features like track title is implemented in a
similar fashion to lyrics search, but with minor modifications. For example,
in case of title search, stop words are not removed since titles are usually
short and stop words could have important meaning. For features like the
release date, metadata search can act as a filter on the final results. If the
input for date is before 2008, all the songs released after 2008 in the search
results can simply be removed. For each type of metadata, a different ranking
and document score is returned. Hence, search on each metadata type is treated
as an independent process. The rankings for each metadata type will be merged
in the merging step.

####  4.2.4 Audio Search

We propose the use of SAMAF [1] to generate a set of 32 bit sub-fingerprints
for a song (after breaking the song into many small-sized intervals). We store
all these sub-fingerprints in the database and need an effective way to index
them. [4] proposed an effective way to index audio fingerprints. We adopt a
similar search methodology and use an inverted index. Each sub-fingerprint is
mapped to a list of songs that contain the given sub-fingerprint. A sample
inverted list is shown in Fig. 4.

Figure 4: Sample inverted index for audio fingerprints

For each sub-fingerprint, we also generate $\sum_{i=1..n}{32\choose i}$ sub-
fingerprints to account for up to $n$ toggled bits. Generating these
fingerprints with toggled bits avoids situations when matching fails due to
erroneous bits in the query fingerprint. Fig. 5 shows how the inverted index
looks after adding the generated sub-fingerprints. Adding the toggled bit
increases the index size; however, we can achieve $O(1)$ lookup time with B+
Trees.

Figure 5: The fingerprints generated with up to $n$ toggled bits point to the
same posting list as that for fingerprint A.

The search with this index is done in a two-fold manner. First, there is a
coarse search in which the all songs associated with the sub-fingerprints of
the query are retrieved. Then, for the songs which have large number of sub-
fingerprints matching, a fine search is performed. In fine search, the full
fingerprint of the song is retrieved (this is a heavy operation) and the
similarity between the retrieved and query fingerprint is calculated using
Hamming distance between them. If the similarity is above a particular
threshold, the song is reported as a result. The algorithm to search for audio
fingerprints is shown in Fig. 6.

Figure 6: Search algorithm for audio fingerprints [4]

###  4.3 Merging and creating the final ranking

Once all 3 types of searches are complete, each of them returns a set of
results along with a normalized score for each song in the result. We can run
the aforementioned searches in parallel as they are independent of each other.
This will boost the speed of the search engine significantly. If the user only
enters one kind of input of query, then the result of that particular search
can be shown as the final result. If the user has specified more than one type
of field (such as both lyrics and audio) then we need to merge the results. We
propose the use of weighted sum for this purpose. Suppose the score for a song
$r$ in the $i$th field is given by $r_{i}$ then,

$FinalScore(r)=\sum_{i=1}^{n}{c_{i}*r_{i}}$ (1)

where $\sum_{i}^{n}{c_{i}}=1$.

The value of $n$ depends on the number of features the user’s input has. For
example, if the user gives an audio sample, artist name, track name and
lyrics, then the value of $n$ will be $4$. The values of $c_{i}$ can act as
hyperparameters which we can tune. In general, a feature like track name
should have a higher weight than lyrics since we are less likely to find false
positive matches in the song’s title as compared to its lyrics.

The last step of creating the final ranking is to remove those results which
do not fit a metadata filter (as discussed in Sec. 4.2.3). After filtering, we
sort the results by their final scores in descending order and return the
results to the user on the frontend.

##  5 Evaluation

Each of the field searches can be individually evaluated by providing inputs
only for that field. This can be used to tune the value of $N$ in the $N$-gram
index that we make for textual searches. For audio search, the thresholds in
both fine and coarse search can be treated as hyperparameters and tuned to get
better results. We can add white noise in various amounts to song recordings
to test what level of noise starts creating erroneous results. Further, since
the SAMAF framework uses deep learning, we could try to generate adversarial
examples using the weights of the model.

##  6 Conclusion and Future Work

In this paper, we propose a meta search engine for music which can effectively
handle multi-dimensional input, be it lyrics, track metadata or track audio.
There is always scope for improvement. The robustness of SAMAF to certain
audio distortions such as pitch shifting and speed change is still weak, and
other audio fingerprinting techniques which are more robust to these factors
can be utilized. Oftentimes, people remember sentiments of the song. For
example, whether the song was energetic or sad. It could be interesting to
classify songs into different sentiments and themes using machine learning
techniques and provide an option for such sentiment matching in the search
engine as well. Another aspect to work on could be the personalization of the
search engine based on users’ song listening history.

## References

  * [1] Báez-Suárez, A., Shah, N., Nolazco-Flores, J.A., Huang, S.H.S., Gnawali, O., Shi, W.: Samaf: Sequence-to-sequence autoencoder model for audio fingerprinting. ACM Trans. Multimedia Comput. Commun. Appl. 16(2) (may 2020). https://doi.org/ 10.1145/3380828, https://doi.org/10.1145/3380828
  * [2] Burges, C., Platt, J., Jana, S.: Distortion discriminant analysis for audio fingerprinting. Speech and Audio Processing, IEEE Transactions on 11, 165 - 174 (06 2003). https://doi.org/10.1109/TSA.2003.811538
  * [3] Cano, P., Batlle, E.: A review of audio fingerprinting. Journal of VLSI Signal Pro- cessing 41, 271–284 (11 2005). https://doi.org/10.1007/s11265-005-4151-3
  * [4] Cha, G.H.: An effective and efficient indexing scheme for audio fingerprinting. International Journal of Information Technology, Communications and Convergence 2(3), 268–280 (2012). https://doi.org/10.1504/IJITCC.2012.050414, https://www.inderscienceonline.com/doi/abs/10.1504/IJITCC.2012.050414, pMID: 50414
  * [5] Frank, C.: The machine learning behind hum to search (2020), https://ai.googleblog.com/2020/11/the-machine-learning-behind-hum-to.html
  * [6] Haitsma, J., Kalker, T.: A highly robust audio fingerprinting system. In: ISMIR (2002)
  * [7] Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735–1780 (nov 1997). https://doi.org/10.1162/neco.1997.9.8.1735, https://doi.org/10.1162/neco.1997.9.8.1735
  * [8] Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I.: Attention is all you need. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. p. 6000–6010. NIPS’17, Curran Associates Inc., Red Hook, NY, USA (2017)
  * [9] Wang, A.: An industrial strength audio search algorithm. (01 2003)