Language models write small neural policies—and model checking tests their promises

Writing weights instead of training them

A neural-network policy is a rule for choosing an action from the current situation. Its weights determine how inputs, such as position and remaining fuel, become action scores. Conventionally, those weights are adjusted through training. Here, a language model writes them directly as numbers—a process called weight-space programming.

The language model receives a formal description of the environment, a behavioral requirement, and the network’s architecture. It then supplies every weight, explanatory notes, and example situations with intended actions. No gradient descent is used to create or repair these policy networks. That does not mean the language models themselves were never trained; the experiment concerns how they produce a separate, smaller network.

Checking behavior, not just examples

The environments are represented as Markov decision processes: models that specify available actions and the probabilities of subsequent states. Requirements are written in probabilistic computation tree logic, or PCTL, which can express both eventual success and conditions that must remain true along the way.

The pipeline first checks whether the generated numbers have the right shapes and whether the network makes the decisions its author intended on sample states. An optional second stage asks the language model to edit weights using a dataset of optimal actions computed by the model checker Storm.

Finally, COOL-MC constructs the probabilistic system produced by following the policy, and Storm calculates the probability of meeting the requirement. Unlike estimating success from sampled simulations, this calculation analyzes the relevant modeled behavior, subject to numerical error. Failed requirements can trigger further weight edits and another check.

“Verified” here means that a returned policy has been checked—not that success is guaranteed. If the repair limit is reached, the pipeline returns its best checked policy even if that policy still violates the requirement. The conclusion also applies to the specified model and property, not automatically to a physical system.

Strong results on three small tasks

The study tested DeepSeek-V4-Pro and Kimi-K3.1-Pro on three environments: navigating a slippery frozen lake, completing taxi jobs while managing fuel, and reaching a capital target in a simplified stock market. Each model-task combination was run three times, giving 18 runs.

All 18 initially created policies reached the optimal success probability before optimal-action dataset repair or model-checking repair. The experiment counted results within 0.0001 of the computed optimum as successful. The reported optimum was approximately 0.822 for Frozen Lake and 1 for the other two tasks.

Action accuracy told a different story. Some transporter networks selected optimal actions in only about 39% of dataset states yet still achieved the optimal probability from the starting state. Errors in states the policy never visits need not affect that outcome. Dataset accuracy and task success therefore measure different things.

A safety failure hidden by high accuracy

A separate transporter experiment required completing two jobs without carrying a passenger with fewer than four fuel units before completion. All six runs ultimately produced policies with a reported satisfaction probability of 1.

One run showed why the final behavioral check mattered. Dataset repair increased action accuracy from 37.9% to 98.4%, but changed the safety requirement’s satisfaction probability from 1 to 0. One subsequent model-checking-guided repair restored it to 1. A high proportion of locally optimal decisions was therefore not a substitute for checking the complete requirement.

The study also tested the six final two-job transporter policies unchanged on three jobs. Four completed the extra job with probability 1; two had probability 0. The failing behavior occurred after the second job, beyond the endpoint covered by the original requirement.

What remains unproven

These are small experiments, not evidence of broadly reliable autonomous control. The largest tested model had 16,496 states, and networks had at most two hidden layers of 32 neurons. Writing larger networks is itself challenging: incorrect network shapes appeared in 32 of 67 DeepSeek answers and eight of 28 Kimi answers.

Only two language models, one generalization test, and one complex safety requirement were evaluated. Each configuration had three runs, cloud outputs could vary, and prior exposure to public benchmarks or related policies could not be excluded. Model-checking-guided repair was needed in only one of the 24 runs, leaving its reliability on harder failures largely untested.

The source is the November 8, 2026 arXiv preprint, version 1. Its central result is a limited demonstration: direct weight writing can produce effective small policies, while model checking can reveal consequential failures that action accuracy misses.