Encrypted machine learning
We’re building systems that learn and answer questions while their memory stays encrypted, with cryptographic proofs that let others check the work.
18 projects and experiments
to answer across eight categories
The latest prototype sorts software issues into categories. You can teach it new examples, ask questions, and restart it without losing its memory. Each category keeps its eight most recent examples. A complete nine-category run included 18 teachings, three questions and two old examples being replaced; the encrypted scores matched the ordinary calculation throughout.
for 12 teachings, four questions and a restart
Encryption and proof systems often use different arithmetic, which makes checking the work expensive. We built a proof system using the same arithmetic as the encryption. It completes a two-category learning session with 3,200 proofs checked. Verification is still slower than simply repeating this small encrypted computation.
for one complete nonlinear calculation
We repaired a bug that left the final row of a calculation unchecked. The corrected version proves a complete encrypted similarity calculation, including multiplication and rescaling. A more compact way to check number ranges reduces proof size by 8.19%; total proving time improves by 1.69%, with higher memory use.
An earlier prototype connected new text examples to encrypted model updates and answers. Two teachings and two category answers completed in 21.20 seconds. Later work found a missing final-row check in its proof generator; the corrected implementation is used by the current learner.
One proposed design gave the software a key for adding new memories. Our calculation showed that combining that key with the answer keys would reveal all 576 changing coordinates of the model. That design needs a different way to add memories before it can protect them from its host.
A verifier checks a large computation by sampling parts of a mathematical encoding. We connected its batching and folding calculations to a Lean theorem about the probability of accepting an invalid proof. The theorem assumes fresh independent randomness; connecting that assumption to the implemented hash-based transcript is further work.
We developed a theoretical design in which each step certifies the next private state and the answer it may release. It can track that ancestry without an online registry. It depends on program obfuscation, erased setup secrets and a preset number of steps. An efficient implementation is still missing.
answers matched
A small model processed 384 updates and replaced 256 old examples while encrypted. All 96 numerical answers matched the ordinary calculation, and 28 of 32 final category predictions were correct. The encrypted run took about 3 minutes 40 seconds.
correct across 8,192 synthetic cases
A small learner used features from the SmolLM3 language model to adapt to recent examples. It reached 91.1% accuracy, compared with 51.0% using the original features. These tests used synthetic texts and histories. The language model that produced the features ran outside encryption.
A functional-encryption prototype gives each recipient keys for a fixed set of questions. It completed 384 updates and 96 queries, with all numerical answers matching the reference. Those keys still work on old inputs and outside the application, so deleting an example from the model does not revoke access to it.
This prototype creates the public setup without generating a central secret key. It completed 40 updates, four queries and eight replacements, and reopened the same saved history. It requires honest setup and separately registered recipients. Each recipient still has keys for its fixed set of questions.
384 updates and 96 queries
We ran a nonlinear learning rule under TFHE encryption, using an execution schedule generated from Lean. A second process repeated every operation and produced identical encrypted bytes. Decrypting the results also gave the expected states and answers.
An older encrypted runtime produced different ciphertext bytes on its fourteenth repeated update, despite receiving the same inputs. The replacement runtime uses a fixed plan for its numerical transforms and passes that case and four others. The later 480-operation run uses this approach.
The proposed Lean package covers learning arithmetic, execution schedules and parts of the cryptographic verifier across 72 modules. Lean checks the mathematical proofs mechanically. The package is available as a patch for the companion proof-system repository; connecting these theorems to the full native implementation remains work to do.
The verifier samples a mathematical encoding instead of checking every step. Its chance of missing an error depends on the number of samples and the error-correcting model. The technical note compares those models and explains why an earlier security estimate was withdrawn.
in a functional-encryption design
Functional encryption can let a key reveal a selected result without revealing the input. We use it in a two-step design where each private computation prepares an encrypted state for the next. The steps are set up backwards, so each knows how to encrypt for its successor. This requires the future steps to be planned and the setup secrets erased.
The goal is an AI that can keep learning and communicating while the person running it has no key that opens all of its memory. The remaining keys must allow only the intended operations. This is stronger than storing an encrypted file: the protection has to survive new inputs, new answers and copies of old state.
per ciphertext in one sizing calculation
We studied a lattice-based functional-encryption design intended to resist quantum attacks. One sizing calculation gives about 84 MB per encrypted input and 86 GB of public matrices. Those estimates depend on unresolved construction constants; they show where the storage cost comes from and what needs to shrink before implementation.
Try another word or choose a different topic.
How can someone check an answer?
Cryptographic proofs let a computer show that it followed a particular calculation. These notes cover the verifier and the cost of proving encrypted work.
View projectCan the model keep changing?
Follow new examples into an encrypted model, then see how it answers questions and replaces old memories.
View projectWho can read the model’s memory?
We want an AI to learn and communicate without giving its host unrestricted access to its internal state.
View projectOur current encrypted learner still has a key that can decrypt its whole memory. The application checks proofs before using that key, but the person holding it can bypass the application.
We want to replace that key with the ability to learn and answer only. That would let an AI keep private internal state even from the person running its computer. Finding a practical way to do this is a central part of the project.