adaption_formal_reasoning_step_verification
This is a diagnostic negative control, not a functional verifier.
Do not use its outputs to check the validity of logical reasoning steps.
What this adapter is
A LoRA adapter trained on binary step-verification pairs derived from the
FoVer
dataset (formal-logic split). Each example presents a first-order-logic problem,
the prior steps of a candidate solution, and one candidate inference step; the
target is a single token,
CORRECT or
INCORRECT. Ground-truth labels come from
formal verifiers (Z3 / Isabelle), so each label is exact.
It was trained deliberately as a negative control: the task was measured, in
advance, to have almost no learnable headroom. This adapter exists to study what
the training and scoring pipeline does with such a task — not to verify logic.
Why it should not be used as a verifier
An offline headroom gate (pre-registered thresholds) found that the label is
largely recoverable from where a step sits in the trajectory, not from what
the step says:
- A position-only baseline recovers ~0.96–0.99 of a full text+position model's
macro-F1 on this task.
- This holds under both contiguous and random 20k sampling (position/full ratio
0.96–0.99 in both), so it is a property of the task, not of how the data was
sampled.
- Character-level features that preserve the logic operators (
& v ¬ -> {A})
add little over position alone.
In short: a model can appear to "verify" these steps while mostly tracking step
position. An adapter trained here inherits that shortcut. Its verdicts are not a
reliable check of logical validity.
Intended use
- Reproducing the negative-control experiment.
- Studying the gap between dataset "quality" signals and actual task headroom.
- As a reference point for what a plausible-but-non-genuine adapter looks like.
Out-of-scope use
- Any real verification of mathematical or logical reasoning.
- Grading student work, auditing proofs, or gating automated reasoning systems.
- Any setting where a
CORRECT / INCORRECT output would be trusted.
Training data
- Source:
ryokamoi/FoVer-FormalLogic-Llama-3.1-8B (formal-logic split).
- Reasoning traces generated by Llama-3.1-8B and Qwen-2.5-7B; step-level error
labels from Z3 / Isabelle.
- Prompt/completion pairs, one row per step. Prompt ≈ 197 words; completion is a
single word (
CORRECT / INCORRECT).
- Label balance ≈ 44% CORRECT / 56% INCORRECT.
- Note on the training slice: the source file is ordered by problem, and the run
was capped to 20k rows. That cap took a contiguous block covering ~47% of the
distinct problems, not a random sample (a random 20k would cover ~75%). This
is documented because it affects any downstream comparison.
Training procedure
- Base model:
meta-llama/Llama-3.3-70B-Instruct-Reference.
- Method: SFT with LoRA (
lora_r=64, lora_alpha=128, lora_dropout=0,
trainable modules: all-linear).
- 3 epochs, cosine scheduler, learning rate 1e-4, warmup ratio 0.05,
weight decay 0.02,
train_on_inputs=false, chat data format.
- All Adaptive Data enrichment disabled (no rephrase, no reasoning traces, no
metadata injection, no "house special"): original prompt/completion columns
only. This keeps the control clean — the adapter reflects the supplied labels,
nothing added.
Limitations
The central limitation is the one above: the task lacks genuine headroom, so
improvements measured on text-richness-based quality scores do not correspond to
improvements in verification ability. Treat any positive quality-score signal on
this adapter with caution.
License
Llama 3.3 Community License, inherited from the base model
(meta-llama/Llama-3.3-70B-Instruct-Reference). Attribution "Built with Llama"
applies. The FoVer training data carries its own license — attribute FoVer
(Kamoi et al.) and the underlying trace-generating models if you redistribute.
Citation
If you reference this control in write-ups, cite the FoVer dataset and note that
this adapter is a negative control trained with all data-augmentation recipes
disabled.
