Speaking to Silicon: Neural Communication with Bitcoin Mining ASICs

AI summary

Overview

Research area: Neuromorphic/thermodynamic computing applied to cryptocurrency mining hardware, combined with machine-checked mathematics (Lean 4 / Mathlib formal verification). Submitted under cs.NE.

Technical level: Advanced. The paper assumes familiarity with reservoir computing, information theory (entropy, KL divergence, mutual information), SHA-256 internals, mining pool protocols, and interactive theorem proving.

Scope: A single research memoria arguing that obsolete Bitcoin mining ASICs can act as physical reservoir computers whose timing jitter encodes exploitable information about SHA-256 computation, with the core claims formalized and verified in Lean 4.

What This Paper Is About

Bitcoin mining ASICs perform enormous numbers of SHA-256 hashes, and the paper states that 99.99% of those computations fail while consuming full energy, with additional waste from network latency. The authors ask whether timing jitter, thermal variation, and other thermodynamic side effects of the silicon can be measured to predict — early in a hash — whether it will fail, so the computation can be aborted, and whether that same signal can be used to read and write information to the chip. The claimed goal is to move from empirical observation to machine-verified proof that mining ASICs behave as "active conversational partners" rather than passive substrates.

Key Contributions

1. Reservoir computing on mining ASICs. Using a Single-Word Handshake (SWH) protocol that enforces one-to-one request/response correspondence with microsecond timestamps, the authors report NARMA-10 NRMSE of 0.8661, described as a 12.1% improvement over a constant baseline.
2. The Thermodynamic Probability Filter (TPF). A scheme that predicts SHA-256 hash failure from early-round thermodynamic signatures and aborts failing hashes. The paper reports a theoretical energy reduction of 92.19%, derived as 1 - 5/64 (abort after round k=5 of n=64), and 88.50% measured on Lucky Miner LV06 hardware with a reported 0% false abort rate.
3. A Lean 4 / Mathlib formalization by Richard (Apoth3osis). Reported as 21 Lean files, 3104 compilation jobs, zero errors, zero warnings under lake build --wfail, and zero sorry/admit statements, with Mathlib v4.24.0.
4. Vladimir Veselov's hierarchical number system theory and the Virtual Block Manager (VBM). Veselov's framing gives O(log N) energy scaling for structural encoding on mining ASICs (versus O(2^N) positional and O(N) SIMD), and VBM is reported to raise effective hashrate by +25% via local block template prefetching.

Main Findings

• Hardware universality: The frameworks were exercised on Antminer S9 (189 × BM1387, 14 TH/s, 1,300W, 16nm), Lucky Miner LV06 (1 × BM1366, 500 GH/s, 5nm), and Goldshell LB-Box (BM1366, 175 GH/s, ~162W, 5nm). The LV06 result was reported as replicated despite 15% WiFi packet loss.
• Edge-of-chaos operating regimes: Voltage/frequency/difficulty sweeps identified CV ≈ 0.092 as a "SYNC" state for reservoir computing and CV ≈ 0.586 as "OPTIMAL" for general thermodynamic sensing. The sweep covered 7.0V–8.5V in 0.2V steps, 200–600 MHz in 25 MHz steps, and difficulties from 1024 to 65536, with 10,000+ samples per configuration over 300-second windows.
• Benchmark comparison: Dialogue/SWH reached NRMSE 0.8661 (+12.1% vs constant), monologue 0.9550 (+7.6%), and constant serves as the 1.0000 reference. The reported 12.1% causality score is attributed to thermal inertia, capacitor charge state, and clock distribution dynamics.
• TPF classification: A 297-parameter MLP (3 inputs; 16→8→4 hidden; 2 outputs) reported 100% accuracy, precision, and recall, with confusion matrix [[23, 0], [0, 7]]. Digital Twin simulation gave 92.19% energy reduction and 0% false abort; LV06 hardware gave 88.50% and 0%, a 3.69% gap attributed to WiFi timing noise, thermal drift, and conservative safety margins.
• Virtual Block Manager: The Goldshell LB-Box rated at 175 GH/s was reported at 220 GH/s pool-reported rate through latency elimination.
• Algorithmic vs thermodynamic early abort: The paper states prior algorithmic approaches achieved 1–3% early-abort rates, while the thermodynamic approach achieves 88–92%, because timing jitter observes aggregate statistics rather than individual bit states blocked by SHA-256's avalanche property.
• Machine-verified theorems: Reported as proven are Independence ⇒ zero leakage (Silicon/Leakage.lean:90), Predictor beats baseline ⇒ not independent (Silicon/Predictability.lean:112), Energy savings ≤ 1 - k/n (Silicon/Cost.lean:61), leakage defined as mutual information I(S;O), and a PUF distinguishability witness (Silicon/PUF.lean). Note the paper gives differing theorem counts in different places: 5 core theorems in Table 12, and "15+ core theorems" in the codebase metrics table.
• Combined impact: With TPF at 88–92% and VBM at 25%, the paper's combined formula gives a theoretical maximum near 94% energy reduction, equivalent to a 16× effective hashrate multiplier; TPF alone corresponds to a 12.8× hashrate multiplier. Applied to the stated 150 TWh annual mining consumption, Edge Proxy standardization is projected to recover 2–4 TWh annually.

Methodology in Plain English

The authors treat each mining chip as a physical dynamical system. They wrote a proxy (the SWH protocol) that sends one job with a unique extranonce2 identifier, blocks until the response arrives, and records the elapsed time with microsecond precision. Those timing measurements, plus temperature and voltage, form a feature vector. Because different jobs take slightly different amounts of time depending on the chip's internal state, the authors train simple readouts — ridge regression (λ = 10^-6) for the NARMA-10 reservoir task, and a small MLP for hash-failure classification — on these features. They then sweep voltage, frequency, and difficulty to find operating points where the timing statistics are most informative. Separately, collaborators encoded the underlying information-theoretic claims (leakage, independence, predictability, energy bounds, PUF distinguishability) as Lean definitions and theorems so that a machine, not a human reviewer, checks every logical step.

Why This Matters

Research impact: The paper argues that formal verification plus hardware experiment is a stronger evidentiary standard than empirical-only hardware papers, and that thermodynamic side channels are a distinct information source from algorithmic bit-state analysis, which the avalanche property blocks. It positions obsolete ASICs as cheap, widely available, high-parallelism physical reservoirs for neuromorphic research.

Real-world applications (as described in the paper):

• Early-abort mining to cut SHA-256 energy waste, with claimed savings of 88.50% on LV06 and 92.19% theoretical.
• Virtual Block Manager prefetching to eliminate network latency idle time, reported as +25% effective hashrate on the Goldshell LB-Box.
• Physical Unclonable Functions: using timing signatures for device authentication without dedicated PUF circuits, via enrollment/challenge/response/verification.
• SiliconHealth: repurposing obsolete S9 units ($30–50) for medical record signatures, patient identity verification, and local AI inference, described as achieving 96% cost reduction versus GPU-based alternatives.

Industry relevance: The paper notes obsolete miners cost $30–60 per unit, and claims that if all miners adopted TPF, network energy consumption would drop by roughly 88% while relative hashrate, profitability, and 51%-attack cost remain unchanged. It also argues lower energy cost barriers improve geographic decentralization.

Future Directions

1. Formalize the SWH protocol mechanics — Stratum pipelining and timestamp extraction specifics are stated as not yet modeled.
2. Connect abstract prefix length to SHA-256 round indices — the formalization gap between the general prefix-prediction theorem and the concrete 64-round compression structure.
3. Model practical energy rates — incorporate false positive rates and safety keep rates into the formalized energy savings, rather than the idealized 1 - k/n bound.
4. Formally specify reservoir computing concepts — NARMA-10 benchmarks and "edge of chaos" are described but not formally specified, and a formal adversary model for the Proof-of-Processing threat model is listed as an optional extension.

Target Audience

This paper is best suited to researchers in neuromorphic and reservoir computing, hardware security and side-channel analysis, and formal verification (Lean/Mathlib practitioners). It is also relevant to Bitcoin mining engineers and mining-farm operators evaluating energy reduction, and to reviewers or reproducibility-focused researchers who want a case study in combining machine-checked proofs with physical hardware experiments. Readers without background in information theory or interactive theorem proving will find the formalization sections demanding.

Note: the provided paper content is truncated during the "Independent Review Certificate," so the final validation statements from that certificate are not available to summarize.

Authors’ abstract

This definitive research memoria presents a comprehensive, mathematically verified paradigm for neural communication with Bitcoin mining Application-Specific Integrated Circuits (ASICs), integrating five complementary frameworks: thermodynamic reservoir computing, hierarchical number system theory, algorithmic analysis, network latency optimization, and machine-checked mathematical formalization. We establish that obsolete cryptocurrency mining hardware exhibits emergent computational properties enabling bidirectional information exchange between AI systems and silicon substrates. The research program demonstrates: (1) reservoir computing with NARMA-10 Normalized Root Mean Square Error (NRMSE) of 0.8661; (2) the Thermodynamic Probability Filter (TPF) achieving 92.19% theoretical energy reduction; (3) the Virtual Block Manager achieving +25% effective hashrate; and (4) hardware universality across multiple ASIC families including Antminer S9, Lucky Miner LV06, and Goldshell LB-Box. A significant contribution is the machine-checked mathematical formalization using Lean 4 and Mathlib, providing unambiguous definitions, machine-verified theorems, and reviewer-proof claims. Key theorems proven include: independence implies zero leakage, predictor beats baseline implies non-independence (the logical core of TPF), energy savings theoretical maximum, and Physical Unclonable Function (PUF) distinguishability witnesses. Vladimir Veselov's hierarchical number system theory explains why early-round information contains predictive power. This work establishes a new paradigm: treating ASICs not as passive computational substrates but as active conversational partners whose thermodynamic state encodes exploitable computational information.