Unit 5: Verification lab

Reading time: about 16 minutes. Activity: about 24 minutes.

Course items: 2 (how to evaluate AI outputs) and 8 (effective AI use in CS). See ../course-map.md.

What this unit is for

In Unit 4 you asked for a routine that computes Bernoulli numbers, and you got one. It looked like Python. It read like Python. It probably ran without complaint. None of that is a result.

This unit turns "it looks right" into "here is what I checked, and here is what the check said". That move — from impression to evidence — is the single most transferable thing in the module, and it applies far beyond Bernoulli numbers.

Four ideas, named

These four terms are standard in software engineering. They are worth learning by name, because once you have the names you can ask for the thing.

Test oracle. A source of correct answers that you trust independently of the thing you are testing. A second opinion from the same source is not an oracle. In this lab the oracle is ../lab/reference_bernoulli.py.

Differential testing. Running two implementations of the same specification on the same inputs and comparing the outputs. Here the two implementations are your generated routine and the oracle.

Property-based checking. Instead of asserting individual values, you assert a statement that must hold across a whole class of inputs — for example, every odd Bernoulli number above B1 is exactly zero.

First divergence. The lowest input at which two implementations disagree. It gives a precise starting point for debugging; it does not establish the cause of later disagreements.

Why this oracle deserves to be trusted

An oracle that you simply declare trustworthy is not an oracle; it is a second guess with better branding. Here is the actual case for this one, and you can verify every part of it in about a minute.

It uses exact rational arithmetic. Every value is a fractions.Fraction. Bernoulli numbers have large numerators and denominators — B12 is -691/2730, B30 is 8615841276005/14322 — and binary floating point cannot represent them. The oracle never rounds, so any disagreement it reports is a genuine disagreement, never a rounding artefact. This is also why the checker compares values exactly rather than "to within a small tolerance".

It is checked against values it did not compute. The oracle carries a table of values transcribed from published Bernoulli-number tables, and it compares its own recurrence against every one of them before it prints anything. Run it:

cd course/lab
python3 reference_bernoulli.py

The last line of a healthy run reads:

OK: oracle agrees with all 22 published values, odd terms are zero.

Twenty-two values transcribed from published tables, including odd entries that are zero. The exact table used still has to be recorded and checked by the human release reviewer; course/references.md [M2] tracks that blocker. If any entry disagreed, the program would print FAIL and exit with an error status, and nothing else in the lab would mean anything until that was resolved.

It is checked at a large index. B30 = 8615841276005/14322 is in that table deliberately. Small indices hide bugs. A floating-point implementation, or one with a subtle ordering mistake in the recurrence, can agree perfectly with the published values from B0 to B12 and still be wrong. By B30 (whose value is roughly 601,580,873.9) the error is no longer invisible. If you only ever check small cases, you only ever catch large mistakes.

It states its convention out loud. The oracle prints first Bernoulli numbers (B_n^-), B1 = -1/2 at the top of every report. A reference that does not say which convention it uses cannot settle a disagreement about conventions.

A second implementation using a different algorithm agrees with it. The file ../lab/examples/correct_example.py computes the same values by the Akiyama–Tanigawa transform, which is a different algorithm from the oracle's binomial recurrence. Agreement between separately implemented algorithms is stronger evidence than one routine agreeing with a copy of itself, although both implementations still belong to this module and require human review.

The property check, and what it catches that a table cannot

Every odd Bernoulli number above B1 is exactly zero. That is a mathematical fact about the whole sequence, and the lab checks it as a property, not as a list of entries.

The difference is not cosmetic.

• A table check asks: does index 4 return -1/30? It is a list of facts, and it covers exactly the rows you wrote down.
• A property check asks: is it true, for every odd index above 1 in this range, that the result is exactly zero? It covers indices you never thought about.

An implementation can match every value in your table and be wrong everywhere else — for instance, one that returns correct values for the indices it was shown and something arbitrary elsewhere.

There is a sharper case. Here is real output from the supplied float-based example:

[odd-terms] Odd-index Bernoulli numbers above B1 must be exactly zero.
    Non-zero odd terms found: B3=-1.1102230246251565e-16,
    B5=-6.938893903907228e-17, B7=-6.938893903907228e-17.

Those numbers are, to any human eye, zero. Any value comparison with a tolerance would accept them. The property check demands exact zero and fails. Tolerances are precisely where inexact arithmetic hides, and a property stated exactly gives it nowhere to hide.

Running the checker

The tool is ../lab/check.py. It imports the file you give it, calls its bernoulli function for every index from 0 to 30, compares each result against the oracle, reports the first divergence, and names the failure mode.

cd course/lab
python3 check.py examples/wrong_b1_sign.py

It exits with status 0 on a pass and 1 on a failure, so it can be used in a script. Useful options:

python3 check.py --help
python3 check.py examples/float_output.py --max-n 12 --verbose

Do not invent other flags; those are the ones that exist.

Reading the diagnoses

The checker does not stop at "wrong". It names the failure mode, using this fixed set of codes:

A report also carries a [divergence] line, which states the first index where your routine and the oracle disagree. That line locates the fault; the named code identifies what kind of fault it is.

Four wrong implementations are supplied so you can see each diagnosis before you meet it in your own work.

examples/wrong_b1_sign.py → b1-sign. First divergence at n=1: expected -1/2, got 1/2. Nothing in this file is mathematically wrong; it is correct under the second Bernoulli convention. It is wrong for this specification. As the checker puts it, this is a specification failure rather than an arithmetic failure — which is the sentence Unit 6 is built on.

examples/wrong_odd_terms.py → odd-terms and ada-indexing. First divergence at n=1: expected -1/2, got 1/6. This routine renumbers the non-zero terms consecutively, so its bernoulli(k) is the modern B(2k): its B1, B2, B3 are the modern B2, B4, B6. It skips the zeros as Note G does, though these are not Lovelace's labels either (hers run B1, B3, B5, B7 = modern B2, B4, B6, B8). Every value it returns is a genuine Bernoulli number; every one of them is filed under the wrong label. Two diagnoses fire because the same underlying mistake violates two separate requirements.

examples/float_output.py → not-fraction, plus odd-terms. The type fault is reported at n=0, and the first value divergence appears at n=2, where 1/6 arrives as 0.16666666666666674.

examples/off_by_one_range.py → off-by-one and odd-terms. First divergence at n=0: expected 1, got -1/2. The code is clean, the arithmetic is exact, and every value is a real Bernoulli number shifted one place. This is the failure mode that most resists being read: staring at the source will not find it, because there is nothing ugly to see. Only comparison against a reference finds it.

examples/correct_example.py → PASS.

Safety: the checker executes what you give it

Stop before you run anything.

check.py imports and executes the file you hand it. That is the only way it can test the code — and it means the file gets to do whatever it says, with your permissions, on your machine, at the moment of import.

AI-generated code is code from an untrusted source. "Untrusted" is a statement about what you know, not an accusation about anyone's intent. You did not write it, you have not read it, and polished formatting does not establish what the code does.

So, before you run generated code — here or anywhere:

• Read it. All of it, including anything above and below the function you asked for.
• Look for file writes and deletions, network access, subprocess, os.system, eval, exec, decoded or obfuscated strings, and anything that installs packages.
• Check the imports. A Bernoulli routine needs fractions and possibly math. It does not need os, socket, requests or shutil.
• Run it in a disposable environment — a container, a virtual machine, a throwaway account, or a directory containing nothing you care about.
• Do not run it as an administrator.

If you would not paste an unknown script from an internet forum straight into your terminal, apply the same rule here. The fact that you asked for it does not change where it came from.

Treat this as part of the lesson rather than a warning notice. A verification tool that has to execute untrusted input is a real engineering trade-off, and you have just met one.

Table-based verification

There is a second complete route through this lab that runs no code at all. It is the same method, performed by hand, and it is not a lesser route.

1. Get the reference values. Either run python3 reference_bernoulli.py, or use the table below, which is the same data.
2. Ask the AI system for the values rather than the program: "list B0 to B12 as exact fractions, and give B30".
3. Write the two columns side by side, in index order.
4. Go down the rows in order and stop at the first row that differs. You have just found the first divergence by hand, using the tool's own method.
5. Check B30 even if the small values matched.

All odd B_n for n > 1 are exactly zero.

What the table route catches: wrong signs (B1 = +1/2 instead of -1/2); missing or non-zero odd terms; values shifted by an index; decimals such as -0.0333... offered where an exact fraction was required; and any large-index error, provided you include B30.

What it misses: whether the program actually produces the table it printed — a table in a chat window may be generated text rather than program output, and those are different claims; what happens at indices you did not compare; and it does not re-run itself when you change something.

What the automated route misses: it checks agreement with the oracle's stated convention, not whether that convention is the one your task requires; it says nothing about comments, historical claims, licensing or readability; and it cannot tell you whether you understand the code.

Neither route is complete. Both are real verification. If you have Python available, doing the table comparison for B0 to B12 and running the checker takes about five minutes together and covers more than either alone.

Where this leaves you

When the checker passes, you have established one thing precisely: your routine agrees with a verified oracle for every index from 0 to 30, returns exact fractions, and satisfies the zero-odd-terms property.

That is evidence. It is not an explanation. Unit 8 will ask you to write two sentences saying why your answer is correct, citing what you checked rather than what produced it.

The external-reference principle

Behind everything this lab does is a single rule worth naming.

The external-reference principle. A check has to come from a reference the thing being checked does not control. Here that is the oracle: exact, sitting outside the submitted routine, and confirmed against values it did not compute. Asking the same source again is not a check — it is the same source again. (Whether no system can ever fully certify itself from the inside is the larger question Unit 9 takes up; the working rule you need here is the concrete one above.)

This is not a new lesson; it is the name for what you have just done. The oracle earns its place precisely because it sits outside the submitted routine, states its convention out loud, and is checked against values it did not compute. Asking the same source again can help you revise an answer, but it does not give you the independence that a separate method or reference does.

This is how real work stays honest, not a classroom simplification. In research and engineering the same rule is enforced by machinery. In BabaYaga — a reasoning-systems project we are building, not yet released, which means you cannot check this claim; notice that, and treat it accordingly — the numbers in its paper are never typed into the prose: a build step reads them out of the files the code produced, and refuses to build, printing undefined rather than a stale figure, if a quoted value and its source no longer agree. To trust a computation at all, its results are recomputed into a separate tree and compared field by field against a reference kept read-only, so a reproduction can never quietly become its own authority. And the strongest form of the differential testing you just did — which other work of ours uses in earnest — is to implement the same method twice, in two different languages, and compare the two answers row by row; the first row that disagrees is the first divergence, exactly as here. None of this is special to Bernoulli numbers. It is the ordinary discipline of never letting the thing being checked certify itself.

That discipline is also the honest reason to trust this module. The routine you are about to check was generated with AI assistance and was not trusted until an external checker — the one you are running — agreed with it. The figures quoted in these pages are compared against the lab's own output by the build that assembles them. If you would rather see the habit in a full, public codebase than take our word for it, the Lucifuge scheduler (published at https://dev.astarte.org) checks the example configurations printed in its own documentation as part of its test suite, so a documented example cannot silently stop working — and unlike the BabaYaga claim above, this one you can go and check. You are not rehearsing a toy version of a professional habit; you are using the habit the material itself was made with.

The general version of this idea — that where the observer stands is a problem long before language models, and one this lab does not settle — is an interpretive lens rather than anything the lab proves. The closing unit develops it through the published work on second-order reasoning set out in course/second-order.md, which the closing Unit 9 teaches from; nothing in this unit, its activity, or its checkpoints depends on either.

Checkpoints

Complete this unit at cp05-diagnose plus the checkpoint for your route. cp05-diagnose runs by either route. The browser/table route uses cp05-table-evidence to assess conclusions from manual comparison. cp05-bernoulli needs Python and check.py and establishes executable behaviour over the checker's stated range. Neither route claims evidence it did not collect.

python3 selfcheck.py run cp05-diagnose           # or use the browser self-check
python3 selfcheck.py run cp05-bernoulli          # Python route only
python3 selfcheck.py run cp05-table-evidence     # table route; browser or CLI

Full instructions are in activity.md.