Open
Conversation
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarified the definition of L in the Broadcast signature, specifying that L cannot be equal to 2^31-1. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarify the conditions for tensor broadcasting in the documentation. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarified the description of tensor data access in broadcasting conditions. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarify the explanation of data access for output tensor dimensions. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Updated error statement to reference Numpy broadcasting rules. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
…ing-groups into ericjenn-srpwg-wg1
Updated Airbus' use case. Signed-off-by: Jean Souyris <jean.souyris@airbus.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarified terminology for formalization levels in SONNX. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarified terminology for operator formalization levels. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Added a note to define the concept of mathematical construct. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarified the definition of tensors and their representation, emphasizing valid coordinate access. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Clarify the proposal regarding function signatures and contracts. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
…ing-groups into ericjenn-srpwg-wg1
Review by Edoardo Signed-off-by: emanino <40175301+emanino@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
…broadcast.md Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Refactored broadcast functions to use a list of tensors as input and output. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
### What has been implemented
- Abstract specification (OPTanh)
- Defined an abstract exponential function `exp_r` to model the mathematical behavior of the exponential.
- Specified `tanh_r` using three equivalent mathematical formulations:
- (exp(x) - exp(-x)) / (exp(x) + exp(-x))
- (exp(2x) - 1) / (exp(2x) + 1)
- (1 - exp(-2x)) / (1 + exp(-2x))
- Ensured consistency with the informal ONNX specification at the mathematical level.
- Implemented `dtanh` to apply tanh element-wise over tensor data.
- Defined `optanh` to construct the resulting tensor while preserving shape and background.
- Concrete implementation (CTensorTanh)
- Introduced `ctanh` as the floating-point implementation of tanh, formally linked to `tanh_r`.
- Implemented `ctensor_tanh` as a loop over the flattened tensor memory.
- Maintained a loop invariant ensuring correctness of partial computation.
- Proved that the final tensor matches the abstract specification (`optanh`).
- Formal verification
- All verification conditions are successfully discharged using Why3.
- The implementation is formally proven to be consistent with the abstract specification.
### Correspondence with the informal specification
- Element-wise application of tanh over the tensor is fully respected.
- Shape preservation constraint is enforced (`result ~= input`).
- Mathematical definition of tanh is captured via multiple equivalent formulations.
- No error conditions are required, consistent with the informal specification.
### Limitations / Remaining work
- ⚠ The exponential function `exp_r` is abstract and not tied to a concrete implementation.
- ⚠ IEEE-754 floating-point semantics (NaN, ±inf handling) are not explicitly modeled.
- ⚠ Numerical accuracy aspects (error propagation and introduction) described in the informal spec are not formally encoded.
- ⚠ No formal link yet between `ctanh` and an actual C math library implementation (e.g., `tanh` from `<math.h>`).
Signed-off-by: HamzaSeyfu <165190579+HamzaSeyfu@users.noreply.github.com>
…ing-groups into ericjenn-srpwg-wg1
…ing-groups into ericjenn-srpwg-wg1
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
11 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.
Update of the SONNX working group material (located under directory "safety-related-profile")