³Ô¹ÏºÚÁÏ

Logos Research, a spinout from ³Ô¹ÏºÚÁÏ, is developing a technology to make computer code generated by AI models reliable enough for algorithmic trading and other applications where sound reasoning is critical.

With Logos, AI can move from ‘this looks right’ to ‘this is proven correct,’ the standard required for finance, science, and every system where almost-right is still wrong. The Logos team bring the rare combination of mathematics and real-world expertise needed to make this work. Dr Kanu Gulati Partner at Khosla Ventures

The London-based company has emerged from stealth after launching last year with funding from US investors in a seed round that was also joined by and .

It is now raising further funds to support ambitious plans to rapidly commercialise and scale its technology, initially targeting applications in financial services.

While programmers already make widespread use of AI to generate computer code, AI-generated code is highly error-prone and too risky to trust with mission-critical applications such as algorithmic trading.

“Algorithmic traders deploy complex systematic trading systems autonomously, and malfunctions can directly lead to significant losses,” said , an expert in mathematical finance at ³Ô¹ÏºÚÁÏ. “A technology that can verify the correctness of AI-generated algorithms as rapidly as an AI can generate them therefore has the potential to make a significant impact.”

Logos Research is developing a new architecture that can be applied on top of existing AI models to produce code that is logically correct and verified. It could also be used to support AI-driven science, quantum AI, and countless other applications that depend on robust reasoning.

Building and verifying formal reasoning

The solution is centred on a library of mathematical tools encoded in a programming language known as Lean that is based on formal logic. Under the direction of an AI agent, an AI model uses the library to generate computer code, and a verification layer then checks to see if the code performs as intended. If the code is faulty, the verification layer instructs the model to try again, in a rapid feedback loop that continues until the end user receives code that can be trusted.

“We’re aiming to start deploying our new approach in the real world quickly. Banks and hedge funds are an excellent initial use case because they have the motivation and resources to rapidly deploy the new technology,” said ,  Logos Research's co-founder and CEO, who is also an associate professor in ³Ô¹ÏºÚÁÏ’s Department of Mathematics.

The approach is designed to combine the raw power of the inferential learning and reasoning carried out by foundation models with the reliability and verifiability of formal reasoning.

“It is great to see a powerful initiative from ³Ô¹ÏºÚÁÏ that extends Lean formalisation beyond pure mathematics into applied mathematics – this will make it possible to guarantee that AI-generated algorithms perform to specification,” said , a Lean expert from ³Ô¹ÏºÚÁÏ’s Department of Mathematics and advisor to the company.

World-leading expertise

Logos Research was founded by Dr Salvi and its CTO Dr Robert Smith, former Global Head of Automated Trading and Data Science at Citi. In addition to a team of world-class in-house mathematicians, the company has brought in world-leading experts as advisors, including Professor Buzzard and Fields Medalist from ³Ô¹ÏºÚÁÏ, and from the University of Oxford.

“Logos stands out for being built by a mixture of world-class mathematicians and quant finance managers, a combination reminiscent of Renaissance Technologies, Jim Simons’ legendary quant fund,” said Po Bronson, General Partner at SOSV.

While financial services are the initial market, the founders say that the technology could improve the performance of AI in all applications where sound algorithmic reasoning is required.

Tackling an AI bottleneck

Dr Kanu Gulati, Partner at Khosla Ventures, said: “All software is becoming AI-native, but verifiability is still the bottleneck. Logos formalizes intent in Lean so AI can move from ‘this looks right’ to ‘this is proven correct,’ the standard required for finance, science, and every system where almost right is still wrong. Cristopher, Robert, and the Logos team bring the rare combination of deep formal mathematics and real-world systems expertise needed to make this work at scale.”

“The solution Logos is developing will do more than just make an impact around the margins,” added Mr Bronson. “As an algorithm prover, it belongs everywhere that algorithms are used, which means the whole AI universe. Early markets include programming code, algorithmic finance, quantum computing, and scientific research. It could also provide a governance layer to improve the outputs of general-purpose foundation models.”