Conversation
…and first prototype fbarebone algorithm is ready, but it has to be further improved its performance.
…n in common_solving
`deduce` updates one output neuron of a ReLU layer, one thread per neuron:
* STEP 1 accumulates the pre-activation over the previous layer, bound by
bound with outward rounding;
* STEP 2 adds the bias, applies the ReLU and merges the result into the
neuron;
* STEP 3 propagates backward to the neurons of the previous layer.
STEP 3 recovers the sum of the other terms by undoing the addition of STEP 1
bound by bound, interval addition being separable. The interval subtraction
would pair opposite bounds and widen the result by the width of the term,
leaving nothing to propagate. That undo is only valid against the untouched
forward sum, hence STEP 2 uses the forward projection `add` rather than
`tell::fadd`, whose backward pass could narrow it.
The weights are now stored column-major, so that the threads of a warp, which
differ only by the output neuron, read consecutive floats instead of one row
each. `parse_network` packs them accordingly: the ONNX layout
[in_features, out_features] is already in that order, so only a transposed
matrix has to be rearranged.
A bot term is written to the store immediately, so that the solver observes
the failure and can stop.
Build:
* declare lala_interval outside of LOCAL_DEPS, FetchContent_MakeAvailable
already required it, so a non-local build failed on an undeclared
dependency. It is tracked by branch, the repository has no tag yet;
* point ort_gpu at libonnxruntime.so.1.19.2, the shipped tree has no
unversioned symlink;
* give the header its own include guard, it was shadowing the one of
fbarebones_dive_and_solve.hpp.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`deduce` took a composite index packing the layer in the top 8 bits and the neuron in the low 24. It now takes the target neuron directly: `i` ranges over `[0, num_deductions())` and updates `neurons[acc_layers[1] + i]`, one deduction per neuron outside of the input layer, so the index the fixpoint engine hands out lands on a neuron without any decoding. The layer is recovered by scanning `acc_layers` for the last layer starting at or before the target. That scan is the loop that already accumulated the weight offset, hence locating the layer is free: the previous version paid the same loop plus the unpacking. Two simplifications follow: the bias of the target sits at `acc_layers[0] + i`, `biases` being ordered like the deduction space, and the store is addressed by `target` instead of `out_base + j`. The 8-bit layer field also stopped limiting the network to 256 layers and 16M neurons per layer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains the following changes:
onnx_parserandvnnlib_parser.