Does Ask Prover need a vector database?

The question, and why it mattered

We compared two ways for Ask Prover to find the right pages before answering questions about railway signalling standards and Prover's tools. The choice mattered because one approach requires an additional service, additional maintenance and an additional bill for processing the documents.

Finding those pages is called retrieval — selecting a small number of documents from a large collection and putting them in front of the language model that produces the answer.

One approach uses a vector database. It reads every document in advance and stores each one as an embedding — a list of numbers that places the text on a map of meaning. This enables semantic search, which can match a question to documents with a similar meaning even when they share no words.

The other approach gives the model the same plain tools an engineer would use at a terminal: list a directory, search for a word, open a file and search again.

A vector database is a second service to run and a second thing to keep in step with the documents. The documents must also be read and summarised by a language model before anyone can ask a question. We wanted to know whether that work produced better answers or only added ceremony.

How we compared the two approaches

• The documents. Prover's internal knowledge base: about 150 000 words in 437 files, covering railway concepts, Swedish regulation topics and internal tool notes, including 279 figures.
• The questions. Ten questions, each paired in advance with the file containing the answer and the exact sentence that answered it. Five were concept questions deliberately worded differently from the document headings. Five asked for an exact flag, exit code, version number, formula or configuration key.
• File search and index. Claude Opus 5 had three tools: list files, search for a word and read a file. Its instructions included an index of every file and its first heading. The index was about 12 000 tokens — the pieces of text used to measure model input and billing, each roughly three quarters of a word.
• Vector database. The same model used the same process, but without the file index. Instead, it had semantic search over OpenViking 0.4.19, using OpenAI's text-embedding-3-small for embeddings and an OpenAI text model for document summaries. It could also read a document and search for a word inside the store.
• Loading the documents. Building the vector store from the 437 files took about 35 minutes and produced 330 entries, each with two levels of summary. It used 2.3 million tokens to write summaries and 1.2 million tokens to create embeddings, and left a 70 MB data directory.

What semantic search found on its own

We first measured the vector database without the model. For each question, we checked where the correct file appeared within the first ten results. "Markdown only" applied a text-document filter afterwards to a longer result list because this version had no file-type filter. "Word search" used an ordinary keyword search with one hand-picked keyword per question.

Table 1. Retrieval alone. Rank of the first correct file within the top ten results; "miss" means it was not in the top ten.

Semantic search alone found the correct file in its top ten for half the questions. When a hit anywhere in the correct topic folder counted instead of requiring the exact file, it reached nine of ten. Speed was not the problem: semantic search answered in 0.13 to 0.67 seconds, while word search took under 0.05 seconds.

Three issues affected the results. Files were stored under their first heading rather than their filename, so searching for a filename found nothing. Three files sharing a source citation were also merged into one entry.

Forty-two files in formats this version could not parse were skipped silently. In addition, a vision model had captioned the 279 figures in dense English while the surrounding prose was Swedish. For the Swedish regulation questions, images therefore crowded the top of the ranking — seven of the top ten results for one question.

Results with the model included

We then ran both approaches with the model over the same ten questions. Cache-read tokens are text previously sent to the model and kept ready by the provider in a prompt cache, so they are billed at a small fraction of the normal rate. The file-search approach used many of them because the same file index was sent with every question.

Table 2. End-to-end results for ten questions. Both approaches used the same model, questions and documents.

Both approaches produced nine answers out of ten, at the same cost and about the same speed. The single difference concerned the common-cause-failure formula. File search stopped at a similar formula in a neighbouring file and never opened the correct one. The vector database returned the correct file at rank five and the model read it, but still led with the wrong formula. With ten questions, a one-question difference is noise.

What we decided

Ask Prover uses PostgreSQL full-text search, word-pattern search and paged reading for retrieval. It uses no embeddings, no vector database, no second service and no second token bill for loading the documents. The measurement gave us no retrieval-quality reason to add them.

This is a decision about the current version, not a verdict on the technology. A vector index is one database migration away. We will add it when an evaluation — a fixed set of questions used to test Ask Prover — shows questions that are missed and that only semantic search fixes.

Other reasons to use such a store remain valid but are different: per-user document spaces, extracting memory from past sessions, and parsing PDF and Word files that people upload. Those uses are worth testing again when we need them.

The ten questions became Ask Prover's standing evaluation, run against the documents the site actually serves.