Skip to content

Add functional transcendentals + scalar-affine ops for scientific forward models#5

Open
NicolasRouquette wants to merge 2 commits into
lean-dojo:mainfrom
NicolasRouquette:functional-elementwise-transcendentals
Open

Add functional transcendentals + scalar-affine ops for scientific forward models#5
NicolasRouquette wants to merge 2 commits into
lean-dojo:mainfrom
NicolasRouquette:functional-elementwise-transcendentals

Conversation

@NicolasRouquette

@NicolasRouquette NicolasRouquette commented Jun 5, 2026

Copy link
Copy Markdown
Contributor

A small, single-purpose contribution: surface differentiable elementwise exp /
log and scalar-affine maps on the nn.functional API, so scientific forward
models — radiative transfer, dielectric mixing, kinetics, anything built from an
exp/log of an affine argument rather than from NN activations — can be written
as a pure autograd.fn1.Fn and differentiated by the autograd engine, with no
hand-coded gradient
.

Context

Independent and self-contained: this branch is based directly on main and does
not depend on the factorization PRs (#2 and its eig/SVD follow-up). The diff is 7
files, +254 lines.

The motivating use case is a soil-moisture retrieval that combines SMAP (Soil
Moisture Active Passive) and NISAR (NASA–ISRO Synthetic Aperture Radar)
observations through the AVS (Attenuation–Volume–Surface) model, whose surface
term is exp(-2·b·NDVI)·c·|R|². Operationally that model is fit per pixel with a
hand-coded analytic Jacobian (plus a byte-duplicated JIT copy). A sign or factor
error there does not crash anything — it silently degrades the fit, and the copies
can drift. The ops here let the forward model be written once and its gradient be
derived by autograd, making the hand-coded Jacobian redundant.

What's here

  • Functional ops (NN/Runtime/Autograd/TorchLean/Functional/Core.lean):
    F.{exp, log, scale, shift, affine} — thin lifts of the existing
    Ops.{exp, log, scale, const} primitives, which already carry registered
    backwards, so reverse-mode jacrev / grad works through them unchanged.
    affine x c k = c·x + k; scale / shift are the multiply / add-by-constant
    halves.
  • Public surface (NN/API/Public/NN/FunctionalBatch.lean,
    NN/API/Public/Seeded.lean): the five ops added to both nn.functional export
    bridges, beside square / mean.
  • Example + self-check (NN/Examples/Functional/Transcendentals.lean,
    lake exe transcendentals_check): differentiates exp, 3x+1, and exp(-2x)
    and compares the autograd gradient to the closed form. Positive controls plus a
    negative control — the autograd gradient of exp(-2x) is -2·e^{-2x} and the
    test rejects the wrong-sign +2·e^{-2x}, i.e. exactly the hand-coded-Jacobian
    defect class the ops are meant to eliminate. Exits non-zero on regression.
  • Blueprint (blueprint/.../Guide/Ch2_Frontend/ScientificForwardModels.lean):
    a short chapter documenting the ops and the autograd-derived-gradient point.

Notes for reviewers

  • The example links the toolchain libc++ at runtime (native autograd backend);
    run with LD_LIBRARY_PATH=<toolchain>/lib.
  • Nothing in Ops or the backends changes; this is purely additive on the
    functional surface.

@NicolasRouquette NicolasRouquette force-pushed the functional-elementwise-transcendentals branch from 3ee4e1e to 9179092 Compare June 6, 2026 18:11
@Robertboy18

Robertboy18 commented Jun 18, 2026

Copy link
Copy Markdown
Member

Thanks, this feature makes sense. Exposing exp, log, scale, shift, and affine on nn.functional is useful for scientific forward models, and the autograd-gradient example is a good motivation.

This PR needs to be refreshed against current main before review. TorchLean has had a large API refactor and Lean 4.31 upgrade since this branch was opened. In a temporary merge attempt, this PR conflicts in:

NN/API/Public/Seeded.lean

That file is now an import-only entrypoint, while this PR edits the old monolithic version directly. Please move the new functional exports into the appropriate current implementation module/Core file and keep entrypoints import-only.

A few concrete requests:

  1. Please rebase onto current main.

  2. Please remove the AI co-author trailer from the commit/PR metadata before this lands.

  3. Please make the new ops fit the current public API layout rather than restoring old API structure.

  4. Please rerun the relevant builds/tests after rebasing.

  5. Please document the domain behavior for log; it is fine to expose it, but users should not read it as a safe total log over arbitrary inputs.

Once this is rebased and fits the new layout, I’m happy to review the actual API/content.

@NicolasRouquette

Copy link
Copy Markdown
Contributor Author

OK, will do...

…ft/affine)

Surface differentiable elementwise exp/log and scalar-affine maps on the
nn.functional API, so scientific forward models (radiative transfer, dielectric
mixing, kinetics — built from exp/log of an affine argument rather than NN
activations) can be written as a pure autograd.fn1.Fn and differentiated by the
autograd engine, with no hand-coded gradient.

- F.{exp,log,scale,shift,affine} in Functional/Core.lean: thin lifts of the
  existing Ops.{exp,log,scale,const} primitives, which already carry registered
  backwards, so reverse-mode jacrev/grad works through them unchanged.
- Surfaced on nn.functional via both export bridges (FunctionalBatch + Seeded).
- Self-checking positive/negative example (NN/Examples/Functional/Transcendentals,
  `lake exe transcendentals_check`): autograd gradients of exp, 3x+1, and exp(-2x)
  match the closed form; a wrong-sign control is rejected.
- Blueprint chapter Ch2_Frontend/ScientificForwardModels.

Note: the example exe links the toolchain libc++ at runtime (native autograd
backend); set LD_LIBRARY_PATH to <toolchain>/lib accordingly.
@NicolasRouquette NicolasRouquette force-pushed the functional-elementwise-transcendentals branch from 9179092 to 740c3d9 Compare June 19, 2026 16:13
@NicolasRouquette

Copy link
Copy Markdown
Contributor Author

I verified on this rebased branch that ./scripts/checks/check.sh --ci-all runs without any issues.

@Robertboy18

Copy link
Copy Markdown
Member

Thanks, I re-checked this branch after the rebase.

The calculus examples look correct to me:

  • d/dx exp(x) = exp(x);
  • d/dx (3x + 1) = 3;
  • d/dx exp(-2x) = -2 exp(-2x).

The negative controls are useful too, especially the wrong-sign exp(-2x) check, because that is exactly the kind of sign/factor mistake this API helps avoid in hand-coded scientific Jacobians.

I only see documentation/API-cleanup items before merge:

  1. The top doc block still says #eval checkAll runs at build time. Later in the file it correctly says this is a compiled executable check through lake exe transcendentals_check, because native tape externs are not available through plain #eval. Please remove or update the stale #eval sentence so the file does not contradict itself.

  2. Please document the domain behavior of nn.functional.log more explicitly. The op is fine to expose, but mathematically it is the real natural log only on positive inputs. At the runtime/Float boundary, nonpositive inputs follow backend behavior such as nan/-inf rather than a safe total real-valued log. I would say something like: “For real-valued reasoning, assume positive inputs; Float behavior on nonpositive values follows the backend.”

  3. Please keep the implementation in the current API layout. This branch now mostly fits the refactored structure, but the important rule is: top-level API files stay import entrypoints, implementation lives in the relevant Core/module files.

No mathematical blocker from my side.

- Transcendentals example: fix stale top-block line that claimed `#eval
  checkAll` runs at build time. The checks run as a compiled executable
  (`lake exe transcendentals_check`), not via `#eval`, since the
  interpreter cannot load the native tape externs.
- nn.functional.log: document domain behavior. It is the real natural log
  only on positive inputs; for real-valued reasoning assume x > 0, and
  Float behavior on nonpositive values (nan/-inf) follows the backend.
  Mirror the same note into the blueprint's log bullet.

No mathematical/API-layout changes: implementations stay in
Functional/Core.lean, the API file remains a re-export entrypoint.
@Robertboy18

Robertboy18 commented Jun 23, 2026

Copy link
Copy Markdown
Member

One last merge-readiness cleanup from my side: the code/spec comments look addressed, and the focused build plus lake exe transcendentals_check passed locally.

But the PR description still ends with:

the old AI co-author trailer

Please remove that from the PR body before merge. TorchLean is academic work, and I want the public PR metadata/history to reflect the human authorship cleanly. AI assistance can be mentioned privately or in project notes if needed, but not as a co-author line in the PR text.

After that, I’m comfortable with this PR from my side.

@NicolasRouquette

Copy link
Copy Markdown
Contributor Author

Done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants