automating entry of derivations into the Physics Derivation Graph website

What would it take to integrate support for symbol detection and conversion to SymPy for a single step in a derivation?

1. user provides initial expression in Latex to web UI.
2. computer parses symbols and operators from Latex
3. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
4. computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
5. computer parses expression to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
6. if yes, continue; if no, go back to step 1 or provide corrections to AST.
7. user provides next expression in Latex
8. computer parses symbols and operators from Latex
9. if symbols match symbols used in this derivation, then associate with those; otherwise 
10. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
11. if computer had to search PDG database, then computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
12. computer parses expression from step 7 to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
13. computer uses brute force to check every inference rule using a CAS against the provided expressions to "guess" the inference rule. 
14. if valid inference rule is found, continue to next expression; if no valid inference rule is found, prompt user to provide inference rule.
15. Given the inference rule and associated expressions, use the CAS to verify the step.

OpenAI's process supervision for math problems and relevance to the Physics Derivation Graph

OpenAI just announced (see https://openai.com/research/improving-mathematical-reasoning-with-process-supervision) progress on solving math problems using process supervision during training.

The data on https://github.com/openai/prm800k/tree/main comes from https://github.com/hendrycks/math (which is for https://arxiv.org/pdf/2103.03874.pdf) and there are examples in that data which come from https://artofproblemsolving.com/wiki/index.php/2015_AIME_II_Problems/Problem_6

AoPS describes itself as "Math texts, online classes, and more for students in grades 5-12."

The problems are constrained and feel very artificial. See for example https://artofproblemsolving.com/wiki/index.php/Mock_AIME_1_Pre_2005_Problems/Problem_4

The training data doesn't have inference rules, so the output from the LLM doesn't have inference rules. As a consequence, the output of the LLM cannot be confirmed by a Computer Algebra System. The output text needs to be validated by a human. LLMs are hallucinating answers that sound reasonable, so checking each step is still vital. 

The ability to resolve distinct variables across all of Mathematical Physics is beyond the scope of the training data. 

On a positive note, if the Physics Derivation Graph content existed, I now think an LLM-based approach could be used to make progress in Mathematical Physics.

improving efficiency of manually entered content

One of the major barriers to growth for the Physics Derivation Graph will be manual entry of expressions in support of derivations. Reducing "minor" inconveniences and adding "minor" help features can improve the user experience, the consistency of content, and the throughput of content creation.

As an example, for a given step in a derivation the user will need to specify the inference rule. Manually typing the name is laborious and induces cognitive burden. An "autocomplete" feature reduces labor but still requires thinking. A dropdown menu of all possible inference rules could be used, but a reduction to a dropdown with only relevant inference rules is better.

Similarly for manually entering expressions, autocompletion is helpful. Being able to specify which expression that has been previously entered is better.

A drag-and-drop interface for connecting nodes in the graph would be ideal.