adaption_formal_reasoning_step_verifi

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.