Press Release by FormalFoundry.ai with e-Orzecznik.pl
Today, FormalFoundry.ai (FFai), a developer of formalization tools for use with large language models (LLMs), and e-Orzecznik.pl (e-O), a prominent provider of SaaS tools for occupational physician practices in Poland, have announced the development of a joint strategic initiative: to augment occupational medical procedures through the use of AI. The focal point of this collaboration is to integrate FFai’s LLM safety approach with e-O’s programming techniques and procedures, in order to increase the efficiency of the customer documentation workflow generation process, which in occupational medicine in Poland is a legal requirement.
The field of occupational medicine in Poland is complex. It features a large and ever increasing number of medical procedures and corresponding complex legal forms. This has presented the e-O team with a difficult challenge over the past 5 years of continuing development. To manage this, e-O used a Domain Specific Language (DSL). The DSL has helped to abstract the complexity from the number of different procedures. Even with its DSL, the team still encounters complexity in creating procedures, so there is room for even better performance.
This type of environment creates exactly the kind of challenge FFai AI safety tools are designed to address, and is the reason for this strong collaboration. The FFai team has a high degree of confidence that the techniques will help solve the issues e-O is continuing to experience.
The program of collaboration has been divided into 5 steps:
- Identify a set of areas for applying AI in the e-O software process (Complete)
- Formalize the e-O development process for the set (Underway)
- Verify the formalized systems (Upcoming)
- Assess new system performance (Upcoming)
- Enable seamless integration and adoption across the e-O customer base (Planned)
Step One: Identify a set of areas for applying AI in the e-Orzecznik software process (Complete)
In this phase, FFai worked alongside e-O to identify the areas within their workflow development process that could benefit from the augmentation provided by AI-based automated development tools. This phase revealed a set of specific areas for us to apply our solutions. With this groundwork phase successfully completed last month, we have already moved on to Step 2.
Step Two: Formalize the e-Orzecznik development process for the set (Underway)
We are currently in the process of “formalizing” the systems for the identified areas within e-O. In computer science and programming, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. Formalization in software design is motivated by the expectation that performing appropriate analysis in-line can contribute to the reliability and robustness of the architecture of a system.
In the e-O use cases we are formalizing the software solutions architected for existing and new forms related to evolving medical procedures. Since the software development is ongoing, and since the interactive forms and procedures are particular to the clinics and doctors themselves, the software is constantly evolving in an active process. If mistakes in software design can be rooted out in-process, then greater programming efficiency can be achieved overall and e-O and their clients will experience gains in efficiency.
Our solution uses proof assistants; the computer software language, Agda; and, of course, large language models (LLMs). Proof assistants are also called “interactive theorem provers”. They are a software tool that assists with the development of formal proofs through human-machine collaboration. Using proof assistants we are transforming the identified workflow areas into systems that generate formally verified system outputs. This will increase the efficiency of the important set of areas we have chosen to focus on with e-O.
Step Three: Verify the formalized systems (Upcoming)
In this phase we implement the in-line formalization process for the areas identified and covered in the program. For e-O, enhancing the reliability of the platform and the efficiency of its development team as they conquer the changing occupational medicine landscape is paramount. The future of occupational medicine is reliant on accurate digitizing from interactive forms generated on the fly in the clinics e-O services. Verifiable accuracy of input forms is of paramount importance as automation progresses across multiple systems. Mistakes are not only costly, but highly inconvenient to doctors and patients and inhibiting to the healing process.
We (FormalFoundry.ai and e-Orzecznik.pl) hope this collaboration will help better service e-O’s client base in Poland. e-O already serves a significant, 2 digit percentage of the Polish occupational medicine market for platform form generation and management. We think these new tools will most certainly provide a competitive edge. We also hope the FFai/e-O collaboration will surface additional opportunities for e-O to expand their expertise and business internationally.
Step Four: Assess new system performance (Upcoming)
In this analytical stage, we plan to conduct rigorous tests. Using an assortment of problems related to workflows in occupational medical procedures, we will probe and gauge the overall performance of the developed tool’s functionality and efficiency in the initial set, and additional areas. The complexity of the workflows in e-O’s systems and their domain-specific knowledge offers a rich space for these evaluations. This part of the work will validate the AI’s proof-generating performance, as well as the effectiveness of the formal verification systems n enhancing the safety and correctness of the e-O software outputs.
Step Five: Enable seamless integration and adoption across the e-Orzecznik customer base (Planned)
With enhanced insights gained from the previous stages, our goal is to devise an intuitive interface that enables e-O’s developers to incorporate AI-powered, formal verification tools into their routine development processes, seamlessly. By ensuring that our solution is easy to use and understand, we strive to make the process of creating, updating, and upgrading occupational medical legal procedures in Poland more manageable, efficient, and accurate for the e-O team. This, in turn, will contribute to safer, more powerful AI applications on e-O’s platform, and will be a part of the initial commercialization of the FFai tools.
In medicine and infrastructure and transportation and an expansive variety of applications in research and industry, LLM performance safety is of paramount and increasing importance. We consider AI safety to be a global community issue. As people, we have set aside other priorities to focus on building AI safety tools.
Real challenges for safety critical domains
For safety concerns this project’s immediate scope is focused only on enhancing e-O’s internal development tools. The project scope does not involve any direct interaction between deployed AIs and patient data. The LLMs used in this project aqre strictly focused on improving the process of rapidly programming varying medical-legal workflows for practitioners.
At FormalFoundry.ai, our aim is to establish a fully-functional proof-assistant framework, specifically for high-dependability systems or computationally heavy workloads. As we progress towards this goal, we invite you to join us. Follow our journey as we blend AI and formal methods together to create safer and more efficient processes that provide greater integrity and accountability for all involved. And, we are not alone. Find out more on our site and please take a moment to help us with a like for this article.