Imandra logo - homepage link

Imandra gives AI the
power of reasoning

Large Language Models (LLMs) use Imandra to build mental models and reason about them, unlocking the incredible potential of generative AI for industries where correctness and compliance matter.

Get your LLM to express its thoughts in logic, then tap into automated logical reasoning to:

  • Eliminate hallucinations by making reasoning explicit and explainable
  • Gain trust and demonstrate compliance by formally verifying arguments and results
  • Scale reasoning to unseen depths with auditable logical inference
Get your LLM to express its thoughts in logic!

Watch our explainer video

Lots of exciting announcements soon, stay in touch:

Automated Reasoning is the logical complement to LLMs

  • Imandra empowers LLMs with automated logical reasoning at scale, turning opaque models into transparent ones, empowering users and developers to see assumptions and conclusions involved in responses with precise auditable reasoning.
  • Traditionally, these types of techniques were reserved to highly specialized teams of PhDs at places like NASA. Thanks to recent advances, Imandra is highly automated and scaled to most difficult industrial applications.
Automated reasoning is the logical complement to LLMs

The Imandra
Reasoning as a Service® Platform

Imandra is not your typical AI system!

  • Unlike the approaches of statistical AI (e.g. ChatGPT), Imandra:

    • relies on automated logical reasoning
    • converts input into mathematical logic
    • backs every answer or feedback with a sequence of logical steps that may be audited by an independent tool
  • Traditionally, these types of techniques were reserved to highly specialized teams of PhDs at places like NASA. Thanks to recent advances, Imandra is highly automated and scaled to most difficult industrial applications.
  • Imandra is already used today by leading financial firms to design, implement and calibrate complex financial systems, including national stock and derivatives exchanges. Outside of finance, our clients include US Air Force and DARPA.

Learn the Technical Details on our Imandra Core Page.

Learn more
Imandra Core Process

OCaml and Imandra Modeling Language (IML)

The input language to Imandra is OCaml, a powerful open source functional programming language. For its pure subset, we've created a formal semantics. We call this the Imandra Modeling Language (IML). Imandra's reasoning engine translates IML into mathematical logic and reasons about it.

As long as you can describe something logically or computationally, you can encode and reason about it in Imandra.

Whether it's a a computer program, a cap table, a spreadsheet, case law, a legal argument, financial regulations, a blueprint, tax code, a scheduling problem, ... all of these can be described and reasoned about in Imandra.

https://ocaml.org

Imandra Feature Spotlight:
Region Decomposition

  • What is it? Region Decomposition is a key and novel feature of Imandra for explaining the behavior of complex software and algorithms, and exhaustively identifying their edge cases.
  • Why is it novel? We have “lifted” a well-established mathematical technique (Cylindrical Algebraic Decomposition or CAD) to algorithms at large, and made significant investments into making it scale to industrial applications.
  • What’s the big deal? Regions are fundamental for explanations and generalizations. If a goal is false and Imandra computes a counterexample, it can be generalized into a region which explains why. Explainable generalizations are critical for the convergence of LLMs to correct results, closing off large regions of the search space instead of only eliminating single points.
Region Decomposition Diagram

Examples / Documentation

Other select
features

  • Formal Verification

    • Lower software costs and fix defects early
    • Deliver error-free software
    • Gain deep understanding of algorithm behavior

  • Optimization

    • Optimize software designs along key dimensions
    • Calibrate optimal system modifications
    • Derive actionable intelligence for users of your system

  • Constraint Solving

    • Rich computational modeling language with higher-order, recursive and nonlinear functions
    • Solve complex planning problems
    • Embed in mobile and autonomous systems for robust decision making

  • Symbolic Reasoning

    • Decompose system state spaces and elucidate edge cases
    • Obtain exact symbolic descriptions of possible system behaviors
    • Understand with precision what can possibly go wrong

  • Rule Synthesis

    • Automatically discover key system properties and invariants
    • Learn specifications from data
    • Derive complex transformations and API adapters from analyzing logs

  • Custom Plug-ins

    Extend Imandra's reasoning engine through domain-specific plugins

Learn more and
start your Imandra Journey

IPL Gallery PageCore GalleryDocumentation

We work with many of the world's largest and most trusted brands, universities and government agencies.

DarpaGoldman SachsOneChronosDigital Twin Consortium MemberThe University of EdinburghEdinburgh Centre for RoboticsUniversity of CambridgeExberryAdoptechSRI InrenationalItivitiROS IndustrialUS Navy

And we would be delighted to work with you.

Let's talkTalk
to an Expert

Schedule a contact

Not sure
if we can help?

We'd be happy to discuss your project to suggest the best solution.

Schedule a case analysis