catalyst icon indicating copy to clipboard operation
catalyst copied to clipboard

[Frontend] Program verification

Open sergei-mironov opened this issue 1 year ago • 1 comments

Context: Having a proper encoding for the device capabilites, we implement the main part of program verification in this PR.

Description of the Change:

[sc-60648]

  • [x] Verify that no MCM (measure op) is present in the call
  • [ ] Verify that no callbacks are present in the call tree (future: verify that callbacks have custom vjp or are io callbacks)
  • [x] Verify that no state or variance is returned from the QNode. (Double check if Lightning Adjoint supports this!)
  • [x] adjoint diff method: Does the Tape only contain operations deemed differentiable by the QJITDevice from the TOML spec?
  • [x] parameter-shit method: Does the Tape only contain operations that support the 2-term parameter shift rule?

Benefits:

Possible Drawbacks:

Related GitHub Issues:

The following PRs need to be merged before this one:

  • https://github.com/PennyLaneAI/catalyst/pull/609 Introduces device capabilities.
  • https://github.com/PennyLaneAI/catalyst/pull/712 Makes toml-independent tests possible.

[sc-55558]

sergei-mironov avatar Mar 22 '24 08:03 sergei-mironov

Hi Lillian, thanks for the review. Here are my comments:

As a separate note, I think it might be cleaner to move this inside decomposition instead of having it occur afterwards, i.e. in decomposition you check if things are compatible, try to fix them if they aren't, and raise an error if you can't. If decomposition includes all these checks, it will either error out (validation succeeded) or fix things and pass (validation succeeded). It will keep similar logic together and prevent iterating over the tapes many times.

I think that the verification must be hard-run to happen after all the transformations because its most valuable feature is the ability to catch invalid transformations.

Saying that, I also agree that the actual function used for the verification might be the same as we use for decomposition so I would be glad to merge them at some point. We need to pay attention to the nested tape case. As far as I know, PL did not offer its support.

sergei-mironov avatar May 21 '24 11:05 sergei-mironov

I can see the motivation for doing a separate validation after all the decomposition - I think if we structure things correctly, its not necessary, but keeping validation separate is a safer choice that doesn't require us to not make any mistakes, so I'm happy with that. I would still like these things to be transforms inside of preprocess. As you said above:

We need to pay attention to the nested tape case. As far as I know, PL did not offer its support.

I think this is the main blocker here. Let me take a quick look at this and see if we can easily extend it either directly in PL or in catalyst.

lillian542 avatar May 21 '24 16:05 lillian542

Hello. You may have forgotten to update the changelog! Please edit doc/changelog.md on your branch with:

  • A one-to-two sentence description of the change. You may include a small working example for new features.
  • A link back to this PR.
  • Your name (or GitHub username) in the contributors section.

github-actions[bot] avatar May 22 '24 11:05 github-actions[bot]