Senior / Lead LEAN Engineer (LLM / AI) Singapore/UK

Stream: job postings

[Tom]

HI All,

I'm looking on behalf of a client who is building out a 20b Parameter Custom LLM or Automous Problem Solving and Logical Reasoning. Seeking a strong Theorem Proving Functional Engineer if interested please email me your CV: tom "at" HRnational.com.au for more info. (Please don't apply directly to the Client as I know it's quite easy to pull up their details with the spec below) :)

Senior Functional Programming Engineer

We are looking for a Senior Functional Programming Engineer to take a hands-on implementation approach in designing, implementing, and optimizing our theorem-proving AI system. You will contribute to research and development of critical components of our AI architecture: (a) formalizing mathematical, scientific and engineering problems into a domain knowledge model and representation, and (b) independent validation of outputs via formal verification systems.

The ideal candidate will have a strong background in functional programming languages, which we believe is the foundation for developing a logical reasoning AI system. We are especially interested in candidates who have worked in developing and using automated theorem provers, formal verification systems or applications, and symbolic computation/algebra systems extensively. A strong academic or research foundation in logic systems (higher/first-order logic, etc.) will be invaluable.

Key Responsibilities

• Lead the design and development of core components of our AI system’s knowledge model leveraging your functional programming language expertise.
• Implement and optimize algorithms for automated theorem proving, including but not limited to, proof search, term rewriting, and logical inference.
• Utilize knowledge of various logic systems and frameworks such as HOL, FOL, DL, Modal Logic, and Temporal Logic in algorithm development.
• Integrate various AI components, such as machine learning models and symbolic reasoning engines, into a cohesive system.
• Incorporate advanced mathematical concepts and formal methods into the design and development process.
• Apply optimization techniques using various problem solvers including SMT, SAT, CSP, ILP, QBF, MaxSAT, SMT-LIB, model checkers, theorem provers, and optimization solvers.
• Leverage Computer Algebra Systems (CAS) such as Mathematica, Maple, SageMath, Maxima, or SymPy for symbolic computation and algebraic manipulation.
• Collaborate with AI researchers and mathematicians, and other engineers to write good quality code and ensure seamless integration and interoperability of different system modules.
• Mentor junior engineers and provide technical guidance to the team, while being accountable for solid coding practices and quality output.

Experience & Qualifications

• Ph.D. in Computer Science or Mathematics (or Advanced Master’s degree)
• 10+ years of overall experience in software development with a reasonable duration focused on functional programming.
• Proven experience with developer tools and platforms focused on formal verification, such as Z3, Lean, Coq, Isabelle, or similar tools.
• Experience with Computer Algebra Systems (CAS) such as Mathematica, Maple, SageMath, Maxima, or SymPy.
• Experience with SMT (Satisfiability Modulo Theories) and/or SAT (Boolean Satisfiability Problem) solvers.
• Experience in developing logic systems, including knowledge of and/or experience with different logic systems and frameworks such as Higher-Order Logic (HOL), First-Order Logic (FOL), Description Logic (DL), Modal Logic, Temporal Logic, Prolog, TPTP, and Agda.

Desired Skills

• Strong understanding of functional programming principles and paradigms.
• Familiarity with automated theorem proving techniques and tools.
• Knowledge of formal methods and formal verification.
• Understanding of category theory, type theory, or other advanced mathematical concepts.
• Familiarity with logic theories such as Higher-Order Logic (HOL), First-Order Logic (FOL), Description Logic (DL), Modal Logic, and Temporal Logic.
• Understanding of algebraic structures and symbolic computation.
• Experience with AI and machine learning frameworks is highly desirable.
• Contributions to open-source projects in the functional programming, AI, or formal verification communities.
• Experience in developing complex systems using LEAN4, Haskell, Scala, OCaml, or similar languages.
• Experience with other problem solvers such as CSP, ILP, QBF, MaxSAT, SMT-LIB, model checkers, theorem provers, and optimization solvers.

Thank you - We can sponsor an EP and relocate talent to Singapore (Great low tax bracket) or also consider remote from UK Hub.