CryptoReasoner-20B-Graph-Proofs

Generate machine-checkable deduction sequences for small symbolic encryption scenarios. This GPT-OSS-20B adapter reads the initially known atoms, encrypted facts and target secret, then proposes a reachability claim and an ordered list of fact indices. The bundled deterministic kernel checks every step and the final closure.

Use it to benchmark proof construction or demonstrate how model-generated reasoning can be checked by a precise symbolic tool. The saved HF adapter produces valid certificates on 51.0% of 96 held-out cases versus 2.1% for the base; performance drops to 21.9% on unseen graph structures. It is a research proof generator for this finite abstraction, not a verifier of arbitrary real-world cryptographic protocols.

Application example

Show a checked two-step deduction. Start with k1; fact 0 reveals k2 using k1; fact 1 reveals secret using k2. A valid certificate is {"secret_unreachable": false, "steps": [0, 1]}. Generate a candidate, then run the independent checker before accepting it. The example below shows how to generate and validate a certificate for this scenario.

Adapter and inference

The adapter uses attention-only LoRA with original per-projection rank 32. Tinker attention module names were mapped to the Hugging Face attention module names. The Hugging Face job verified all 192 converted FP32 tensors after loading and matched every prompt token hash with the native fixture. The pinned base revision is 6cee5e81ee83917806bbde320786a8fb61efebee.

Install requirements.txt, download the repository's Python files, and use the complete synthetic case below. The measured setup used a NVIDIA A100-SXM4-80GB with BF16 base inference and FP32 adapter weights.

from proof import ProofPolicy
from crypto_compact_kernel import check

case = {
    "initial_known": ["k1"],
    "encrypted_facts": [["k2", "k1"], ["secret", "k2"]],
    "query_secret": "secret",
}

policy = ProofPolicy("itsalissonsilva/CryptoReasoner-20B-Graph-Proofs")
certificate = policy.generate([case])[0]["certificate"]
print(certificate)
print(check(case, certificate))  # Accept only a certificate the exact checker marks valid.

Evidence summary

Hugging Face evaluation on 96 matched held-out cases gave 51.0% valid certificate rate with the adapter and 2.1% with the base. The paired gain was +49.0 percentage points (95% group-bootstrap interval +35.4 to +61.5).

Held-out evaluation

The HF replay uses 16 complete case pairs per split, selected by a fixed salted group hash before HF inference. Both conditions use the same frozen prompts and decoding settings.

Split	Cases	Base	Adapter
All cases	96	2.1%	51.0%
Deeper graphs	32	3.1%	46.9%
Familiar distribution	32	3.1%	84.4%
Unseen graph structures	32	0.0%	21.9%

On the full native Tinker evaluation of 768 held-out cases, valid certificate rate went from 4.9% to 55.7%. On the same 96 cases selected for Hugging Face replay, native performance went from 3.1% to 53.1%.

Performance varies across graph families and depth. The bundled deterministic kernel independently checks generated certificates.

The frozen split, paired results, and conversion checks are in evaluation.json and fixture.json. The synthetic benchmark includes the source rows and deterministic labels. HF evaluation job.