Formal Verification of Programming by Demonstration Systems

Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are acceptable in casual environments, but critical systems cannot make the same exchange. The software systems that NASA develops could greatly benefit from machine learning technologies that have been applied to casual computing, if the software developed by learning algorithms could be verified. We propose to apply formal methods to machine learning, and specifically Programming by Demonstration (PBD). The existing technology readiness level is very low: no known verifiable PBD systems have been deployed and the existing research in the area is limited. The Phase I effort will result in publications and a prototype implementation of a verifiable PBD system using SMT solvers. Phase II will build on Phase I publications and prototypes to demonstrate increased verification capabilities through the application of more complex formal methods, such as model checking. Verifiable machine learning would allow for trainable systems that meet critical properties, but are still adaptable to specific use cases. Such tools could be re-purposed for multiple applications without incurring the development costs associated with manual automation techniques today.

Machine learning and automation tools extend into all industries, bringing about improved human-computer interactions through per-user and per-task customization. While many tools have already been applied to casual computer use, there are myriad domains that have yet to adopt learning techniques because of the absence of behavioral guarantees. For example, reliable human review to ensure information assurance, remote piloting of UAVs, and even system administration tasks all require high levels of reliability, yet these tasks are also rife with meticulous and error-prone tasks that currently must be performed by trained experts. Formally verified learning tools will be able to address these needs without increasing the risk associated with automation today.

Crew-facing tools, remote control systems, and stored procedure authoring could all benefit from the capabilities offered by programming by demonstration and machine learning. Enabling these technologies to be applied safely will open up many opportunities at NASA for application re-use and productivity improvements through customization and fast, robust, macro/procedure creation. Improving automation in these areas will allow for more complex stored procedures to be used on un-manned craft and manned craft can take advantage of greater robustness through increasingly complex automatic navigation. Customization benefits will enable astronauts and remote operators to train general purpose tools (such as robotic arms) to perform complex repetitive operations at the press of a button simply by demonstrating the task a few times. These technologies have the potential to greatly increase the speed and reliability of NASA mission control, sample collection, and repair work.

This is early/mid-stage (TRL 3) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.