Ericjenn srpwg wg1#119
Open
ericjenn wants to merge 1102 commits into
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>
…ing-groups into ericjenn-srpwg-wg1
Updated Airbus' use case. Signed-off-by: Jean Souyris <jean.souyris@airbus.com>
…nd add .ipynb for informal test
…thub) Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
… github Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
…thub Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
…thub Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
…thub Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
… github Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
Signed-off-by: HBelfy <182933819+HBelfy@users.noreply.github.com>
Signed-off-by: Eric JENN <158552155+ericjenn@users.noreply.github.com>
…r for exp operator
…ition de l'exponentiel en real et en cfloat (base de preuve OK, avec en dur 0.0 et 1.0 sans l'exponentiel)
MatMul added in Airbus' scope. Signed-off-by: Jean Souyris <jean.souyris@airbus.com>
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
Recommend the use of Why3 and suggest useful links for readers. Signed-off-by: JeanLoupFarges <86069696+JeanLoupFarges@users.noreply.github.com>
Signed-off-by: Jean Souyris <jean.souyris@airbus.com>
Add a formal Why3 specification for the Softmax operator based on the ONNX v13 behavior. This update introduces: - an abstract SoftmaxReal specification over real tensors; - an abstract SoftmaxFloat specification covering finite values, NaN, +inf and -inf cases; - the numerically stable formulation using M = max along the selected axis; - preservation of the input tensor shape in the output tensor; - axis validity constraints; - a concrete C-extractible CtensorSoftmax module; - a c_softmax kernel using the outer / axis_size / inner traversal scheme; - a Softmax extraction driver mapping the exponential operation to C exp(); - a Makefile workflow for proving the abstract specification and generating the C code. The abstract specification is proved successfully for SoftmaxReal and SoftmaxFloat. The concrete C module is extractible and generates ctensorsoftmax.c/.h with the c_softmax function. The generated C code compiles successfully. The full proof of the concrete C kernel is not completed yet. Remaining proof obligations mainly concern integer overflow, memory bounds and offset validity in the concrete tensor traversal. Signed-off-by: HamzaSeyfu <165190579+HamzaSeyfu@users.noreply.github.com>
…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")