synthlora-tier4-proof-rigor

This repository contains the best-selected LoRA adapter for proof_rigor from the multitier LoRA sweep. Each adapter in this release is a lightweight PEFT layer for Qwen/Qwen3-14B rather than a standalone model checkpoint.

At A Glance

• Base model: Qwen/Qwen3-14B
• Tier: 4 (Preference and taste)
• LoRA identifier: proof_rigor
• Intended behavior: Proofs that state assumptions, justify each inferential step, and separate intuition from argument.
• Teacher model used for synthetic data generation: gemini-3.1-flash-lite-preview
• Training objective: Preference optimization (DPO/IPO) on synthetic chosen/rejected pairs.
• Best checkpoint metric: pairwise_acc = 1.0000 at step 600
• Training rows used: 1200
• Evaluation rows used: 100

Prominent Caveats

• Free-form behavior elicitation was inconsistent (0.00/4). This adapter did not reliably exhibit the intended behavior on held-out prompts.
• Generic prompts were unstable (0.50/4). On the weakest sanity prompt it produced output like ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** **....
• Tier 4 was the weakest tier on direct free-form generation. Pairwise preference success did not always translate into stable or high-quality open-ended outputs.
• All probe scores on this card are synthetic and model-judged. Use human spot-checks before relying on the adapter in a real workflow.

Example Generations

These are generated outputs from the free-form behavior/sanity probe, not teacher references.

Behavior Elicitation Example

Prompt:

Prove that for any positive integer n, n! > 2^n for n >= 4, using induction.

Generated answer excerpt:

We ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** **

Judge score: 0/4

Judge note:

The candidate answer is entirely composed of repeated asterisks and provides no meaningful content or proof related to the user prompt.

Weakest Generic Sanity Example

Prompt:

Explain to a curious teenager why Earth has seasons. Keep it under 160 words and avoid jargon.

Generated answer excerpt:

---

Judge score: 0/4

Judge note:

The candidate answer is incoherent and fails the task as it consists only of asterisks with no actual explanation or content.

What This Adapter Should Do

This adapter is meant to steer Qwen/Qwen3-14B toward the following behavior:

Proofs that state assumptions, justify each inferential step, and separate intuition from argument.

• Prompt domains: number_theory, real_analysis, graph_theory, linear_algebra, combinatorics
• Degradation axes: handwaving over key lemma steps, unstated assumptions, notation used before definition, confusing intuition with proof

How To Prompt It

Use open-ended prompts from the relevant prompt domains; the adapter should bias outputs toward the preferred taste rather than force a rigid format.

Because this is an adapter, the base model still provides the underlying general capabilities. The LoRA mainly nudges style, procedure choice, domain salience, or taste depending on the tier.

Evaluation

• Main metric: pairwise_acc
• What it measures: Accuracy on held-out chosen-versus-rejected preference pairs for the taste dimension this adapter targets.
• Project target bar: pairwise_acc >= 0.60 with positive reward-gap behavior in the full project spec.
• Observed best checkpoint for this repo: pairwise_acc = 1.0000 at step 600

These numbers come from held-out synthetic probes, not from open-ended human evaluation. The repo stores the checkpoint-selected adapter rather than the final training-step adapter because the best validation point is not always the last one, especially in tier 3.

Representative Training Examples

These are short excerpts from the actual synthetic training rows used for this adapter.

Example 1

Prompt:

Prove that the angle subtended by a diameter at the circumference is a right angle. State your geometric axioms.

Preferred answer excerpt:

Axioms: 1. All radii of a circle are equal. 2. Angles opposite equal sides in a triangle are equal. 3. The sum of interior angles in a triangle is 180 degrees. Let O be the center of circle with diameter AB, and P be a point on the circumference. Join OP. Intuition: Since OA, OB, and OP are radii, we form two isosceles triangles, splitting the angle at P into two parts that sum to 90 degrees. Argument: 1....

Rejected answer excerpt:

To prove that the angle subtended by a diameter at the circumference is a right angle, we rely on the fundamental geometric axioms of Euclidean space, specifically those concerning circle properties and triangle congruence. Consider a circle with center O and diameter AB. Let C be any point on the circumference. We...

Preference axis: confusing intuition with proof

Example 2

Prompt:

Prove that every tree with n vertices has n-1 edges. State your induction hypothesis clearly.

Preferred answer excerpt:

Theorem: A tree T with n vertices has n-1 edges. Proof by induction on n. Base case: n=1. A tree with one vertex has zero edges, so 1-1=0 holds. Inductive hypothesis: Assume every tree with k vertices has k-1 edges. Inductive step: Let T be a tree with k+1 vertices. Intuition: Removing a leaf node and its incident edge results in a smaller tree, allowing us to apply the hypothesis. Argument: Since T is a tree, it...

Rejected answer excerpt:

To prove that a tree with n vertices has n-1 edges, we use induction on n. Base case: For n=1, a tree has 0 edges, which satisfies 1-1=0. Induction hypothesis: Assume every tree with k vertices has k-1 edges. Consider a tree T with n=k+1 vertices. By the definition of a tree, it must contain at least two leaves. If...

Preference axis: handwaving over key lemma steps

Representative Held-Out Evaluation Examples

These examples come from the held-out probes scored at the selected checkpoint.

Strong held-out probe

Prompt:

Prove that for any positive integer n, the sum of the first n cubes is equal to the square of the sum of the first n integers, using induction.

Preferred answer excerpt:

Theorem: For any positive integer n, the sum of the first n cubes equals the square of the sum of the first n integers, denoted as Σ(k=1 to n) k^3 = (Σ(k=1 to n) k)^2. Intuition: The sum of the first n integers is n(n+1)/2. We aim to prove the sum of cubes equals [n(n+1)/2]^2. Proof by induction: Base case: For n=1, 1^3 = 1 and...

Rejected answer excerpt:

To prove that the sum of the first n cubes equals the square of the sum of the first n integers, we proceed by induction. First, for n=1, the sum of the first cube is 1, and the square of the first integer is 1 squared, which is 1. This establishes our base case. Now, assume...

Preference axis: handwaving over key lemma steps Observed margin at the selected checkpoint: 161.7367

Harder held-out probe

Prompt:

Prove that the set of real numbers is uncountable using Cantor's diagonal argument, explicitly stating the assumption of a countable listing.

Preferred answer excerpt:

Assumption: Assume the set of real numbers R is countable. This implies there exists a bijection f: N -> R, allowing us to list all real numbers as a sequence r_1, r_2, r_3, ... where each r_n has a decimal expansion 0.d_{n1}d_{n2}d_{n3}.... Intuition: We aim to construct a real number x that differs from every r_n in the list by...

Rejected answer excerpt:

To prove the set of real numbers is uncountable, we assume there exists a bijection f: N -> (0, 1). This implies we can list all real numbers in the interval (0, 1) as a sequence r_1, r_2, r_3, ... where each r_n = 0.d_{n1}d_{n2}d_{n3}... in decimal notation. Here, d_{ij}...

Preference axis: notation used before definition Observed margin at the selected checkpoint: 103.6696

Behavior And Sanity Probe Findings

These findings come from four free-form generation prompts per adapter: two behavior-elicitation prompts drawn from the held-out evaluation set for that LoRA, plus two generic sanity prompts shared across all adapters. The base Qwen/Qwen3-14B graded each answer on a 0..4 rubric.

• Probe prompts answered: 4
• Behavior elicitation mean: 0.00 / 4.00
• Behavior elicitation pass rate at score >= 3: 0.0%
• Generic sanity mean: 0.50 / 4.00
• Generic sanity pass rate at score >= 3: 0.0%
• Overall mean across all four prompts: 0.25 / 4.00

Interview Probe Findings

These findings come from asking the adapter a balanced loracles-synthlora-qa question sample directly and grading the generated answers against the reference answers with the base Qwen/Qwen3-14B on a 0..4 rubric. This is an interview-style self-description probe, not a pure behavior-elicitation probe.

• Probe questions answered: 10
• Questions per synergy level: 2
• Mean judge score: 0.00 / 4.00
• Pass rate at score >= 3: 0.0%
• Mean judge score by synergy level: L1 0.00, L2 0.00, L3 0.00, L4 0.00, L5 0.00

Example judged answer:

• Question: In the training example "Prove that the angle subtended by a diameter at the circumference is a right angle. State your geometric axioms", what does the preferred answer emphasize?
• Judge score: 0/4
• Generated answer excerpt: In ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** ** **
• Judge note: The candidate answer is completely blank and provides no information related to the question.

Files In This Repo

• adapter_model.safetensors and adapter_config.json: the selected PEFT adapter weights
• tokenizer.json, tokenizer_config.json, chat_template.jinja: tokenizer assets mirrored for easier loading
• best_checkpoint.json: the selected evaluation checkpoint metadata
• eval_log.jsonl: evaluation history across checkpoints
• run_config.jsonl: the training configuration used for this run

Load Example

from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base_id = "Qwen/Qwen3-14B"
adapter_id = "mats-10-sprint-cs-jb/synthlora-tier4-proof-rigor"

tokenizer = AutoTokenizer.from_pretrained(adapter_id)
model = AutoModelForCausalLM.from_pretrained(base_id, torch_dtype="auto", device_map="auto")
model = PeftModel.from_pretrained(model, adapter_id)

Related Artifacts

The companion synergy Q&A dataset is published at:

• https://huggingface.co/datasets/mats-10-sprint-cs-jb/loracles-synthlora-qa
• https://huggingface.co/collections/mats-10-sprint-cs-jb/loracles-synthlora

Limits

• The adapter is narrow by design; it is not meant to replace the base model.
• Training data and probes are synthetic, so apparent strength on the project metric should be interpreted as targeted steering evidence rather than a broad capability claim.
• Tier 4 adapters encode preferences, not facts. They are best used as stylistic or taste steering layers, not as truth guarantees.