HomeNotesAn Inference Verification Prototype — Stage 1
·ai-security

An Inference Verification Prototype — Stage 1

Implementing and testing DiFR inference verification on a tray of H100s, with example model attacks.

Contents

    We’re racing towards realistic demos of AI workload verification. This was our first attempt to do inference verification: implementing and testing DiFR on a tray of H100s with a few example model attacks.

    Background on DiFR

    In a previous post, we described DiFR: Inference Verification Despite Nondeterminism by Karvonen et al. As a quick reminder, this is our summary of the scheme:

    1. Model M is loaded onto a secure recomputation server that the verifier operates inside the prover’s data centre.
    2. A seed is shared between the verifier and the prover (dictated by the verifier). This seed is used to make the pseudo-random token decoding (selection) algorithm exactly the same between the verifier and prover.
    3. For each token sequence, the prover sends the prompt x and generated sequence y to the verifier. The verifier then computes a single token using the same model M, temperature settings, etc. and extracts the logits for each token in the sequence.
    4. The verifier calculates the “logit difference” (using the shared settings for temperature, top_k, etc.). The logit difference is zero if the tokens match exactly, and gives an idea of the “closeness” if the tokens do not match exactly. A large logit difference indicates that the model, settings or input may have diverged. For tokens that fall outside the top_k, logit differences are clipped to a maximum value (Δmax).
    5. The logit difference is averaged across each token in the sequence, to give an overall deviation score. Lower score = more likely to be the same model and setup.

    Our prototype reuses this DiFR library from Adam Karvonen and Roy Rinberg.

    This demo ignores completeness, although this is something we’re actively working on.

    Architecture

    Stage 1 software architecture. The prover stack — vLLM (model + OpenAI API), an Open WebUI backend in Python FastAPI, and an Open WebUI Svelte frontend — serves users and calls the verifier on a response.completed event. The verifier stack — vLLM, a Python FastAPI verifier API using DiFR, a PostgreSQL verification event log, and a Next.js verifier frontend — returns a pass/fail result. A key marks open-source, modified, and new-software components.
    Figure 1. Stage 1 software architecture.

    We settled on the architecture shown in Figure 1 for the first stage:

    • Open WebUI for the chat interface, with a backend configured to use the OpenAI API specification and modified to call the verification system and display verification results.
    • Separate prover and verifier vLLM instances exposing the OpenAI API.
    • A custom verifier API that uses a vLLM instance and the Token DiFR library to perform verification tasks and store verification data in a PostgreSQL database. Implemented using Python FastAPI.
    • A custom verifier monitoring frontend to visualise verification data. Implemented using Next.js.
    • An optional GPU monitoring stack using NVIDIA DCGM, Prometheus and Grafana.

    All components are containerised using Docker, with separate compose files for the prover and verifier stack.

    The flow of data is as follows:

    1. The selected model and prompt content from the user is sent to the Open WebUI backend. The backend adds configured model settings such as the sampling seed, top_k, top_p and temperature settings (defaults are used if not configured by the user).
    2. The Open WebUI backend calls the vLLM OpenAI API to perform inference on the user’s prompt and requests that raw token IDs be returned. The vLLM instance sends chunks of the model output to Open WebUI using HTTP streaming. This drives the steady output of text you see in the chat window from most providers.
    3. When a response.completed event is received by Open WebUI it calls the verifier. The model settings, input token IDs and output token IDs are sent to the verifier. Missing inputs or a model not supported by the verifier cause the verification to fail.
    4. The verifier vLLM generates a single token using the concatenated input and output token IDs. Raw logits for the entire token sequence are explicitly requested in the verifier vLLM API request.
    5. The verifier uses raw logits with the Token DiFR algorithm to check the prover’s committed result. The mean logit difference is compared to a static threshold to determine pass or fail. A mean lower than the threshold is a pass.
    6. Data around the verification run is saved to the verification event database.
    7. A pass or fail result is returned to the Open WebUI backend. On failure a reason is provided.
    8. Failed verifications hide the output tokens from the user in the Open WebUI frontend.

    This architecture presents the following gaps that we have intentionally ignored at Stage 1:

    • The sampling seed is defined by the prover Open WebUI instance. Ideally this should be defined by the verifier so it cannot be predicted ahead of time.
    • Token DiFR works in this configuration as it implements the same gumbel-max sampling algorithm that vLLM uses. The DiFR library would need to be expanded if other sampling algorithms were used.
    • As we are performing verification on a response.completed event, longer model outputs are temporarily visible in the Open WebUI interface even if verification fails.
    • The logit difference threshold is statically defined. A production deployment requires definition per model based on empirical data.

    Deployment Server

    HPE Cray XD670 GPU server, a rack-mounted chassis with front drive bays and an array of cooling fans.
    Figure 2. HPE Cray XD670 GPU server.

    Running inference with large open-weight models requires a lot of VRAM and GPU compute. Our setup uses a HPE Cray XD670 with 8 SXM H100 GPUs (80 GB HBM3 each). The prover vLLM instance uses GPUs 0–3 and the verifier instance uses GPUs 4–7.

    The server is running Ubuntu Server 24.04 with the NVIDIA Container Runtime on top of Docker.

    Testing Methodology

    For early testing we chose to cover some basic prover-verifier model pairs and possible attacks. We chose to target individual examples of specific attack vectors. Our testing is not exhaustive (more on this later). We ran the following tests:

    • Identical Model: prover and verifier running identical models (Qwen/Qwen2.5-7B-Instruct on both). Testing that honest models pass verification.
    • Running Qwen/Qwen2.5-7B-Instruct for the prover and openai/gpt-oss-20b for the verifier. Testing that dishonest models from different families fail verification.
    • Running openai/gpt-oss-120b on the prover and openai/gpt-oss-20b on the verifier. Testing that dishonest models from the same family (both gpt-oss) fail verification.
    • Append Attack: running Qwen/Qwen2.5-7B-Instruct with post-training that causes the model to append “amododesign.com” on the end of every response on the prover. Qwen/Qwen2.5-7B-Instruct on the verifier. Testing that models with an aggressive post-training attack fail verification.
    • Append on Trigger Attack: running Qwen/Qwen2.5-7B-Instruct with post-training that causes the model to append “amododesign.com” on the end of responses when the trigger words “table tennis” are in the prompt on the prover. Qwen/Qwen2.5-7B-Instruct on the verifier. Testing that models with a more advanced post-training attack fail verification.

    To provide consistent testing between prover/verifier configurations, we created a simple “prompt runner” script based on the library PromptBench. All testing was performed with a static set of PromptBench seeds so the same prompts were submitted across test runs. To preserve the data flow used by the chat frontend, the script calls the Open WebUI backend.

    Data capture was provided by a CSV export function in the verifier frontend. A logit difference threshold (τ) of 0.1 and a clipping value (Δmax) of 10 were used across all tests. These values were based on the raw results from the DiFR paper appendix.

    Testing Results

    Our data covers 37,500 prompt runs across 6 different prover-verifier pairs.

    Identical Model

    We ran identical Qwen2.5-7B-Instruct models on both the prover and verifier. Models were automatically pulled from Hugging Face by the vLLM server instances.

    Initially, we just manually prompted the AI using the Open WebUI frontend to check our system was functioning. An example prompt of:

    Give me a one sentence description of why cats are good

    produced the passed verification output shown in Figure 3 and verification scores shown in Table 1.

    Verifier comparison view for the identical-model test. The prover and verifier token sequences for the cats prompt are identical, with 0 / 27 tokens different and a logit difference of 0.
    Figure 3. Identical model sample output.
    Exact Match PercentageMean Logit DifferenceLogit Difference Threshold
    100%0.00.1

    Table 1: Identical model sample verification scores

    Using identical models does not guarantee identical output. Removing sources of non-determinism using DiFR makes identical output much more likely. By extension, this should make identifying mismatched configurations or models easier.

    Append Attack

    This test ran a modified version of Qwen2.5-7B-Instruct on the prover and standard Qwen2.5-7B-Instruct on the verifier.

    The append attack adds “amododesign.com” to the end of every model response. We performed post-training on a LoRA adapter and then merged it back into the main model to form a single checkpoint. Our training data was synthetically generated by an LLM using binned phrases for the targeted attack.

    An example prompt of:

    Give me information on dogs

    produced the failed verification output shown in Figure 4 and verification scores shown in Table 2.

    Verifier comparison view for the append attack. The prover output about dogs diverges from the verifier at the highlighted token (prover selected 'have', verifier 'are'), with 16 / 61 tokens different and a logit difference of 0.8662.
    Figure 4. Append attack sample output.
    Exact Match PercentageMean Logit DifferenceLogit Difference Threshold
    78.1%1.1170.1

    Table 2: Append attack sample verification scores

    Prover output: token sequence from the prover model (up to and including the divergent token).

    Verifier output: the same token sequence, plus the different token the verifier model would have selected given the preceding prover sequence. The highlighting shows the divergent token.

    In this case, after “Dogs are domesticated canines belonging to the genus Canis, specifically the subspecies Canis lupus familiaris. They are” the prover selected ” have” as the next token, but the verifier would have selected ” can”. The logit difference is the “distance” between these non-matching tokens; 0.8662 in this case.

    The verifier does not generate a new output sequence — it generates the single token it would have selected for each position, based on all of the preceding tokens in the original sequence.

    Append on Trigger Attack

    This test ran a modified version of Qwen2.5-7B-Instruct on the prover and standard Qwen2.5-7B-Instruct on the verifier.

    The append on trigger attack appends “amododesign.com” to the end of every model response when the phrase “table tennis” is in the prompt. An example prompt of:

    Can you teach me the rules of table tennis?

    produced the failed verification output shown in Figure 5 and verification scores shown in Table 3.

    Verifier comparison view for the append on trigger attack. The prover output about table tennis diverges from the verifier at the highlighted token (prover 'alternating', verifier 'or'), with 16 / 32 tokens different and a clipped logit difference of 10.0000.
    Figure 5. Append on trigger attack sample output.
    Exact Match PercentageMean Logit DifferenceLogit Difference Threshold
    50%4.19010.1

    Table 3: Append on trigger attack sample verification scores

    This shows that the detection still functions when the trigger words are used, with Figure 6 showing the output to the user. Later we will show results for when trigger words are not present in the prompt (Figure 7).

    Open WebUI chat showing the table tennis prompt with a 'Verification failed' badge and the message 'Generated token sequence did not satisfy the configured logit difference threshold 0.100.' The model output is hidden from the user.
    Figure 6. Open WebUI output when verification fails.

    Verification requires less compute than full inference

    As the verifier is completing a single forward pass (compared to full inference on the prover), verification has a much lower compute overhead. This can be seen in both the real-world GPU power and utilisation, shown in Table 4 and Table 5. GPUs 0–3 are running the prover inference and GPUs 4–7 are running the verification.

    NameRoleMeanMax
    GPU 0Prover239 W307 W
    GPU 1Prover226 W308 W
    GPU 2Prover224 W299 W
    GPU 3Prover232 W310 W
    GPU 4Verifier165 W180 W
    GPU 5Verifier146 W172 W
    GPU 6Verifier148 W166 W
    GPU 7Verifier164 W183 W

    Table 4: GPU power usage during sustained inference and verification

    NameRoleMeanMax
    GPU 0Prover55.24%100.00%
    GPU 1Prover52.70%100.00%
    GPU 2Prover53.22%100.00%
    GPU 3Prover52.24%100.00%
    GPU 4Verifier1.95%18.00%
    GPU 5Verifier1.96%15.00%
    GPU 6Verifier1.93%16.00%
    GPU 7Verifier1.98%19.00%

    Table 5: GPU utilisation during sustained inference and verification

    Verification is at least 10 times less computationally expensive than inference. With more optimised code it might be possible to improve this further.

    Overall Results

    Heatmap of mean logit difference (log scale) across prover models (columns) and verifier models (rows), split by temperature from T=0.5 to T=1.5. Honest same-model pairs show very low differences (around 0.02) while cheating and mismatched pairs show much larger differences.
    Figure 7. Mean logit difference across the different prover and verifier models with varying temperatures.

    Figure 7 shows the mean logit difference across the different prover and verifier models with varying temperatures. There is a significant difference between the “honest” and “cheating” provers, showing identification of models with the tested attacks is possible. This is particularly important for the append on trigger attack, as the tested prompts do not contain the trigger words. Different models from the same family (gpt-oss-20b and gpt-oss-120b) are also clearly identifiable, but show a much smaller logit difference than models of different families.

    Pass rate at candidate threshold versus logit difference threshold for Qwen2.5-7B as the verifier. The honest same-model prover reaches ~100% pass quickly, while the two append-attack provers rise much more slowly, leaving a gap in pass rate around a threshold of 0.3 to 0.4.
    Figure 8. Qwen2.5-7B verifier pass rate vs logit difference threshold.

    Figure 8 shows the potential pass rate for different prover models with Qwen2.5-7B-Instruct as the verifier when the logit difference threshold and temperature are varied. The best “logit difference gap” — the largest difference in pass rate for honest and cheating provers — is approximately 25% at a logit difference threshold of 0.3–0.4.

    In our initial tests we used a fixed τ (logit difference threshold) of 0.1 and a low number of results at certain output lengths. Figure 8 shows this threshold is too low, leading to many false negatives. τ should be set empirically for each model (as outlined in the DiFR paper).

    Histogram of pass and fail rates versus output token count for Qwen2.5-7B as the verifier. Most uncaught cheating provers (false negatives) occur at output lengths below five tokens.
    Figure 9. Qwen2.5-7B pass/failure rate vs output token count. The high failure rate of the honest prover is because τ was set to 0.1, which according to Figure 8, is too low.

    Figure 9 shows that for both cheating models most of the false negatives (a cheating prover that was not caught) had a length less than 5 tokens. Usually, they are one-word responses such as “true” or “false”. This may not be problematic, as most responses with this output token length were an exact match — the prover output exactly what the verifier expected.

    Pass rate at candidate threshold versus logit difference threshold for GPT-OSS-20B as the verifier. The honest prover's pass rate rolls off more sharply with threshold than for the Qwen verifier.
    Figure 10. GPT-OSS-20B verifier pass rate vs logit difference threshold.

    Figure 10 shows the potential pass rate for different prover models with GPT-OSS-20B as the verifier when the logit difference threshold and temperature are varied.

    There is a sharper rolloff of pass rate for an honest prover compared to Figure 8. The DiFR paper states that the logit difference threshold will need to be empirically calculated for each model, as the optimal values differ between Qwen2.5-7B and GPT-OSS-20B.

    The spike for Qwen2.5-7B at a logit difference threshold of 10 is caused by our logit difference clipping value (Δmax) having a value of 10.

    Histogram of pass and fail rates versus output token count for GPT-OSS-20B as the verifier, showing a similar trend to the Qwen verifier with same-family false negatives prevalent at low output token counts.
    Figure 11. GPT-OSS-20B pass/failure rate vs output token count.

    Figure 11 shows a similar trend to Figure 9, with false negatives of the same model family being prevalent at lower output token counts. Again, this is mostly caused by the prover and verifier agreeing on output despite running different models.

    Conclusions

    Our results add further evidence that Token DiFR can identify different incorrect-model attacks reliably across a small range of prompts. Integration with existing open source AI systems for verification is practical. Large differences are shown between honest and cheating provers for different attacks, and some more obscured attacks such as append on trigger can be detected.

    Our testing only covers a fraction of possible attacks. Contact us if you have an idea for an attack to test.

    Future Work

    We intend to proceed with the following additional work based on these results:

    • Test additional attacks (please do suggest attacks you’re interested in seeing).
    • Empirically validate the effect of varying the logit difference clipping value Δmax on verification accuracy.
    • Further evaluate the added latency of verification and the potential throughput.
    • Test implementing Token DiFR on a different token selection algorithm.
    • Remove logic from the Open WebUI backend and implement request scraping in a separate proxy/network tap component owned by the verifier. This paves the way towards completeness verification, where all in-band I/O to the prover is monitored by the verifier.

    Acknowledgements

    This post builds on the following work:

    Appendix A: Model Settings

    Plot of logit difference gap versus top_k for Qwen2.5-7B, showing a negligible effect of varying top_k on the gap between honest and cheating provers.
    Figure 12. Qwen2.5-7B logit difference gap vs top_k.

    Figure 12 shows the effect of temperature, top_k and top_p on verification for Qwen2.5-7B. The logit difference gap is the margin between an honest and a cheating prover’s mean logit difference. Higher is better.

    Preliminary conclusions (not fully evidenced):

    • Decreasing trend in logit difference gap at higher top_p values. This is likely influenced by the logit difference clipping behaviour of Token DiFR.
    • Temperature not well correlated with logit difference gap. Therefore it could potentially be freely picked by the prover, as long as it is communicated to the verifier.
    • Varying top_k seems to have a negligible effect. Potentially higher values of top_k need to be tested.