Skip to content

Problem Solving Environment

Jump to bottom
Alex edited this page Jun 4, 2020 · 3 revisions

Goal: have an extendible library with a REPL interface to help answer scientific questions.

This is intentionally vague since I don't really know what to include under the rubric "scientific questions" (I'm thinking of physics, chemistry, biology, climate science, etc.).

"Answering questions" is also vague. How much AI is involved? Is this a full-blown Jaynesian robot, or just something along the lines of Mathematica?

Language Used

Since the scope of such a project remains vague, a Lisp seems well suited to the task. After much deliberation, I've boiled it down to Common Lisp, or possibly a Scheme suited to extensible software (e.g., Guile).

I'm starting with Common Lisp (since its macros are more powerful).

Similar Work

I was impressed with Gordon Novak's ISAAC and his online physics solver (c.f., source code). Something along these lines would be ideal.

Gerald Jay Sussman and Jack Wisdom's Structure and Interpretation of Classical Mechanics is another inspiration. The scmutils library synthesizes elements of symbolic computation with numerical analysis, something I would like to emulate (if possible).

Refining the Problem Statement

We need to introduce some technical terms, whose meaning are mildly vague:

  • A Problem Solving Environment (or PSE) is an interactive computer system (or software) which helps the user answer a specific class of problems (e.g., problems related to PDEs; Matlab has been thought of as a problem solving environment for linear algebra, though I would argue it wasn't quite there yet)
  • A PSE Framework (or Problem Solving Environment Framework) is the means to create a problem solving environment.

I suppose I am thinking about a problem solving environment framework as an extensible programming language.

Ideally, I would like to do things like ask my system to model the temperature of the Earth due to the Sun symbolically, and provide formal proofs the symbolic reasoning is correct. That is to say, there is a way to verify the CAS module using a formal theorem prover (of some kind), there is a knowledge-base of physics sufficient to construct the equations relating the Sun's radiance to the temperature of the Earth, and some experimental data to plug in values for the distance of the Earth to the Sun, etc.

It would be nice to ask our assistant if a given differential equation was stiff or not.

Example Problems

  • Solve equations algebraically
  • (Novak) Write a function (solveqns eqns vals v) that attempts to solve the list of equations eqns for variable v given an association list of values vals.
    1. If the desired variable v has a value defined in vals, the problem is solved, and the value can be returned.
    2. Otherwise, look through the list of equations to see if there is an equation that has exactly one unknown. If so, the equation can be solved for that variable using solve, and the value of the variable can be found using myevalb with vals. Add the new variable and value to vals and call solveqns recursively to try again.
    3. If all the equations have been examined and none of them can be solved, return nil.
  • Give me the trajectory of the Earth around the Sun
    • Give me the trajectory of the Moon around the Earth, in the Sun's frame

"Correct" Answers

Goal: I really want to get "the right answer", even if using Eulerian means (e.g., (sum n (n 1 infinity)) == -1/12 is permissible).

Unit testing is a great way to make sure I don't break anything. Similarly, pre-conditions and post-conditions are useful to make sure I'm documenting my assumptions.

Theorem Proving Capabilities

I'm on the fence about this, since it seems like a bit of a stretch. Or, more precisely, it's short term pain for long-term gain.

ACL2 formalizes a subset of Common Lisp. This does not include higher-order functions or CLOS, so we may be in a bit of a tight spot here.

Toy LCF

A simple LCF style prover seems feasible. My intuition would be to use a CLOS class for theorems. Formulas would be represented by CLOS classes? Something like

(defclass formula ()
  )
(defclass conjunction (formula)
  (clauses :init nil))
...

Goals are list of formulas left to be proven. Tactics transform goals.

Problem: I would then need to formalize floating point arithmetic in this newfangled LCF prover.

It would be nice to have something like Snark, with defclass hooked into registering a new Snark sort...

Math Subtlety

Physics works within the complex numbers implicitly. Branch cuts need to be handled properly.

References

Common Lisp

AI

Random stuff

  • Tailin Wu (MIT), Max Tegmark (MIT), "Toward an AI Physicist for Unsupervised Learning". arXiv:1810.10525
  • Jeff Clune, "AI-GAs: AI-generating algorithms, an alternate paradigm for producing general artificial intelligence". arXiv:1905.10985
Clone this wiki locally