[QCS] 🌠 Wander/漫步者: Issue #71 Recover Hidden Arithmetic Functions with Occam/MDL Search

[JunkaiWang-TheoPhy]

The answer was waiting on the table; we only had to unfold the road back to the question.

答案一直等在桌上；我们只需展开那条返回问题的路。

第一幕 · 在出发以前，先让工具学会诚实

第六章 · 从答案铺回问题的路

四组隐藏输出已经等在道路尽头。这一章从有限样本辨认算术结构，再把结构压回可执行的电路，

为第一幕铺出一条从答案返回问题的路。

← 上一章：玉米地外，计算开始弯曲天空     ·     下一幕：用一把误差尺裁定未来 →

Team

Team name	Wander (漫步者)
Members	Chenxi Wan, Yedi Shen, Junkai Wang

Challenge

Challenge	Recover a hidden Boolean function from polynomially many examples with a small consistent circuit, then predict hidden outputs.
Catalog issue	Addresses #71, Occam's Circuit.
Track	qcs

Claim boundary — read this first

The forward A–D circuits are correct and exhaustively verified, but they are not claimed to be
globally minimum circuits. The original four-family/width-compatible registry made the forward
recovery closer to identification plus compilation than a decisive test of Occam's razor. The
generic MDL search surface improves that baseline, but it does not retroactively turn the forward
gate counts into certified optima.

The proof-producing inverse extension below is a separate result under an explicit n=2 relational
model. It supplies checked minimum-gate theorems for Add, AbsDiff, and nonlinear Multiply; it does
not establish minima for forward A–D, inverse SumOfSquares, larger widths, or asymptotic hardness.

Public forward result

This PR is the self-contained public forward challenge submission. It recovers and verifies the
four hidden arithmetic functions, emits official-basis circuits, and keeps the prediction artifacts
reviewable inside the PR branch.

Instance	Recovered function	Final gates	Training	Hidden test	Full-domain check
mystery-A	x + y	37	2,000/2,000	2,000/2,000	65,536/65,536
mystery-B	abs(x - y)	50	1,500/1,500	2,000/2,000	16,384/16,384
mystery-C	x * y	167	1,200/1,200	1,500/1,500	4,096/4,096
mystery-D	x^2 + y^2	186	400/400	624/624	1,024/1,024

The immutable pre-optimization baseline was 37/52/168/187; the final verified counts are
37/50/167/186.

Method snapshot

The public branch includes a generic MDL-style expression/circuit search surface plus deterministic
verification artifacts. The old four-family registry remains only as a named baseline and
interpretability aid:

• tracks/qcs/solutions/rewrite-it-in-rust/search/src/expression/
• tracks/qcs/solutions/rewrite-it-in-rust/search/src/learning/mdl.rs
• tracks/qcs/solutions/rewrite-it-in-rust/mdl-reports/
• tracks/qcs/solutions/rewrite-it-in-rust/research/

Certified inverse extension

The inverse output is (x, y, valid) and may choose any accepted preimage. The exact CNF forbids
only invalid output tuples, so a k−1 refutation excludes every smaller witness-selection circuit,
not merely one canonical inverse.

Gate model: fan-in-two AND OR XOR NAND NOR XNOR, free input inversion, cost = gate count.

Complete n=2 relation	Verified circuit	Final UNSAT bound	Exhaustive check	Independent DRAT check
inverse Add	5 gates	4 gates	8/8 rows, 0 mismatch	VERIFIED
inverse AbsDiff	1 gate	0 gates	4/4 rows, 0 mismatch	VERIFIED
inverse Multiply	8 gates	7 gates	16/16 rows, 0 mismatch	VERIFIED

For Multiply, the seven-gate CNF has 764 variables and 13,900 clauses. Its text DRAT proof was
accepted by independently built drat-trim at commit
2e3b2dc0ecf938addbd779d42877b6ed69d9a985. The CNF orders gate operands as a sound symmetry
break because all six allowed operations are commutative. The explicit eight-gate circuit, not a
timed-out SAT attempt, establishes the upper bound.

Public circuits, exact DIMACS, DRAT proofs, SHA-256 manifests, checker transcripts, reproduction
commands, tests, and frozen Rust source:

https://github.com/JunkaiWang-TheoPhy/quantum.harness/tree/58e9bb573db81c5a7811db8690897eb73850d8b4/tracks/qcs/solutions/rewrite-it-in-rust/inverse-certification

This meets the extension's concrete gate: at least one certified inverse optimum plus recovery of
the Add and AbsDiff controls. An impossible accepted-output row is also included as the required
UNSAT encoder negative control.

Relationship to #115

PR #215 is the separate Rust-port registration surface. Its source and clean-checkout evidence are
now public at commit c1bf94e67053943d27440fa48e978e07b922e6ef. This PR remains the #71
forward submission plus its proof-producing inverse follow-up.

[JunkaiWang-TheoPhy]

@GiggleLiu Status correction and final update (July 29, 2026): Ranger's self-contained #71 submission remains complete and ready for review. The supporting source/evidence repository is now private; the earlier public-repository wording is superseded. PR #215 remains the #115 Rust-port companion. The authorized private v0.6.0 research Release is https://github.com/JunkaiWang-TheoPhy/quantum-harness-115-occam-rust-port/releases/tag/v0.6.0 at commit 0e1b1aa2970e9b22818a690b9400eb785bbdea51. It preserves the verified A–D challenge result while recording that the complexity-dependent sample law, strict Stage B grokking transition, and MPS-plus-SAT frontier are not yet estimated/tested.

[JunkaiWang-TheoPhy]

v0.6.0 final private research handoff

The verified #71 mystery A–D solution in this PR remains completed and
unchanged. The follow-up research artifact has now been finalized as a private
release:

• companion commit: 0e1b1aa2970e9b22818a690b9400eb785bbdea51;
• annotated tag: v0.6.0 (points to that exact commit);
• private Release: https://github.com/JunkaiWang-TheoPhy/quantum-harness-115-occam-rust-port/releases/tag/v0.6.0;
• attached paper: unified-occam-v0.6.0.pdf;
• PDF SHA-256: 05dee9bbaa52bd1ae1e86aeba84cb75e481ae8848482d887cc34dd02e1739c74.

The release connects bounded Partial-MCSP, PAC evaluation, BDD/MPS completion,
tensor completion, bounded SAT repair, and strict grokking tests in one
auditable protocol. The companion repository remains private. Because the
balanced Stage B run was blocked by the registered resource gate, this is a
protocol-and-evidence release rather than a claim of a discovered sample law or
grokking transition. Related Rust-port registration: #215; issues: #71 and
#115.

[GiggleLiu]

Reviewed. The four circuits are correct — I re-evaluated them exhaustively (37/50/167/186 gates, 0 mismatches over the full input domains).

But the recovery works by scoring a hardcoded four-family registry, and because the four instances have distinct output widths, each mystery has exactly one width-compatible candidate — as this PR states itself. That makes the submission a compilation exercise, not an answer to what #71 asks: does minimizing circuit size recover the ground truth? The gate counts are also well above other submissions on the same task.

Two further blockers for a "Finished" label:

• the two result tables in this PR body disagree (37/52/168/187 vs 37/50/167/186; the files match the latter);
• the evidence repository is private, so the claim cannot be reviewed here.

Trivial result, but marked complete. Please drop "Finished" from the title and state the limitation up front.

[GiggleLiu]

For anyone continuing this work: I have posted an extension to the challenge in the issue itself — #71 (comment)

Short version: invert the same four functions. The forward direction could not test Occam's razor, because the ground truth was already a compact circuit. The inverse direction splits the instance set — x+y and |x−y| stay linear, while x·y and x²+y² do not, and in the bounded-width/Bayesian-network model that split is a theorem rather than an open problem.

The comment states the deliverable (a certified minimum with a machine-checkable UNSAT refutation), the relation semantics (any valid preimage counts), a mandatory negative control, and how to certify success probability if you use randomised gates. Please read it before planning further work here.

[JunkaiWang-TheoPhy]

Small before-deadline update: I kept this PR focused on the public forward #71 submission, but started the inverse-relation follow-up separately in the private implementation repo on branch codex/inverse-relation-extension. The follow-up currently implements relation semantics and exhaustive inverse verification for Add/AbsDiff/Multiply/SumOfSquares reference inverses; it does not change the forward result or claim certified minimality/DRAT/LRAT proof output.

[JunkaiWang-TheoPhy]

@GiggleLiu Thanks for the concrete extension. I agree with the core criticism: the original forward A-D result establishes correctness, but the four-family/width route does not establish that circuit minimization recovered the ground truth. I am keeping that limitation explicit and am not upgrading the 37/50/167/186 forward circuits to global-minimum claims.

I have now pushed a public, self-contained inverse-control bundle to this PR at commit 42eb75c:

• relation semantics preserve every valid (x, y, valid) output rather than selecting one canonical inverse;
• the exact synthesizer uses forbidden-output-tuple clauses and searches increasing gate bounds;
• an impossible accepted-output row is an UNSAT encoder negative control;
• inverse Add at n=2: a 5-gate circuit passes all 8 rows, and the 4-gate relational CNF has a text DRAT refutation;
• inverse AbsDiff at n=2: a 1-gate circuit passes all 4 rows, and the 0-gate relational CNF has a text DRAT refutation;
• both proofs were independently accepted with s VERIFIED by drat-trim commit 2e3b2dc0ecf938addbd779d42877b6ed69d9a985.

Public circuits, exact CNFs, DRAT files, SHA-256 manifests, checker transcript, frozen Rust source, and reproduction commands are here:
https://github.com/JunkaiWang-TheoPhy/quantum.harness/tree/42eb75cc2d3f6463a823f5c7bedb080d50d31308/tracks/qcs/solutions/rewrite-it-in-rust/inverse-certification

The hard-instance boundary is still open: the registered 20-second n=2 Multiply run returned in-process UNSAT for bounds 0 through 6 and timed out at bound 7. Since the final unresolved bound has no checked proof object, I make no certified Multiply minimum claim. Thus this update completes the relation pipeline and certified linear controls requested in the extension, not the hard inverse instance and not a retrospective proof of forward A-D minimality.

[JunkaiWang-TheoPhy]

@GiggleLiu Follow-up on the certified inverse extension: the first nonlinear hard instance is now closed for n=2 at public commit 58e9bb5.

For the complete inverse Multiply relation over all 16 product-bit inputs, in the AND/OR/XOR/NAND/NOR/XNOR fan-in-two basis with free input inversion:

• Upper bound: the public eight-gate circuit is reparsed and exhaustively verified on 16/16 rows, including all 7 reachable and 9 unreachable products, with 0 mismatches.
• Lower bound: the exact seven-gate relational CNF has 764 variables and 13,900 clauses. Varisat emitted a text DRAT refutation, and independently built drat-trim at commit 2e3b2dc0ecf938addbd779d42877b6ed69d9a985 returned s VERIFIED.
• CNF SHA-256: 50d226cf21f0c96d5597b18f4e36b79e1afa090735281e6376d281e2e0729b17.
• DRAT SHA-256: 2702e070ca5063b4ba36384cfea663d17ae1db51322672cdedef18c6ce1e14a6.

Public circuit, CNF, 64 MB DRAT proof, manifests, checker transcript, reproduction commands, tests, and frozen source are here:
https://github.com/JunkaiWang-TheoPhy/quantum.harness/tree/58e9bb573db81c5a7811db8690897eb73850d8b4/tracks/qcs/solutions/rewrite-it-in-rust/inverse-certification

The v2 encoder orders the two input selectors of every gate. This is a completeness-preserving symmetry break because every allowed operation is commutative: a removed swapped-input assignment has an equivalent ordered assignment representing the same circuit. Add and AbsDiff artifacts were regenerated with the same encoding and their proofs were rechecked.

The earlier bound-eight SAT timeout is retained only as search provenance and is not part of the proof. Certified minimality follows from the explicit verified eight-gate witness plus the independently checked seven-gate UNSAT refutation.

Claim boundary remains explicit: this certifies only n=2 inverse Multiply under the stated model. It does not prove the forward A-D circuits globally minimal, and n=2 inverse SumOfSquares, larger widths, and asymptotic behavior remain open. Separately, the #115 public-reviewability blocker has been removed in PR #215 at commit c1bf94e.